Теорема Карпа-Липтона — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
(не показана 21 промежуточная версия 3 участников)
Строка 2: Строка 2:
 
'''Теорема Карпа-Липтона'''  
 
'''Теорема Карпа-Липтона'''  
  
<math>NP \subset P/poly</math> то <math>\Sigma_2=\Pi_2</math>
+
Если <math>NP \subset P/poly</math> то <math>\Sigma_2=\Pi_2</math>
  
 
== Доказательство ==
 
== Доказательство ==
Строка 20: Строка 20:
 
Рассмотрим язык <tex>L\in \Pi_2</tex>. Это означает, что <tex>x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}</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>\exists{z}:\psi{(x,y,z)}</tex>?'''
 +
 
 +
----
  
 
Обозначим пары <tex><x,y></tex>, для которых такой <tex>z</tex> существует как какой нибудь язык <tex>L_1</tex>.
 
Обозначим пары <tex><x,y></tex>, для которых такой <tex>z</tex> существует как какой нибудь язык <tex>L_1</tex>.
Строка 27: Строка 30:
 
Заметим что <tex>L_1 \in NP</tex> по определению <tex>NP</tex>
 
Заметим что <tex>L_1 \in NP</tex> по определению <tex>NP</tex>
  
Итого
+
Таким образом получается, что
 
  <tex>L=\{x|\forall{y} <x,y>\in{L_1}\}</tex>
 
  <tex>L=\{x|\forall{y} <x,y>\in{L_1}\}</tex>
  
Требуется доказать, что <tex>L\in \Sigma_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><x,y> \subset{L_1}</tex>?'''
 
  
Если <tex>L_1\in{} NP</tex> то <tex>\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>f(<x,y>)\subset{SAT}</tex> - для некоторого набора логических схем это означает выполнимость всего этого набора. Если предположить, что набор этих схем нам известен то получится что <tex>L=\{x|\forall{y} C_n(f(<x,y>))=1\}</tex> где <tex>n</tex>- длина входа <tex><x,y></tex>.
 
 
Требуется откуда то взять этот набор. Его можно угадать, используя квантор "<tex>\exists{}</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 Решает SAT?'''  
+
'''Что такое <tex>C_n</tex> Решает <tex>SAT</tex>?'''  
  
 
Запишем это используя квантор "<tex>\forall{}</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>C_n</tex> решает <tex>SAT</tex> <tex>\Leftrightarrow</tex> если <tex>\forall{\varphi} \forall{x} (fi(x)=1 \Rightarrow C_n(fi)=1)</tex>
Внутри будем проверять используемый набор
 
<tex>\forall{\varphi{}} (C_{|\varphi{}|}(\varphi{})=0 \Rightarrow \forall{x} \varphi(x)=0) (C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)</tex>
 
  
// Если Cn(фи)=0 то для любого x (для любого тут можем использовать) фи(х)=0
+
Воспользуемся самосведением <tex>SAT</tex>:
Если Cn(фи)=1 то либо фи(ч1=0) принадлежит сат либо фи(х1=1) принадлежит сат тут не N а длина фи
+
<tex>L=\{x|\exists{C1,C2,..,Cn} \forall{y} C_n(f(<x,y>))=1\}</tex>,
Вот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далее. Это правильная проверка причем за полином
+
где - <tex>C1,C2,..,Cn</tex> набор логических схем для <tex>SAT</tex>.
  
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо, если нет то зафиксируем формулу которую он не решает. Если выдаст 0 а должна выдать 1 то вот эту первую часть не удолветворяет и тут не будет работать, если наоборот выдаст 1 а на самом деле формула не удавлетворима то ни эта ни эта не будет работать
+
Внутри будем проверять используемый набор
 +
<tex>\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 и мы не узнаем набор схем. Можно попробовать развернуть формулу до конца. Видимо это будет выглядеть так
+
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, то зафиксируем формулу <tex>\varphi{}_0</tex>, которую он не решает. Если на этой формуле выдаст 0, а должна выдать 1, то получается что не удовлетворяет первую часть предыдущего выражения и, значит, не будет работать. Если наоборот выдаст 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>
+
Рассмотрим минимальную неправильную схему. Тогда на той формуле, на которой эта схема неправильна, по предположению, что все более короткие формулы правильны,эта формула распознается схемами с меньшим числом входов. Поэтому  обе скобки будут 0 и мы не узнаем набор схем. Развернем формулу до конца.
  
<tex>C_{m-1}(\varphi{}|_{x_1=1})=0 \Rightarrow \varphi{}|_{x_1=0}(x_2)=0</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.
  
<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>
 
Получаем что <math>L\in \Sigma_2</math>
 +
 
Теорема доказана
 
Теорема доказана

Текущая версия на 19:18, 4 сентября 2022

Формулировка

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

