53
правки
Изменения
Нет описания правки
* Второй этап - переписать формулу, которая представляет собой логическое '''И''' и '''ИЛИ''' литералов, в виде произведения дизъюнктов, т.е. привести ее к КНФ. Введение новых переменных позволяет провести это преобразование за время, полиномиально зависящее от размера исходной формулы. Рассмотрим дерево разбора произвольной формулы. Листья этого дерева будут соответствовать литералам, а узлы - логической операции '''И''' или '''ИЛИ''' над двумя его потомками.
# Для узла с меткой '''И''' соответствующая КНФ получается как конъюнкция ('''И''') всех дизъюнктов двух подформул <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> \omega </tex> можно представить как ''(число листьев) * (число вершин)'', что соответствует оценке работы алгоритма <tex> O(|\phi|^2) </tex>. Таким образом, условия сведения выполнены, и действительно <tex> CNFSAT \in NPH </tex>.
Теорема доказана.
