Изменения

Перейти к: навигация, поиск

Теорема Карпа-Липтона

639 байт убрано, 19:18, 4 сентября 2022
м
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>p</tex> - какой-то полином от <tex>n</tex>.
Не утверждается, что их можно как то конструктивно построить. Если бы их было возможно построить за полином, то это бы означало, что <tex>SAT_2=\Pi_2</tex> и '''Что значит <tex>P = NP</tex>."разрешается логической схемой"?'''
Итак, это означает, Это значит что если зафиксировать на вход логической схеме подать каким-то логичным образом закодированную формулу, то на выходе получется логичным образом в виде 0 и 1 закодированный ответ - имеется разложение или нет. И причем размер этой логической схемы <tex>|C_n|\le p(n) </tex>, для этого фиксированного <tex>nгде </tex> <tex>\exists{C_n}\forall{} формулы \varphi{} p(\varphi{} \in{} SAT |\varphi{}|=n \Leftrightarrow C_n(\varphi{})=1)</tex> - какой-то полином.
Здесь не утверждается, что эти логические схемы можно как-то конструктивно построить. Если бы их было возможно построить за полином, то это бы означало, что <tex> \exists{C_n} \forall{\varphi{}} (\forall{x} формулы длины n \varphi{(x)}SAT_2=0 \Leftrightarrow C_n(\varphi{})Pi_2</tex> и значит <tex>P =0)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>\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><x,y> L_1\subsetin{L1}NP</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>)\subset{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>NP</tex> входит в <tex>P/poly</tex> т.е.
<tex>L=\{x|\exists{C_n}: C_n решает SAT и \forall{y} C_n(f(<x,y>))=1\}</tex>
'''Что такое Cn <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} \forall{y} C_n(f(<x,y>))=1\}</tex>,где - <tex>C1,C2,..,Cn</tex> набор логических схем для <tex>SAT</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>.
Внутри будем проверять используемый набор
<mathtex>\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)</mathtex>// Если Cn(фи)=0 то для любого x (для любого тут можем использовать) фи(х)=0Если Cn(фи)=1 то либо фи(ч1=0) принадлежит сат либо фи(х1=1) принадлежит сат тут не N а длина фиВот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далее. Это правильная проверка причем за полином
Если <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.
<tex>C_{m-1}(\varphi{}|_{x_1=1})=0 \Rightarrow \varphi{}|_{x_1=0}(x_2)=0</tex>Второй вариант был угадать не только булевы схемы для сат но и те схемы, которые выдают правильные значения.
Получаем что <texmath>C_{m-1}(L\varphi{}|{x_1=0}) in \vee{} C_{m-1}(\varphi{}|_{x_1=1})Sigma_2</texmath> И рекурсивно вызываемся от того из них которое равно 1. Ту же самую формулу но записываем от того из них которое равно 1 (это же предикат но для того из них фи при х1= для которого труе)Второй вариант был угадать не только будевы схемы для сат но и те которые выдают нам правильные значения
Получаем что <math>L\in \Sigma_2</math>
Теорема доказана
1632
правки

Навигация