Изменения
Нет описания правки
|proof=
#<tex> \mathrm{CNFSAT} \in \mathrm{NP} </tex> <br> Можно написать недетерминированную программу <tex>p</tex>, которая распознает язык <tex> \mathrm{CNFSAT} </tex>. Она будет недетерминированно выбирать подстановку, проверять, истинна ли формула при такой подстановке, и выдавать ответ.
# <tex> \mathrm{CNFSAT} \in \mathrm{NPH} </tex> <br>Сведем задачу <tex> \mathrm{SAT} </tex> к задаче <tex> \mathrm{CNFSAT} </tex>. Построим функцию <tex> f(x) </tex>, которая будет строить по булевой формуле, булевую формулу в [[КНФ]], такую что <tex> x \in \mathrm{SAT} \Leftrightarrow f(x) \in \mathrm{CNFSAT} </tex>, причем <tex> |f(x)| \le p(|x|) </tex> для некоторого полинома <tex> p </tex>. <br> Опишем как будет работать функция <tex> f </tex>.
##Для начала преобразуем формулу так, чтобы все отрицания относились только к переменным. Это можно сделать по правилам:
##* <tex> \neg{(x \lor y)} = \neg{x} \land \neg{y} </tex>
##* <tex> \neg{(x \land y)} = \neg{x} \lor \neg{y} </tex>
## Далее построим дерево по формуле <tex> x </tex>. Будем строить формулу в [[КНФ]] для поддеревьев рекурсивно. Есть два случая:
##* Вершина Корень дерева {{---}} <tex> \land </tex>. Пусть левое и правое поддерево <tex> x </tex> {{---}} это <tex> x_l </tex> и <tex> x_r </tex> соответственно. Тогда <tex> f(x) = f(x_l) \land f(x_r) </tex>.##* Вершина Корень дерева {{---}} <tex> \lor </tex>.Пусть левое и правое поддерево <tex> x </tex> {{---}} это <tex> x_l </tex> и <tex> x_r </tex> соответственно. Создадим новую переменную <tex> z </tex>. Тогда <tex> f(x) = (f(x_l) \lor z) \land (f(x_r) \lor \neg{z}) </tex>. <tex> f(x_l) </tex> и <tex> f(x_r) </tex> {{---}} формулы в [[КНФ]], поэтому переменную <tex> z </tex> и ее отрицание можно внести в каждую скобку в <tex> f(x_l) </tex> и <tex> f(x_r) </tex>.## Посчитаем какой длины будет <tex> f(x) </tex>. Это зависит от количества логических операций в формуле. Заметим, что количество скобок в конечной формуле равно количеству операций <tex> \land </tex>. Количество операций <tex> \land </tex> не более чем <tex> |x| </tex>, так как <tex> \land </tex> добавляется один раз в первом из рассмотренных выше случаев. А во втором из рассмотренных случаев добавляется <tex> \lor </tex> в том количестве, сколько скобок у нас есть. А количество скобок равно количеству <tex> \land </tex>, поэтому количество операций <tex> \lor </tex> не превысит <tex> |x|^2 </tex>. <tex> \mathrm{CNFSAT} \in \mathrm{NP} \land \mathrm{CNFSAT} \in \mathrm{NPH} \Rightarrow \mathrm{CNFSAT} \in \mathrm{NPC} </tex>
}}
=== NP-полнота 3-SAT ===
