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

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 11: Строка 11:
  
 
<tex> \exists{C_n} \forall{\varphi{}} (\forall{x} формулы длины n \varphi{(x)}=0 \Leftrightarrow C_n(\varphi{})=0)</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>
 +
 +
 +
 +
 +
 +
 +
 +
 +
  
  
Строка 30: Строка 56:
 
Рассмотрим <tex>L_1 = \{<x,y>|\exists{z}: \psi{(x,y,z)}\}</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>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>)\in{SAT}</tex> - это значит, что для некоторого набора формул выполняется для всего набора, если предположить, что <tex>L=\{x|\forall{y} C_n(f(<x,y>))=1\}</tex>
 
  
 
Но надо откуда-то взять этот набор. Можно его угадать, используя квантор существует. Добавим его.
 
Но надо откуда-то взять этот набор. Можно его угадать, используя квантор существует. Добавим его.
Строка 45: Строка 66:
  
 
Что означает <tex>C_n</tex> решает <tex>SAT</tex>? Нужно переписать с квантором для любого.
 
Что означает <tex>C_n</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>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} - набор логических схем для SAT и\forall{y} C_n(f(<x,y>))=1\}</tex>

Версия 22:26, 2 июня 2010

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

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

[math]NP \subset P/poly[/math] то [math]\Sigma_2=\Pi_2[/math]

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

Пусть есть логические схемы для [math]NP[/math] (любой задаче из NP).Например зафиксируем любую из NP например пусть сат разрешает логическими схемами [math]SAT : C_1...C_n...[/math], сат который поддерживается с одним битом разрешается логической схемой с1 сат с двумя переменными логической схемой с2...Что значит разрешается? Это значит что логическая схема, в инпуте которой который каким то логичным образом закодирована формула, а на выходе логичным образом в вмде 0 и один закодировано есть ли доказательство(разложение) или нет. И причем размер этой логической схемы не больше чем какой то полином от n. Но мы не утверждаем, что можем как то конструктивно их построить. Если бы мы могли за полином их построить, то это бы означало, что сат2=п2, что P=NP. Итак, что это означает, рассмотрим, это означает на самом деле что для любого n (зафиксируем n)

Это означает что для фиксированного [math]n[/math] [math]\exists{}[/math] такая логическая схема [math]C_n[/math], что [math]\forall{} формулы \varphi{} (\varphi{} \in{} SAT |\varphi{}|=n \Leftrightarrow C_n(\varphi{})=1)[/math]

[math] \exists{C_n} \forall{\varphi{}} (\forall{x} формулы длины n \varphi{(x)}=0 \Leftrightarrow C_n(\varphi{})=0)[/math].

Рассмотрим язык [math]L\in \Pi_2[/math]. Это означает, что [math]x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}[/math] Что такое существует z что пси от х игрик z? Обозначим пары <x,y>, для которых такой z существует как какой нибудь язык L1 Рассмотрим [math]L_1 = \{\lt x,y\gt |\exists{z}: \psi{(x,y,z)}\}[/math]. Заметим что [math]L_1 \in NP[/math] по определению [math]NP[/math] Итого L это множество слов [math]L={x|\forall{y} \lt x,y\gt \in{L_1}}[/math] Нужно доказать что [math]L\in \Sigma_1[/math]

Что такое <x,y> \in L1 ? Если [math]L_1\in{} NP \Rightarrow тоL_1 \le{}_m SAT[/math] по карпу с помощью [math]f[/math], т.е. [math]L=\{x|\forall{y} f(\lt x,y\gt )\in{SAT}\}[/math]

Что такое f(<x,y>)\in SAT ? [math]f(\lt x,y\gt )\in{SAT}[/math] - это значит, что для некоторого набора булевых(логических) схем, выполнимость всего этого набора, если предположить, что набор этих схем нам известен то получится что [math]L=\{x|\forall{y} C_n(f(\lt x,y\gt ))=1\}[/math] где n- длина входа <x,y> Нам надо откуда то взять этот набор. Мы можем его угадать используя квантор существует снаружи. Cn он существует по предположению что NP входит в P/poly т.е. [math]L=\{x|\exists{C_n}: C_n решает SAT и \forall{y} C_n(f(\lt x,y\gt ))=1\}[/math]

Что такое Cn Решает SAT? Нам разрешается использовать только квантор для любого. [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]i[/math] символов, разрешимых логической схемой [math]C_i[/math]. Размер [math]|C_i|\le p(n)[/math].

Это означает что для фиксированного [math]n[/math] [math]\exists{}[/math] такая логическая схема [math]C_n[/math], что [math]\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]L\in \Pi_2[/math]. Это означает, что [math]x\in L \Leftrightarrow \forall{y} \exists{z}: \psi{(x,y,x)}[/math]

Рассмотрим [math]L_1 = \{\lt x,y\gt |\exists{z}: \psi{(x,y,z)}\}[/math]




Но надо откуда-то взять этот набор. Можно его угадать, используя квантор существует. Добавим его. Так как [math]NP \subset P/poly[/math] то [math]L=\{x|\exists{C_n}: C_n решает SAT и \forall{y} C_n(f(\lt x,y\gt ))=1\}[/math]

Что означает [math]C_n[/math] решает [math]SAT[/math]? Нужно переписать с квантором для любого.


Воспользуемся самосведением [math]SAT[/math]: [math]L=\{x|\exists{C1,C2,..,Cn} - набор логических схем для SAT и\forall{y} C_n(f(\lt x,y\gt ))=1\}[/math]

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

[math]\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)[/math]

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

[math] \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[/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]

Получаем что [math]L\in \Sigma_2[/math] Теорема доказана