33
правки
Изменения
Нет описания правки
'''Теорема Карпа-Липтона'''
Если <math>NP \subset P/poly</math> то <math>\Sigma_2=\Pi_2</math>
== Доказательство ==
Пусть есть логические схемы для <tex>NP</tex> (для любой задаче задачи из NP).Например зафиксируем Зафиксируем любую задачу из <tex>NP например </tex>. Например пусть сат разрешает <tex>SAT</tex> разрешается логическими схемами <tex>SAT : C_1...C_n...</tex>, сат который поддерживается (<tex>SAT</tex> с одним битом разрешается логической схемой с1 сат <tex>C_1</tex>, <tex>SAT</tex> с двумя переменными логической схемой с2.<tex>C_2</tex> и т.д.Что значит разрешается? Это значит что логическая схема, в инпуте которой который каким то логичным образом закодирована формула, а на выходе логичным образом в вмде 0 и один закодировано есть ли доказательство(разложение) или нет. И причем размер этой логической схемы не больше чем какой то полином от n. Но мы не утверждаем, что можем как то конструктивно их построить. Если бы мы могли за полином их построить, то это бы означало, что сат2=п2, что P=NP.Итак, что это означает, рассмотрим, это означает на самом деле что для любого n (зафиксируем n)
'''Что такое <tex>\forall{\varphi{}} (C_{|\varphiexists{z}|}(\varphi{})=0 \Rightarrow :\forallpsi{x} \varphi(x,y,z)=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> L_1 \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)=0in NP</tex> по определению <tex>NP</tex>
Таким образом получается, что <tex>C_{m-1}(L=\varphi{}x|_\forall{x_1=1y})=0 \Rightarrow <x,y>\varphiin{L_1}|_{x_1=0\}(x_2)=0</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>
'''Что такое <tex>C_n</tex> Решает <tex>SAT</tex>?'''
Запишем это используя квантор "<tex>\forall{}</tex>".
Воспользуемся самосведением <tex> SAT</tex>: <tex>L=\{x|\exists{C_nC1,C2,..,Cn} \forall{\varphi{}y} C_n(\forall{x} \varphi{f(<x,y>))}=0 1\Leftrightarrow C_n(\varphi{})=0)</tex>,где - <tex>C1,C2,..,Cn</tex> набор логических схем для <tex>SAT</tex>.
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, то зафиксируем формулу <tex>\varphi{}_0</tex>, которую он не решает. Если на этой формуле выдаст 0, а должна выдать 1, то получается что не удовлетворяет первую часть предыдущего выражения и, значит, не будет работать. Если наоборот выдаст 1 а на самом деле формула не удавлетворима то обе скобки не выполнятся и опять формула работать не будет.
Рассмотрим минимальную неправильную схему. Тогда на той формуле, на которой эта схема неправильна, по предположению, что все более короткие формулы правильны,эта формула распознается схемами с меньшим числом входов. Поэтому обе скобки будут 0 и мы не узнаем набор схем. Развернем формулу до конца.
<tex> \forall{\varphi{}}: |\varphi{}|=m \forall{x_1}..\forall{x_m} </tex><tex> C_m(\varphi{})=0 \Rightarrow \varphi{(x_1)}=0</tex>
иначе <tex> 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.
Второй вариант был угадать не только булевы схемы для сат но и те схемы, которые выдают правильные значения.
Получаем что <math>L\in \Sigma_2</math>
Теорема доказана