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

Определения

• Литералом является переменная или отрицание переменной. Например, [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], то есть задача [math] CNFSAT [/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 \Sigma_1 = 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] \omega [/math] можно представить как (число листьев) * (число вершин), что соответствует оценке работы алгоритма [math] O(|\phi|^2) [/math]. Таким образом, условия сведения выполнены, и действительно [math] CNFSAT \in NPH [/math].

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