Изменения

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

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

1549 байт добавлено, 22:57, 2 июня 2010
Нет описания правки
<tex>C_n</tex> решает <tex>SAT</tex> <tex>\Leftrightarrow</tex> если <tex>\forall{\varphi} \forall{x} (fi(x)=1 \Rightarrow C_n(fi)=1)</tex>
Воспользуемся самосведением <tex>SAT</tex>: <tex>L=\{x|\exists{C1,C2,..,Cn} - набор логических схем для SAT и\forall{y} C_n(f(<x,y>))=1\}</tex>
Внутри будем проверять используемый набор
<tex>\forall{\varphi{}} (C_{|\varphi{}|}(\varphi{})=0 \Rightarrow \forall{x} \varphi(x)=0) (C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)</tex>
// Если Cn(фи)=0 то для любого x (для любого тут можем использовать) фи(х)=0
Если Cn(фи)=1 то либо фи(ч1=0) принадлежит сат либо фи(х1=1) принадлежит сат тут не N а длина фи
Вот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далее. Это правильная проверка причем за полином
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо, если нет то зафиксируем формулу которую он не решает. Если выдаст 0 а должна выдать 1 то вот эту первую часть не удолветворяет и тут не будет работать, если наоборот выдаст 1 а на самом деле формула не удавлетворима то ни эта ни эта не будет работать
Рассмотрим минимальную схему которая неправильна, тогда на той формуле, на которой эта схема неправильна по предположению что все более короткие формулы правильны,эта распознается схемами с меньшим числом входов, поэтому и эта и эта будут 0 и мы не узнаем набор схем. Можно попробовать развернуть формулу до конца. Видимо это будет выглядеть так
<tex> \forall{\varphi{}}: |\varphi{}|=m \forall{x_1}..\forall{x_m} если C_m(\varphi{})=0 \Rightarrow \varphi{(x_1)}=0 иначе C_{m-1}(\varphi|_{x_1=0})=0 \Rightarrow \varphi|_{x_1=0}(x_2)=0</tex>
<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>
Рассмотрим <tex>L_1 = \{<x,y>|\exists{z}: \psi{(x,y,z)}\}</tex>
 
 
 
 
Воспользуемся самосведением <tex>SAT</tex>: <tex>L=\{x|\exists{C1,C2,..,Cn} - набор логических схем для SAT и\forall{y} C_n(f(<x,y>))=1\}</tex>
Внутри будем проверять используемый набор
<tex>\forall{\varphi{}} (C_{|\varphi{}|}(\varphi{})=0 \Rightarrow \forall{x} \varphi(x)=0) (C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)</tex>
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо, если нет то зафиксируем формулу на которой не решает. Если выдаст 0 а должна выдать 1 то первую не удолветворяет, если наоборот то обе не удовлетворяет.
<tex> \forall{\varphi{}}: |\varphi{}|=m \forall{x_1}..\forall{x_m} если C_m(\varphi{})=0 \Rightarrow \varphi{(x_1)}=0 иначе C_{m-1}(\varphi|_{x_1=0})=0 \Rightarrow \varphi|_{x_1=0}(x_2)=0</tex>
<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>
Получаем что <math>L\in \Sigma_2</math>
Теорема доказана
Анонимный участник

Навигация