14
правок
Изменения
Нет описания правки
==== Определения ====
* ''Литералом'' является переменная или отрицание переменной. Например, <tex>x</tex> или <tex>\neg y</tex>.* ''Дизъюнктом'' называется логическое '''ИЛИ''' одного или нескольких литералов. Например, <tex>x \vee \neg y \vee z</tex>
* Говорят, что формула записана в ''конъюнктивной нормальной форме'' (КНФ), если представляет собой логическое '''И''' дизъюнктов.
==== Определение ====
<tex>CNFSAT = \{\phi \ |\ \phi </tex> ''в КНФ,'' <tex>\phi \in </tex> [[SAT]] <tex> \} </tex> — задача о выполнимости булевой формулы в форме КНФ.
== Теорема ==
* <tex> CNFSAT \in NPH </tex>
==== Доказательство принадлежности классу NP ====
В качестве сертификата выберем множество <tex>\{y_1, ...,y_n\}</tex>, представляющее собой набор из нулей и единиц. Верификатору останется подставить эти значения в качестве аргументов в формулу <tex>\phi(x_1, ..., x_n)</tex> и проверить, выдает ли она единицу. Длина сертификата и время работы верификатора, очевидно, удовлетворяют условиям полиномиальности. Таким образом, <tex>CNFSAT \in \Sigma_1 = NP</tex>
==== Доказательство принадлежности классу NPH ====
Выполним [[сведение по Карпу]] задачи <tex>SAT</tex> к задаче <tex>CNFSAT</tex>. Для этого необходимо построить функцию <tex>f</tex>, вычислимую за полиномиальное время от длины входа, которая выполняла бы преобразование <tex>\phi \to \omega</tex>, где <tex>\omega</tex> в КНФ. Заметим, что в общем случае время построения эквивалентной формулы в форме КНФ может оказаться больше полиномиального. В частности, длина формулы может вырасти экспоненциально, и тогда время порождения тоже экспоненциально вырастет. Однако нам достаточно предъявить формулу <tex>\omega</tex>, которая будет выполнима тогда и только тогда, когда выполнима исходная формула <tex>\phi</tex>. При этом формулы могут оказаться не эквивалентными, ввиду, например, добавления новых переменных.
Итак, опишем действия функции <tex>f</tex>.
* На первом этапе все отрицания <tex> \neg </tex> спускаются вниз по дереву выражения, так что в формуле остаются только отрицания переменных. Булева формула превращается в логические '''И''' и '''ИЛИ''' литералов. Это преобразование дает формулу, эквивалентную исходной, и занимает время, как максимум, квадратичное относительно длины этой формулы. Для этого используются ''законы Де Моргана'' и ''закон двойного отрицания''.
# <tex> \neg(x \wedge y) = \neg x \vee \neg y </tex>
* Второй этап - переписать формулу, которая представляет собой логическое '''И''' и '''ИЛИ''' литералов, в виде произведения дизъюнктов, т.е. привести ее к КНФ. Введение новых переменных позволяет провести это преобразование за время, полиномиально зависящее от размера исходной формулы.
Рассмотрим дерево разбора произвольной формулы. Листья этого дерева будут соответствовать литералам, а узлы - логической операции '''И''' или '''ИЛИ''' над двумя его потомками.
- Для узла с меткой '''И''' соответствующая КНФ получается как конъюнкция ('''И''') всех дизъюнктов двух подформул <tex> \alpha </tex> и <tex> \beta </tex>.
- Для узла с меткой '''ИЛИ''' нужно ввести новую переменную. Добавляем ее во все дизъюнкты левого операнда <tex> \alpha </tex> и ее отрицание во все дизъюнкты правого операнда <tex> \beta </tex>. Можно заметить, что формула <tex> \alpha \vee \beta </tex> выполнима тогда и только тогда, когда выполнима <tex> (\alpha \vee y) \wedge (\beta \vee \neg y) </tex>.
