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

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 5: Строка 5:
  
 
== Доказательство ==
 
== Доказательство ==
Пусть есть логические схемы для <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> и так далее.
+
Пусть есть логические схемы для <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 закодировано имеется разложение или нет.
+
Что значит разрешается логической схемой? Это значит что если на вход логической схеме подать каким-то логичным образом закодированную формулу, то на выходе получется логичным образом в виде 0 и 1 закодированный ответ - имеется разложение или нет.
  
 
И причем размер этой логической схемы не больше чем какой то полином от n. Но мы не утверждаем, что можем как то конструктивно их построить. Если бы мы могли за полином их построить, то это бы означало, что сат2=п2, что P=NP.
 
И причем размер этой логической схемы не больше чем какой то полином от n. Но мы не утверждаем, что можем как то конструктивно их построить. Если бы мы могли за полином их построить, то это бы означало, что сат2=п2, что P=NP.

Версия 13:06, 3 июня 2010

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

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

[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 закодированный ответ - имеется разложение или нет.

И причем размер этой логической схемы не больше чем какой то полином от 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]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] // Если Cn(фи)=0 то для любого x (для любого тут можем использовать) фи(х)=0 Если Cn(фи)=1 то либо фи(ч1=0) принадлежит сат либо фи(х1=1) принадлежит сат тут не N а длина фи Вот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далее. Это правильная проверка причем за полином

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

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

[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] И рекурсивно вызываемся от того из них которое равно 1. Ту же самую формулу но записываем от того из них которое равно 1 (это же предикат но для того из них фи при х1= для которого труе) Второй вариант был угадать не только будевы схемы для сат но и те которые выдают нам правильные значения


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