Теорема Карпа-Липтона — различия между версиями
(→Доказательство) |
(→Доказательство) |
||
Строка 12: | Строка 12: | ||
Рассмотрим язык <tex>L\in Pi_2</tex>. Это означает, что <tex>x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}</tex> | Рассмотрим язык <tex>L\in Pi_2</tex>. Это означает, что <tex>x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}</tex> | ||
− | Рассмотрим <tex>L_1 = {<x,y>|\exists{z}: \psi{(x,y,z)}}</tex> | + | Рассмотрим <tex>L_1 = \{<x,y>|\exists{z}: \psi{(x,y,z)}\}</tex> |
<tex>L_1 \in NP</tex> по определению <tex>NP</tex> | <tex>L_1 \in NP</tex> по определению <tex>NP</tex> | ||
Строка 20: | Строка 20: | ||
Нужно доказать что <tex>L\in \Sigma_1</tex> | Нужно доказать что <tex>L\in \Sigma_1</tex> | ||
− | <tex>L_1\in{} NP \Rightarrow L_1 \le{}_m SAT</tex> по карпу с помощью <tex>f</tex>, т.е. <tex>L={x|\forall{y} f(<x,y>)\in{SAT}}</tex> | + | <tex>L_1\in{} NP \Rightarrow L_1 \le{}_m SAT</tex> по карпу с помощью <tex>f</tex>, т.е. <tex>L=\{x|\forall{y} f(<x,y>)\in{SAT}\}</tex> |
− | <tex>f(<x,y>)\in{SAT}</tex> - это значит, что для некоторого набора формул выполняется для всего набора, если предположить, что <tex>L={x|\forall{y} C_n(f(<x,y>))=1}</tex> | + | <tex>f(<x,y>)\in{SAT}</tex> - это значит, что для некоторого набора формул выполняется для всего набора, если предположить, что <tex>L=\{x|\forall{y} C_n(f(<x,y>))=1\}</tex> |
Но надо откуда-то взять этот набор. Можно его угадать, используя квантор существует. Добавим его. | Но надо откуда-то взять этот набор. Можно его угадать, используя квантор существует. Добавим его. | ||
Так как <tex>NP \in{} P/poly</tex> то | Так как <tex>NP \in{} P/poly</tex> то | ||
− | </tex>L={x|\exists{C_n}: C_n решает SAT и \forall{y} C_n(f(<x,y>))=1}</tex> | + | </tex>L=\{x|\exists{C_n}: C_n решает SAT и \forall{y} C_n(f(<x,y>))=1\}</tex> |
Что означает <tex>C_n</tex> решает <tex>SAT</tex>? Нужно переписать с квантором для любого. | Что означает <tex>C_n</tex> решает <tex>SAT</tex>? Нужно переписать с квантором для любого. | ||
<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>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>SAT</tex>: <tex>L=\{x|\exists{C1,C2,..,Cn} - набор логических схем для SAT и\forall{y} C_n(f(<x,y>))=1\}</tex> |
Внутри будем проверять используемый набор | Внутри будем проверять используемый набор |
Версия 14:36, 15 апреля 2010
Формулировка
Теорема Карпа-Липтона
то
Доказательство
Пусть есть логические схемы для
. Например который кодирует символов, разрешимых логической схемой . Размер . Это означает что для фиксированного такая логическая схема , чтоСуществует C_n для любого fi (для любого x fi(x)=0 <=>C_n(fi)=0).
Рассмотрим язык
. Это означает, чтоРассмотрим
по определению
Нужно доказать что
по карпу с помощью , т.е.
- это значит, что для некоторого набора формул выполняется для всего набора, если предположить, что
Но надо откуда-то взять этот набор. Можно его угадать, используя квантор существует. Добавим его. Так как
то </tex>L=\{x|\exists{C_n}: C_n решает SAT и \forall{y} C_n(f(<x,y>))=1\}</tex>Что означает
решает ? Нужно переписать с квантором для любого. решаетВоспользуемся самосведением
:Внутри будем проверять используемый набор для любого fi (С_|fi|(fi)=0 => для любого x fi(x)=0) (C_|fi|(fi)=1 => fi|_x1=0 \in SAT или fi|_x1=1 \in SAT) Если C решает SAT то все хорошо, если нет то зафиксируем формулу на которой не решает. Если выдаст 0 а должна выдать 1 то первое не удолветворяет, если наоборот то обе не удовлетворяет.
для любого fi |fi|=m для любого x_1...любого x_m если C_m(fi)=0 => fi(x_1)=0 иначе C_m-1(fi|_x_1=0)=0 => fi|_x1=0(x2)=0 C_m-1(fi|_x1=1)=0 =>fi|_x1=0(x2)=0 C_m-1(fi|x1=0) галочка C_m-1(fi|x1=1)
Получаем что
Теорема доказана