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

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
(не показано 47 промежуточных версий 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>
  
 
== Доказательство ==
 
== Доказательство ==
Пусть есть логические схемы для <tex>NP</tex> (любой задаче из NP).Например зафиксируем любую из NP например пусть сат разрешает логическими схемами <tex>SAT : C_1...C_n...</tex>, сат  который поддерживается с одним битом разрешается логической схемой с1 сат с двумя переменными логической схемой с2...Что значит разрешается? Это значит что логическая схема, в инпуте которой который каким то логичным образом закодирована формула, а на выходе логичным образом в вмде 0 и один закодировано есть ли доказательство(разложение) или нет. И причем размер этой логической схемы не больше чем какой то полином от n. Но мы не утверждаем, что можем как то конструктивно их построить. Если бы мы могли за полином их построить, то это бы означало, что сат2=п2, что P=NP.
+
Пусть есть логические схемы для <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> и т.д.).
Итак, что это означает, рассмотрим, это означает на самом деле что для любого n (зафиксируем n)
 
 
 
Это означает что для фиксированного <tex>n</tex> <tex>\exists{}</tex> такая логическая схема <tex>C_n</tex>, что <tex>\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>L\in \Pi_2</tex>. Это означает, что <tex>x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}</tex>
 
Что такое существует 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>
 
 
 
Что такое f(<x,y>)\in SAT ?
 
<tex>f(<x,y>)\in{SAT}</tex> - это значит, что для некоторого набора булевых(логических) схем, выполнимость всего этого набора, если предположить, что набор этих схем нам известен то получится что <tex>L=\{x|\forall{y} C_n(f(<x,y>))=1\}</tex> где n- длина входа <x,y>
 
Нам надо откуда то взять этот набор. Мы можем его угадать используя квантор существует снаружи.
 
Cn он существует по предположению что NP входит в P/poly т.е.
 
<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>\Leftrightarrow</tex> если <tex>\forall{\varphi} \forall{x}  (fi(x)=1 \Rightarrow C_n(fi)=1)</tex>
 
 
 
 
 
 
 
 
 
 
 
  
  
 +
'''Что значит "разрешается логической схемой"?'''
  
 +
Это значит что если на вход логической схеме подать каким-то логичным образом закодированную формулу, то на выходе получется логичным образом в виде 0 и 1 закодированный ответ - имеется разложение или нет. И причем размер этой логической схемы <tex>|C_n|\le p(n) </tex>, где <tex>p(n)</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} \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>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>i</tex> символов, разрешимых логической схемой <tex>C_i</tex>. Размер <tex>|C_i|\le p(n)</tex>.
 
Это означает что для фиксированного <tex>n</tex> <tex>\exists{}</tex> такая логическая схема <tex>C_n</tex>, что <tex>\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>L\in \Sigma_1</tex>'''
  
Рассмотрим язык <tex>L\in \Pi_2</tex>. Это означает, что <tex>x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}</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>L_1 = \{<x,y>|\exists{z}: \psi{(x,y,z)}\}</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>NP \subset 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> решает <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>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>\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>
  
<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>
+
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, то зафиксируем формулу <tex>\varphi{}_0</tex>, которую он не решает. Если на этой формуле выдаст 0, а должна выдать 1, то получается что не удовлетворяет первую часть предыдущего выражения и, значит, не будет работать. Если наоборот выдаст 1 а на самом деле формула не удавлетворима то обе скобки не выполнятся и опять формула работать не будет.
  
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо, если нет то зафиксируем формулу на которой не решает. Если выдаст 0 а должна выдать 1 то первую не удолветворяет, если наоборот то обе не удовлетворяет.
+
Рассмотрим минимальную неправильную схему. Тогда на той формуле, на которой эта схема неправильна, по предположению, что все более короткие формулы правильны,эта формула распознается схемами с меньшим числом входов. Поэтому  обе скобки будут 0 и мы не узнаем набор схем. Развернем формулу до конца.
  
<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> \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>
+
Второй вариант был угадать не только булевы схемы для сат но и те схемы, которые выдают правильные значения.
  
<tex>C_{m-1}(\varphi{}|{x_1=0}) \vee{} C_{m-1}(\varphi{}|_{x_1=1})</tex>
+
Получаем что <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]

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