NP-полнота задачи о выполнимости булевой формулы в форме КНФ — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 1: Строка 1:
 +
{| class="wikitable" align="center" style="color: red; background-color: black; font-size: 56px; width: 800px;"
 +
|+
 +
|-align="center"
 +
|'''НЕТ ВОЙНЕ'''
 +
|-style="font-size: 16px;"
 +
|
 +
24 февраля 2022 года российское руководство во главе с Владимиром Путиным развязало агрессивную войну против Украины. В глазах всего мира это военное преступление совершено от лица всей страны, всех россиян.
 +
 +
Будучи гражданами Российской Федерации, мы против своей воли оказались ответственными за нарушение международного права, военное вторжение и массовую гибель людей. Чудовищность совершенного преступления не оставляет возможности промолчать или ограничиться пассивным несогласием.
 +
 +
Мы убеждены в абсолютной ценности человеческой жизни, в незыблемости прав и свобод личности. Режим Путина — угроза этим ценностям. Наша задача — обьединить все силы для сопротивления ей.
 +
 +
Эту войну начали не россияне, а обезумевший диктатор. И наш гражданский долг — сделать всё, чтобы её остановить.
 +
 +
''Антивоенный комитет России''
 +
|-style="font-size: 16px;"
 +
|Распространяйте правду о текущих событиях, оберегайте от пропаганды своих друзей и близких. Изменение общественного восприятия войны - ключ к её завершению.
 +
|-style="font-size: 16px;"
 +
|[https://meduza.io/ meduza.io], [https://www.youtube.com/c/popularpolitics/videos Популярная политика], [https://novayagazeta.ru/ Новая газета], [https://zona.media/ zona.media], [https://www.youtube.com/c/MackNack/videos Майкл Наки].
 +
|}
 +
 
==== Определения ====
 
==== Определения ====
 
* ''Литералом'' является переменная или отрицание переменной. Например, <tex> x </tex> или <tex> \neg y </tex>.
 
* ''Литералом'' является переменная или отрицание переменной. Например, <tex> x </tex> или <tex> \neg y </tex>.

Версия 07:41, 1 сентября 2022

НЕТ ВОЙНЕ

24 февраля 2022 года российское руководство во главе с Владимиром Путиным развязало агрессивную войну против Украины. В глазах всего мира это военное преступление совершено от лица всей страны, всех россиян.

Будучи гражданами Российской Федерации, мы против своей воли оказались ответственными за нарушение международного права, военное вторжение и массовую гибель людей. Чудовищность совершенного преступления не оставляет возможности промолчать или ограничиться пассивным несогласием.

Мы убеждены в абсолютной ценности человеческой жизни, в незыблемости прав и свобод личности. Режим Путина — угроза этим ценностям. Наша задача — обьединить все силы для сопротивления ей.

Эту войну начали не россияне, а обезумевший диктатор. И наш гражданский долг — сделать всё, чтобы её остановить.

Антивоенный комитет России

Распространяйте правду о текущих событиях, оберегайте от пропаганды своих друзей и близких. Изменение общественного восприятия войны - ключ к её завершению.
meduza.io, Популярная политика, Новая газета, zona.media, Майкл Наки.

Определения

  • Литералом является переменная или отрицание переменной. Например, [math] x [/math] или [math] \neg y [/math].
  • Дизъюнктом называется логическое ИЛИ одного или нескольких литералов. Например, [math] x \vee \neg y \vee z [/math]
  • Говорят, что формула записана в конъюнктивной нормальной форме (КНФ), если представляет собой логическое И дизъюнктов.

Определение

[math] CNFSAT = \{\phi \ |\ \phi [/math] в КНФ, [math] \phi \in [/math] SAT [math] \} [/math] — задача о выполнимости булевой формулы в форме КНФ.

Теорема

[math] CNFSAT \in NPC [/math], то есть задача NP-полная.

Доказательство

Для доказательства теоремы необходимо установить два факта:

  • [math] CNFSAT \in NP [/math]
  • [math] CNFSAT \in NPH [/math]

Доказательство принадлежности классу NP

В качестве сертификата выберем множество [math] \{y_1, ...,y_n\} [/math], представляющее собой набор из нулей и единиц. Верификатору останется подставить эти значения в качестве аргументов в формулу [math] \phi(x_1, ..., x_n) [/math] и проверить, выдает ли она единицу. Длина сертификата и время работы верификатора, очевидно, удовлетворяют условиям полиномиальности. Таким образом, [math] CNFSAT \in NP [/math]

Доказательство принадлежности классу NPH

Выполним сведение по Карпу задачи [math] SAT [/math] к задаче [math] CNFSAT [/math]. Для этого необходимо построить функцию [math] f [/math], вычислимую за полиномиальное время от длины входа, которая выполняла бы преобразование [math] \phi \to \omega [/math], где [math] \omega [/math] в КНФ. Заметим, что в общем случае время построения эквивалентной формулы в форме КНФ может оказаться больше полиномиального. В частности, длина формулы может вырасти экспоненциально, и тогда время порождения тоже экспоненциально вырастет. Однако нам достаточно предъявить формулу [math] \omega [/math], которая будет выполнима тогда и только тогда, когда выполнима исходная формула [math] \phi [/math]. При этом формулы могут оказаться не эквивалентными, ввиду, например, добавления новых переменных.

Итак, опишем действия функции [math] f [/math].

  • На первом этапе все отрицания [math] \neg [/math] спускаются вниз по дереву выражения, так что в формуле остаются только отрицания переменных. Булева формула превращается в логические И и ИЛИ литералов. Это преобразование дает формулу, эквивалентную исходной, и занимает время, как максимум, квадратичное относительно длины этой формулы. Для этого используются законы Де Моргана и закон двойного отрицания.
  1. [math] \neg(x \wedge y) = \neg x \vee \neg y [/math]
  2. [math] \neg(x \vee y) = \neg x \wedge \neg y [/math]
  3. [math] \neg(\neg x) = x [/math]
  • Второй этап - переписать формулу, которая представляет собой логическое И и ИЛИ литералов, в виде произведения дизъюнктов, т.е. привести ее к КНФ. Введение новых переменных позволяет провести это преобразование за время, полиномиально зависящее от размера исходной формулы. Рассмотрим дерево разбора произвольной формулы. Листья этого дерева будут соответствовать литералам, а узлы - логической операции И или ИЛИ над двумя его потомками.
  1. Для узла с меткой И соответствующая КНФ получается как конъюнкция (И) всех дизъюнктов двух подформул [math] \alpha [/math] и [math] \beta [/math], уже находящихся в КНФ.
  2. Для узла с меткой ИЛИ нужно ввести новую переменную. Добавляем ее во все дизъюнкты левого операнда [math] \alpha [/math] и ее отрицание во все дизъюнкты правого операнда [math] \beta [/math]. Заметим, что формула [math] \alpha \vee \beta [/math] выполнима тогда и только тогда, когда выполнима [math] (\alpha \vee y) \wedge (\beta \vee \neg y), [/math] где [math] y [/math] - новая переменная. После чего, воспользовавшись законами преобразования в каждой формуле в скобках, получим формулы в КНФ: [math] \alpha \vee y = ((...)\wedge(...)\wedge ... \wedge(...)) \vee y = (...\vee y)\wedge(...\vee y)\wedge...\wedge(...\vee y). [/math] Аналогично преобразуем [math] \beta \vee \neg y [/math].

Каждый раз новая формула увеличивается не более, чем на количество листьев в поддереве, а значит максимальный размер формулы [math] \omega [/math] можно представить как (число листьев) * (число вершин), что соответствует оценке работы алгоритма [math] O(|\phi|^2) [/math]. Таким образом, условия сведения выполнены, и действительно [math] CNFSAT \in NPH [/math].

Теорема доказана.