1632
правки
Изменения
м
Что значит разрешается? Это значит что логическая схема, на вход которой который подается каким то логичным образом закодированная формула, а на выходе получается логичным образом в виде 0 и 1 закодировано имеется разложение или нет.
И причем размер этой '''Что значит "разрешается логической схемы не больше чем какой то полином от n. Но мы не утверждаем, что можем как то конструктивно их построить. Если бы мы могли за полином их построить, то это бы означало, что сат2=п2, что P=NP.Итак, что это означает, рассмотрим, это означает на самом деле что для любого n (зафиксируем n)схемой"?'''
Что такое существует z что пси от х игрик z? Обозначим пары <x,y>, для которых такой z существует как какой нибудь язык L1 Рассмотрим <tex>L_1 = \{<x,y>|\exists{z}: \psi{(x,y,z)}\}</tex>. Заметим что <tex>L_1 \in NP</tex> по определению <tex>NP</tex>
Итого L это множество слов <tex>L={x|\forall{y} <x,y>\in{L_1}}</tex>
Нужно доказать что <tex>L\in \Sigma_1</tex>
Что такое <x,y> \in L1 ?
Если <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>
Что такое Cn Решает SAT? Нам разрешается использовать только квантор для любого.
<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>L\in \Sigma_1</tex>''' Если <tex>L_1\in{} NP</tex> то <tex>L_1 \le{}_m SAT</tex>: с помощью <tex>f</tex>, т.е. <tex>L=\{x|\existsforall{C1y} f(<x,C2y>)\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,Cny>))=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>C\forall{\varphi{}} (C_{|\varphi{}|}(\varphi{})=0 \Rightarrow \forall{x} \varphi{}(x)=0)\vee{}</tex> решает <tex>(C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SATили \varphi{}|_{x_1=1} \in SAT)</tex> то все хорошо, если нет то зафиксируем формулу которую он не решает. Если выдаст 0 а должна выдать 1 то вот эту первую часть не удолветворяет и тут не будет работать, если наоборот выдаст 1 а на самом деле формула не удавлетворима то ни эта ни эта не будет работать
Рассмотрим минимальную схему которая неправильнаЕсли <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, то зафиксируем формулу <tex>\varphi{}_0</tex>, тогда которую он не решает. Если на той этой формулевыдаст 0, на которой эта схема неправильна по предположению а должна выдать 1, то получается что все более короткие формулы правильныне удовлетворяет первую часть предыдущего выражения и,эта распознается схемами с меньшим числом входовзначит, поэтому и эта и эта будут 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=0}) \vee{} C_{m-1}(\varphi{}|_{x_1=1})</tex> И рекурсивно вызываемся от того из них которое равно 1. Ту же самую формулу но записываем от того из них которое равно 1 (это же предикат но для того из них фи при х1= для которого труе)Второй вариант был угадать не только будевы булевы схемы для сат но и те схемы, которые выдают нам правильные значения .
rollbackEdits.php mass rollback
'''Теорема Карпа-Липтона'''
Если <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>\exists{}</tex> такая логическая схема <tex>C_n) </tex>, что где <tex>\forall{} формулы \varphi{} p(\varphi{} \in{} SAT |\varphi{}|=n \Leftrightarrow C_n(\varphi{})=1)</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} формулы длины n \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>
'''Что такое f<tex>\exists{z}:\psi{(<x,y,z)}</tex>)\in SAT ?''' ---- Обозначим пары <tex>f(<x,y>)\in{SAT}</tex> - это значит, что для некоторого набора булевых(логических) схем, выполнимость всего этого набора, если предположить, что набор этих схем нам известен то получится что которых такой <tex>z</tex> существует как какой нибудь язык <tex>L_1</tex>. <tex>LL_1 =\{<x,y>|\forallexists{yz} C_n: \psi{(f(<x,y>,z))=1}\}</tex> где n- длина входа . Заметим что <tex>L_1 \in NP</tex> по определению <tex>NP<x,y/tex>Нам надо откуда то взять этот набор. Мы можем его угадать используя квантор существует снаружи.Cn он существует по предположению Таким образом получается, что NP входит в P/poly т.е. <tex>L=\{x|\exists{C_n}: C_n решает SAT и \forall{y} C_n(f(<x,y>))=1\in{L_1}\}</tex> ----
Воспользуемся самосведением <tex>SAT</tex>: <tex>L=\forall{\varphi{}} (C_{x|\varphiexists{C1,C2,..,Cn}|}(\varphi{})=0 \Rightarrow \forall{xy} \varphiC_n(f(<x,y>)=0) (C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)</tex>,где - <tex>C1,C2,..,Cn</tex> набор логических схем для <tex>SAT</ Если Cn(фи)=0 то для любого x (для любого тут можем использовать) фи(х)=0Если Cn(фи)=1 то либо фи(ч1=0) принадлежит сат либо фи(х1=1) принадлежит сат тут не N а длина фиВот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далееtex>. Это правильная проверка причем за полином
<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>
Теорема доказана