Изменения

* ''Литералом'' является переменная или отрицание переменной. Например, <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> &mdash; задача о выполнимости булевой формулы в форме КНФ.

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

* <tex> CNFSAT \in NP </tex>* <tex> CNFSAT \in NPH </tex>==== Доказательство принадлежности классу NP ====В качестве сертификата выберем множество <tex> \{y_1, ...,y_n\} </tex>, представляющее собой набор из нулей и единиц. Верификатору останется подставить эти значения в качестве аргументов в формулу <tex> \phi(x_1, ..., x_n) </tex> и проверить, выдает ли она единицу. Длина сертификата и время работы верификатора, очевидно, удовлетворяют условиям полиномиальности. Таким образом, <tex> CNFSAT \in 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> \neg(x \vee y) = \neg x \wedge \neg y </tex># <tex> \neg(\neg x) = x </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> где <tex> y </tex> - новая переменная. После чего, воспользовавшись законами преобразования в каждой формуле в скобках, получим формулы в КНФ: <tex> \alpha \vee y = ((...)\wedge(...)\wedge ... \wedge(...)) \vee y = (...\vee y)\wedge(...\vee y)\wedge...\wedge(...\vee y). </tex> Аналогично преобразуем <tex> \beta \vee \neg y </tex>.Каждый раз новая формула увеличивается не более, чем на количество листьев в поддереве, а значит максимальный размер формулы <tex> \omega </tex> можно представить как ''(число листьев) * (число вершин)'', что соответствует оценке работы алгоритма <tex> O(|\phi|^2) </tex>. Таким образом, условия сведения выполнены, и действительно <tex> CNFSAT /\in NPH </tex>. Теорема доказана. [[Категория:NP]]