Теорема Карпа-Липтона — различия между версиями
(→Доказательство) |
(→Доказательство) |
||
Строка 36: | Строка 36: | ||
<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>\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> то все хорошо, если нет то зафиксируем формулу на которой не решает. Если выдаст 0 а должна выдать 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}(x2)=0</tex> | ||
+ | |||
C_m-1(fi|_x1=1)=0 =>fi|_x1=0(x2)=0 | C_m-1(fi|_x1=1)=0 =>fi|_x1=0(x2)=0 | ||
C_m-1(fi|x1=0) галочка C_m-1(fi|x1=1) | C_m-1(fi|x1=0) галочка C_m-1(fi|x1=1) |
Версия 15:11, 15 апреля 2010
Формулировка
Теорема Карпа-Липтона
то
Доказательство
Пусть есть логические схемы для
. Например который кодирует символов, разрешимых логической схемой . Размер . Это означает что для фиксированного такая логическая схема , что.
Рассмотрим язык
. Это означает, чтоРассмотрим
по определению
Нужно доказать что
по карпу с помощью , т.е.
- это значит, что для некоторого набора формул выполняется для всего набора, если предположить, что
Но надо откуда-то взять этот набор. Можно его угадать, используя квантор существует. Добавим его. Так как
тоЧто означает
решает ? Нужно переписать с квантором для любого. решаетВоспользуемся самосведением
:Внутри будем проверять используемый набор
Если
решает то все хорошо, если нет то зафиксируем формулу на которой не решает. Если выдаст 0 а должна выдать 1 то первую не удолветворяет, если наоборот то обе не удовлетворяет.
C_m-1(fi|_x1=1)=0 =>fi|_x1=0(x2)=0 C_m-1(fi|x1=0) галочка C_m-1(fi|x1=1)
Получаем что
Теорема доказана