Изменения

Перейти к: навигация, поиск

Теорема Бермана — Форчуна

877 байт убрано, 14:55, 27 апреля 2012
Нет описания правки
{{Определение
|definition=
<tex>TAUT = \{\phi </tex> {{---}} булева формула <tex>| \forall x \, \phi(x)=1\}</tex>.
}}
|about=2
|statement=<tex>TAUT \in coNPC</tex>
|proof=<tex>\overline {TAUT} = \{\phi | \exists x : \phi(x) \ne 1\} = \{\phi | \overline {\phi} \in SAT\}</tex>, то есть <tex>\overline {TAUT} \in NPC</tex>. Тогда по лемме (1 ) <tex>TAUT \in coNPC</tex>.
}}
Так как <tex>TAUT \in coNPC</tex> и <tex>S \in coNPC</tex>, то <tex>TAUT \le_f S</tex>, то есть <tex>\phi \in TAUT \Leftrightarrow f(\phi) \in S</tex>. Поэтому, если в предыдущей программе заменить все обращения к <tex>memo[\phi]</tex>, на <tex>memo[f(\phi)]</tex>, то полученная программа по прежнему будет разрешать <tex>TAUT</tex>.
Оценим необходимый размер <tex>memo</tex>. Можно считать, что <tex>T(f(\phi)) \le q(n)</tex>, где <tex>n = |\phi|</tex>, а <tex>q</tex> {{---}} монотонно возрастающий полином. Тогда <tex>|f(\phi)| \le q(n)</tex>. Так как <tex>S \in SPARSE</tex>, то <tex>|S \cap \Sigma^k| \le p(k)</tex>, где <tex>p</tex> {{---}} полином. Можно считать, что <tex>p</tex> монотонно возрастает. Тогда размер <tex>memo</tex> можно оценить сверху: <tex>memo.size() \le \sum\limits_{i=0}^{q(n)}p(i) \le (1+q(n)) \cdot p(q(n)) \le r(n)</tex>, где <tex>r(n)</tex> {{---}} полином.
<tex>check(\phi, i)</tex>
'''if''' <tex>memo[f(\phi)] \ne -1</tex> //(1)
Рассмотрим двоичное дерево, получающееся в результате рекурсивных вызовов данной программы.
Рассмотрим произвольный элемент <tex>memo[i]</tex>. НайдемЗаметим, сколько раз что условие <tex>(1)</tex> в ходе выполнения программы является ложным при обращении к элементу <tex>memo[i]</tex>. Найдем в дереве такой узел, в котором есть обращение к <tex>memo[i]</tex>, а в его поддереве обращений к этому элементу нет, причем <tex>memo[i] = -1</tex>. До этого момента количество обращений к <tex>memo[i]</tex> не превышает глубины найденного узла, что не превосходит высоты дерева, что не превосходит некоторого полинома <tex>p'(n)</tex>. После этого момента условие <tex>(1)</tex> будет принимать истинное значение при обращении к <tex>memo[i]</tex>. Значит, в ходе выполнения программы условие <tex>(1)</tex> является ложным при обращении к <tex>memo[i]</tex> не более <tex>p'(n)</tex> разодного раза. Так как всего в <tex>memo</tex> не более <tex>r(n)</tex> элементов, то суммарно за все время выполнения программы условие <tex>(1)</tex> принимает ложное значение не более <tex>p''(n) = r(n) \cdot p'(n)</tex> раз, то есть <tex>p''</tex> {{---}} полином. Отсюда следует, что присваивание <tex>(2)</tex> выполняется не более <tex>p''r(n)</tex> раз, а значит в дереве не более <tex>p''r(n)</tex> внутренних вершин. Значит всего в дереве не более <tex>2 \cdot p''r(n) + 1</tex> вершин, то есть данная программа работает за полиномиальное время.
Итого, данная программа разрешает <tex>TAUT</tex> за полиномиальное время. Значит <tex>P=coNP</tex>, откуда <tex>P=NP</tex>.
}}
70
правок

Навигация