1632
правки
Изменения
м
Существует C_n для любого fi (для любого x fi(x)=0 <=>C_n(fi)=0).
Рассмотрим язык <tex>L\in Pi_2</tex>. Это означает, что <tex>x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}</tex>'''Что значит "разрешается логической схемой"?'''
Рассмотрим Это значит что если на вход логической схеме подать каким-то логичным образом закодированную формулу, то на выходе получется логичным образом в виде 0 и 1 закодированный ответ - имеется разложение или нет. И причем размер этой логической схемы <tex>L_1 = |C_n|\{le p(n) <x/tex>,yгде <tex>|\exists{z}: \psi{p(x,y,zn)}\}</tex>- какой-то полином.
Нужно доказать Рассмотрим язык <tex>L\in \Pi_2</tex>. Это означает, что <tex>x\in L\in Leftrightarrow \forall{y} \exists{z}: \Sigma_1psi{(x,y,x)}</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>NP \in{} P/poly</tex> то </tex>L=\{x|\exists{C_n}: C_n решает SAT и \forall{y} C_n(f(<x,y>))=1\}</tex>---
Что означает Обозначим пары <tex>C_n</tex> решает <texx,y>SAT</tex>? Нужно переписать с квантором , для любого.которых такой <tex>C_nz</tex> решает существует как какой нибудь язык <tex>SATL_1</tex> . <tex>L_1 = \Leftrightarrow{</tex> <texx,y>|\forallexists{\varphiz} : \forallpsi{x} (fi(x,y,z)=1 }\Rightarrow C_n(fi)=1)}</tex>.
для любого fi <tex>\forall{\varphi{}} (С_C_{|fi\varphi{}|}(fi\varphi{})=0 => для любого \Rightarrow \forall{x fi} \varphi{}(x)=0) \vee{}</tex> <tex>(C_{|fi\varphi{}|}(fi\varphi{})=1 => fi\Rightarrow \varphi{}|_x1_{x_1=0 } \in SAT или fi\varphi{}|_x1_{x_1=1 } \in SAT)Если C решает SAT то все хорошо, если нет то зафиксируем формулу на которой не решает. Если выдаст 0 а должна выдать 1 то первое не удолветворяет, если наоборот то обе не удовлетворяет.</tex>
для любого fi Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, то зафиксируем формулу <tex>\varphi{}_0</tex>, которую он не решает. Если на этой формуле выдаст 0, а должна выдать 1, то получается что не удовлетворяет первую часть предыдущего выражения и, значит, не будет работать. Если наоборот выдаст 1 а на самом деле формула не удавлетворима то обе скобки не выполнятся и опять формула работать не будет. Рассмотрим минимальную неправильную схему. Тогда на той формуле, на которой эта схема неправильна, по предположению, что все более короткие формулы правильны,эта формула распознается схемами с меньшим числом входов. Поэтому обе скобки будут 0 и мы не узнаем набор схем. Развернем формулу до конца. <tex> \forall{\varphi{}}: |fi\varphi{}|=m для любого \forall{x_1}...любого \forall{x_m если } </tex><tex> C_m(fi\varphi{})=0 => fi\Rightarrow \varphi{(x_1)}=0 </tex> иначе C_m<tex> C_{m-1}(fi\varphi|_x_1_{x_1=0})=0 => fi\Rightarrow \varphi|_x1_{x_1=0}(x2x_2)=0</tex>C_m <tex>C_{m-1}(fi\varphi{}|_x1_{x_1=1})=0 =>fi\Rightarrow \varphi{}|_x1_{x_1=0}(x2x_2)=0</tex>C_m <tex>C_{m-1}(fi\varphi{}|x1{x_1=0}) галочка C_m\vee{} C_{m-1}(fi\varphi{}|x1_{x_1=1})</tex> Далее рекурсивно записываем ту же самую формулу от того из них, которое равно 1. Второй вариант был угадать не только булевы схемы для сат но и те схемы, которые выдают правильные значения.
rollbackEdits.php mass rollback
'''Теорема Карпа-Липтона'''
Если <math>NP \in subset P/poly</math> то <texmath>\Sigma_2=\Pi_2</texmath>
== Доказательство ==
Пусть есть логические схемы для <tex>NP</tex>(для любой задачи из NP). Например Зафиксируем любую задачу из <tex>C_1...C_n...NP</tex> . Например пусть <tex>SAT</tex> который кодирует разрешается логическими схемами <tex>iC_1...C_n... </tex> символов, разрешимых логической схемой (<tex>C_iSAT</tex>. Размер с одним битом разрешается логической схемой <tex>|C_i|\le p(n)C_1</tex>.Это означает что для фиксированного , <tex>nSAT</tex> с двумя переменными логической схемой <tex>\exists{}C_2</tex> такая логическая схема <tex>C_n</tex>, что <tex>\forall{}\varphi{} (\varphi{} \in{} SAT |\varphi{}|=n \Leftrightarrow C_n(\varphi{}и т.д.)=1)</tex> .
Здесь не утверждается, что эти логические схемы можно как-то конструктивно построить. Если бы их было возможно построить за полином, то это бы означало, что <tex>L_1 SAT_2=\in NPPi_2</tex> по определению и значит <tex>P = NP</tex>.
Итак, получается, что если зафиксировать <tex>n</tex>L, то для этого фиксированного <tex>n</tex> будет <tex>\exists{C_n}\forall{} формулы \varphi{} (\varphi{} \in{} SAT |\varphi{}|=n \Leftrightarrow C_n(\varphi{x|})=1)</tex> <tex> \exists{C_n} \forall{y\varphi{} <} (\forall{x,y>} \invarphi{L_1(x)}=0 \Leftrightarrow C_n(\varphi{})=0)</tex>, где <tex>x</tex> - вход длины <tex>n</tex>
'''Что такое <tex>f(<x,y>)\inexists{SATz}</tex> - это значит, что для некоторого набора формул выполняется для всего набора, если предположить, что <tex>L=:\psi{x|\forall{y} C_n(f(<x,y>,z))=1\}</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> '''Что такое <tex>C_n</tex> Решает <tex>SAT</tex>?''' Запишем это используя квантор "<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} - набор логических схем для SAT и\forall{y} C_n(f(<x,y>))=1\}</tex>,где - <tex>C1,C2,..,Cn</tex> набор логических схем для <tex>SAT</tex>.
Внутри будем проверять используемый набор
Получаем что <math>L\in \Sigma_2</math>
Теорема доказана