Если [math]NP \subset P/poly[/math] то [math]\Sigma_2=\Pi_2[/math]

Доказательство

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


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

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

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

Итак, получается, что если зафиксировать [math]n[/math], то для этого фиксированного [math]n[/math] будет

[math]\exists{C_n}\forall{} формулы \varphi{} (\varphi{} \in{} SAT  |\varphi{}|=n \Leftrightarrow C_n(\varphi{})=1)[/math] 
[math] \exists{C_n} \forall{\varphi{}} (\forall{x} \varphi{(x)}=0 \Leftrightarrow C_n(\varphi{})=0)[/math], где [math]x[/math] - вход длины [math]n[/math]

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


Что такое [math]\exists{z}:\psi{(x,y,z)}[/math]?


Обозначим пары [math]\lt x,y\gt [/math], для которых такой [math]z[/math] существует как какой нибудь язык [math]L_1[/math].

[math]L_1 = \{\lt x,y\gt |\exists{z}: \psi{(x,y,z)}\}[/math].

Заметим что [math]L_1 \in NP[/math] по определению [math]NP[/math]

Таким образом получается, что

[math]L=\{x|\forall{y} \lt x,y\gt \in{L_1}\}[/math]


Требуется доказать, что [math]L\in \Sigma_1[/math]

Если [math]L_1\in{} NP[/math] то [math]L_1 \le{}_m SAT[/math] с помощью [math]f[/math], т.е.

[math]L=\{x|\forall{y} f(\lt x,y\gt )\in{SAT}\}[/math]


Что такое "[math]f(\lt x,y\gt )\subset{SAT}[/math]"?

[math]f(\lt x,y\gt )\subset{SAT}[/math] [math]--[/math] для некоторого набора логических схем это означает выполнимость всего этого набора. Если предположить, что набор этих схем известен, то получится, что

[math]L=\{x|\forall{y} C_n(f(\lt x,y\gt ))=1\}[/math],

где [math]n[/math]- длина входа [math]\lt x,y\gt [/math].

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

[math]C_n[/math] существует по предположению, что [math]NP \subset{P/poly}[/math] т.е.

[math]L=\{x|\exists{C_n}: C_n[/math] решает [math]SAT[/math] и [math]\forall{y} C_n(f(\lt x,y\gt ))=1\}[/math]


Что такое [math]C_n[/math] Решает [math]SAT[/math]?

Запишем это используя квантор "[math]\forall{}[/math]".

[math]C_n[/math] решает [math]SAT[/math] [math]\Leftrightarrow[/math] если [math]\forall{\varphi} \forall{x}  (fi(x)=1 \Rightarrow C_n(fi)=1)[/math]

Воспользуемся самосведением [math]SAT[/math]:

[math]L=\{x|\exists{C1,C2,..,Cn} \forall{y} C_n(f(\lt x,y\gt ))=1\}[/math],

где - [math]C1,C2,..,Cn[/math] набор логических схем для [math]SAT[/math].

Внутри будем проверять используемый набор

[math]\forall{\varphi{}} (C_{|\varphi{}|}(\varphi{})=0 \Rightarrow \forall{x}  \varphi{}(x)=0)
\vee{}[/math]
   [math](C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)[/math]

Если [math]C[/math] решает [math]SAT[/math] то все хорошо. Если нет, то зафиксируем формулу [math]\varphi{}_0[/math], которую он не решает. Если на этой формуле выдаст 0, а должна выдать 1, то получается что не удовлетворяет первую часть предыдущего выражения и, значит, не будет работать. Если наоборот выдаст 1 а на самом деле формула не удавлетворима то обе скобки не выполнятся и опять формула работать не будет.

Рассмотрим минимальную неправильную схему. Тогда на той формуле, на которой эта схема неправильна, по предположению, что все более короткие формулы правильны,эта формула распознается схемами с меньшим числом входов. Поэтому обе скобки будут 0 и мы не узнаем набор схем. Развернем формулу до конца.

[math] \forall{\varphi{}}: |\varphi{}|=m \forall{x_1}..\forall{x_m} [/math][math] C_m(\varphi{})=0 \Rightarrow \varphi{(x_1)}=0[/math]
иначе [math] C_{m-1}(\varphi|_{x_1=0})=0 \Rightarrow \varphi|_{x_1=0}(x_2)=0[/math]
[math]C_{m-1}(\varphi{}|_{x_1=1})=0 \Rightarrow \varphi{}|_{x_1=0}(x_2)=0[/math]
[math]C_{m-1}(\varphi{}|{x_1=0}) \vee{} C_{m-1}(\varphi{}|_{x_1=1})[/math] 

Далее рекурсивно записываем ту же самую формулу от того из них, которое равно 1.

Второй вариант был угадать не только булевы схемы для сат но и те схемы, которые выдают правильные значения.

Получаем что [math]L\in \Sigma_2[/math]

Теорема доказана