Изменения

Перейти к: навигация, поиск

Теорема Карпа-Липтона

640 байт убрано, 10:24, 4 июня 2010
Нет описания правки
\vee{}</tex>
<tex>(C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)</tex>
 
 
Вот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далее. Это правильная проверка причем за полином
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, то зафиксируем формулу <tex>\varphi{}_0</tex>, которую он не решает. Если на этой формуле выдаст 0, а должна выдать 1, то получается что не удовлетворяет первую часть предыдущего выражения и, значит, не будет работать. Если наоборот выдаст 1 а на самом деле формула не удавлетворима то обе скобки не выполнятся и опять формула работать не будет.
<tex>C_{m-1}(\varphi{}|_{x_1=1})=0 \Rightarrow \varphi{}|_{x_1=0}(x_2)=0</tex>
<tex>C_{m-1}(\varphi{}|{x_1=0}) \vee{} C_{m-1}(\varphi{}|_{x_1=1})</tex>
И Далее рекурсивно вызываемся от того из них которое равно 1. Ту записываем ту же самую формулу но записываем от того из них , которое равно 1 (это же предикат но для того из них фи при х1= для которого труе). Второй вариант был угадать не только будевы булевы схемы для сат но и те схемы, которые выдают нам правильные значения .
Получаем что <math>L\in \Sigma_2</math>
 
Теорема доказана
33
правки

Навигация