Теорема Карпа-Липтона — различия между версиями
Строка 5: | Строка 5: | ||
== Доказательство == | == Доказательство == | ||
− | Пусть есть логические схемы для <tex>NP</tex> (любой задаче из NP).Например зафиксируем любую из NP например пусть сат разрешает логическими схемами <tex>SAT : C_1...C_n...</tex>, сат который | + | Пусть есть логические схемы для <tex>NP</tex> (любой задаче из NP).Например зафиксируем любую из NP например пусть сат разрешает логическими схемами <tex>SAT : C_1...C_n...</tex>, сат который поддерживается с одним битом разрешается логической схемой с1 сат с двумя переменными логической схемой с2...Что значит разрешается? Это значит что логическая схема, в инпуте которой который каким то логичным образом закодирована формула, а на выходе логичным образом в вмде 0 и один закодировано есть ли доказательство(разложение) или нет. И причем размер этой логической схемы не больше чем какой то полином от n. Но мы не утверждаем, что можем как то конструктивно их построить. Если бы мы могли за полином их построить, то это бы означало, что сат2=п2, что P=NP. |
+ | Итак, что это означает, рассмотрим, это означает на самом деле что для любого 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>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>n</tex> <tex>\exists{}</tex> такая логическая схема <tex>C_n</tex>, что <tex>\forall{}\varphi{} (\varphi{} \in{} SAT |\varphi{}|=n \Leftrightarrow C_n(\varphi{})=1)</tex> | ||
Версия 21:57, 2 июня 2010
Формулировка
Теорема Карпа-Липтона
то
Доказательство
Пусть есть логические схемы для
(любой задаче из NP).Например зафиксируем любую из NP например пусть сат разрешает логическими схемами , сат который поддерживается с одним битом разрешается логической схемой с1 сат с двумя переменными логической схемой с2...Что значит разрешается? Это значит что логическая схема, в инпуте которой который каким то логичным образом закодирована формула, а на выходе логичным образом в вмде 0 и один закодировано есть ли доказательство(разложение) или нет. И причем размер этой логической схемы не больше чем какой то полином от n. Но мы не утверждаем, что можем как то конструктивно их построить. Если бы мы могли за полином их построить, то это бы означало, что сат2=п2, что P=NP. Итак, что это означает, рассмотрим, это означает на самом деле что для любого n (зафиксируем n)Это означает что для фиксированного
такая логическая схема , что.
кодируетсимволов, разрешимых логической схемой . Размер .
Это означает что для фиксированного
такая логическая схема , что.
Рассмотрим язык
. Это означает, чтоРассмотрим
по определению
Нужно доказать что
по карпу с помощью , т.е.
- это значит, что для некоторого набора формул выполняется для всего набора, если предположить, что
Но надо откуда-то взять этот набор. Можно его угадать, используя квантор существует. Добавим его. Так как
тоЧто означает
решает ? Нужно переписать с квантором для любого. решаетВоспользуемся самосведением
:Внутри будем проверять используемый набор
Если
решает то все хорошо, если нет то зафиксируем формулу на которой не решает. Если выдаст 0 а должна выдать 1 то первую не удолветворяет, если наоборот то обе не удовлетворяет.
Получаем что
Теорема доказана