Редактирование: Теорема Карпа-Липтона

== Формулировка ==
'''Теорема Карпа-Липтона''' 

<math>NP \subset P/poly</math> то <math>\Sigma_2=\Pi_2</math>

== Доказательство ==
Пусть есть логические схемы для <tex>NP</tex> (для любой задачи из NP). Зафиксируем любую задачу из <tex>NP</tex>. Например пусть <tex>SAT</tex> разрешается логическими схемами <tex> C_1...C_n... </tex> (<tex>SAT</tex> с одним битом разрешается логической схемой <tex>C_1</tex>, <tex>SAT</tex> с двумя переменными логической схемой <tex>C_2</tex> и т.д.).


'''Что значит "разрешается логической схемой"?'''

Это значит что если на вход логической схеме подать каким-то логичным образом закодированную формулу, то на выходе получется логичным образом в виде 0 и 1 закодированный ответ - имеется разложение или нет. И причем размер этой логической схемы <tex>|C_n|\le p(n) </tex>, где <tex>p(n)</tex> - какой-то полином.

Здесь не утверждается, что эти логические схемы можно как-то конструктивно построить. Если бы их было возможно построить за полином, то это бы означало, что <tex>SAT_2=\Pi_2</tex> и значит <tex>P = NP</tex>.

Итак, получается, что если зафиксировать <tex>n</tex>, то для этого фиксированного <tex>n</tex> будет
 <tex>\exists{C_n}\forall{} формулы \varphi{} (\varphi{} \in{} SAT  |\varphi{}|=n \Leftrightarrow C_n(\varphi{})=1)</tex> 
 <tex> \exists{C_n} \forall{\varphi{}} (\forall{x} \varphi{(x)}=0 \Leftrightarrow C_n(\varphi{})=0)</tex>, где <tex>x</tex> - вход длины <tex>n</tex>

Рассмотрим язык <tex>L\in \Pi_2</tex>. Это означает, что <tex>x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}</tex>


'''Что такое <tex>\exists{z}:\psi{(x,y,z)}</tex>?'''

----

Обозначим пары <tex><x,y></tex>, для которых такой <tex>z</tex> существует как какой нибудь язык <tex>L_1</tex>.
 <tex>L_1 = \{<x,y>|\exists{z}: \psi{(x,y,z)}\}</tex>.

Заметим что <tex>L_1 \in NP</tex> по определению <tex>NP</tex>

Таким образом получается, что
 <tex>L=\{x|\forall{y} <x,y>\in{L_1}\}</tex>

----


'''Требуется доказать, что <tex>L\in \Sigma_1</tex>'''

Если <tex>L_1\in{} NP</tex> то <tex>L_1 \le{}_m SAT</tex> с помощью <tex>f</tex>, т.е. 
 <tex>L=\{x|\forall{y} f(<x,y>)\in{SAT}\}</tex>


'''Что такое "<tex>f(<x,y>)\subset{SAT}</tex>"?'''

<tex>f(<x,y>)\subset{SAT}</tex> <tex>--</tex> для некоторого набора логических схем это означает выполнимость всего этого набора. Если предположить, что набор этих схем известен, то получится, что
 <tex>L=\{x|\forall{y} C_n(f(<x,y>))=1\}</tex>,
где <tex>n</tex>- длина входа <tex><x,y></tex>.

Требуется откуда то взять этот набор. Его можно угадать, используя квантор "<tex>\exists{}</tex>" снаружи.

<tex>C_n</tex> существует по предположению, что <tex>NP \subset{P/poly}</tex> т.е.
 <tex>L=\{x|\exists{C_n}: C_n</tex> решает <tex>SAT</tex> и <tex>\forall{y} C_n(f(<x,y>))=1\}</tex>


'''Что такое Cn Решает SAT?''' 

Запишем это используя квантор "<tex>\forall{}</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} \forall{y} C_n(f(<x,y>))=1\}</tex>,
где - <tex>C1,C2,..,Cn</tex> набор логических схем для <tex>SAT</tex>.

Внутри будем проверять используемый набор 
 <tex>\forall{\varphi{}} (C_{|\varphi{}|}(\varphi{})=0 \Rightarrow \forall{x}  \varphi{}(x)=0) \label{f1}
\vee{}</tex>
    <tex>(C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)\label{f2}</tex>


 Вот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далее. Это правильная проверка причем за полином

Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, то зафиксируем формулу <tex>\varphi{}_0</tex>, которую он не решает. Если на этой формуле выдаст 0, а должна выдать 1, то получается что не удовлетворяет первую часть <tex>(\ref{f1})</tex>и не будет работать, если наоборот выдаст 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> И рекурсивно вызываемся от того из них которое равно 1. Ту же самую формулу но записываем от того из них которое равно 1 (это же предикат но для того из них фи при х1= для которого труе)
Второй вариант был угадать не только будевы схемы для сат но и те которые выдают нам правильные значения
 

Получаем что <math>L\in \Sigma_2</math>
Теорема доказана