Теорема Бермана — Форчуна — различия между версиями
AndrewD (обсуждение | вклад) |
Kirelagin (обсуждение | вклад) |
||
Строка 45: | Строка 45: | ||
Так как <tex>\mathrm{TAUT} \in \mathrm{coNPC}</tex> и <tex>S \in \mathrm{coNPC}</tex>, то <tex>\mathrm{TAUT} \le S</tex>, то есть <tex>\exists f \in \mathrm{\widetilde{P}} : \phi \in \mathrm{TAUT} \Leftrightarrow f(\phi) \in S</tex>. Поэтому, если в предыдущей программе заменить все обращения к <tex>memo[\phi]</tex>, на <tex>memo[f(\phi)]</tex>, то полученная программа по-прежнему будет разрешать <tex>\mathrm{TAUT}</tex>. | Так как <tex>\mathrm{TAUT} \in \mathrm{coNPC}</tex> и <tex>S \in \mathrm{coNPC}</tex>, то <tex>\mathrm{TAUT} \le S</tex>, то есть <tex>\exists f \in \mathrm{\widetilde{P}} : \phi \in \mathrm{TAUT} \Leftrightarrow f(\phi) \in S</tex>. Поэтому, если в предыдущей программе заменить все обращения к <tex>memo[\phi]</tex>, на <tex>memo[f(\phi)]</tex>, то полученная программа по-прежнему будет разрешать <tex>\mathrm{TAUT}</tex>. | ||
− | Оценим необходимый размер <tex>memo</tex>. Можно считать, что <tex>\mathrm{T}(f, \phi) \le q(n)</tex>, где <tex>n = |\phi|</tex>, а <tex>q</tex> {{---}} монотонно возрастающий полином. Тогда <tex>|f(\phi)| \le q(n)</tex>. Так как <tex>S \in \mathrm{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>memo</tex>. Можно считать, что <tex>\mathrm{T}(f, \phi) \le q(n)</tex>, где <tex>n = |\phi|</tex>, а <tex>q</tex> {{---}} монотонно возрастающий полином. Тогда <tex>|f(\phi)| \le q(n)</tex>. Так как <tex>S \in \mathrm{SPARSE}</tex>, то <tex>|S \cap \Sigma^k| \le p(k)</tex>, где <tex>p</tex> {{---}} полином. Можно считать, что <tex>p</tex> монотонно возрастает. Тогда размер <tex>memo</tex> (число слов длины не более <tex>q(n)</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>: | <tex>check(\phi, i)</tex>: | ||
'''if''' <tex>\phi=0</tex> | '''if''' <tex>\phi=0</tex> |
Версия 11:06, 3 июня 2012
Лемма (1): |
Язык является -полным тогда и только тогда, когда является -полным. |
Доказательство: |
Пусть — -полный. Тогда и .Рассмотрим произвольный язык лемме). . Тогда . Так как — -полный, то , следовательно (поПолучили, что В обратную сторону доказательство аналогично. и . Значит . |
Определение: |
— булева формула . |
Лемма (2): |
. |
Доказательство: |
, то есть . Кроме того, в качестве сертификата используется , на котором . Значит . Тогда по лемме (1) . |
Определение: |
полином . |
Теорема (Берман, Форчун): |
. |
Доказательство: |
Пусть существует . Разрешим за полином.Для начала напишем программу, разрешающую :: if return 0 if return 1 if return return Ответом будет .Так как и , то , то есть . Поэтому, если в предыдущей программе заменить все обращения к , на , то полученная программа по-прежнему будет разрешать .Оценим необходимый размер . Можно считать, что , где , а — монотонно возрастающий полином. Тогда . Так как , то , где — полином. Можно считать, что монотонно возрастает. Тогда размер (число слов длины не более в языке) можно оценить сверху: , где — полином.: if return 0 if return 1 if //(1) return //(2) if exit return Рассмотрим двоичное дерево, получающееся в результате рекурсивных вызовов данной программы. Рассмотрим произвольный элемент Итого, данная программа разрешает . Заметим, что условие в ходе выполнения программы является ложным при обращении к элементу не более одного раза. Так как всего в не более элементов, то суммарно за все время выполнения программы условие принимает ложное значение не более раз. Отсюда следует, что присваивание выполняется не более раз, а значит в дереве не более внутренних вершин. Значит всего в дереве не более вершин, то есть данная программа работает за полиномиальное время. за полиномиальное время. А так как , то , то есть , откуда . |