Теорема Бермана — Форчуна — различия между версиями
AndrewD (обсуждение | вклад) |
AndrewD (обсуждение | вклад) |
||
Строка 44: | Строка 44: | ||
Ответом будет <tex>check(\phi, 1)</tex>. | Ответом будет <tex>check(\phi, 1)</tex>. | ||
− | Так как <tex>TAUT \in coNPC</tex> и <tex>S \in coNPC</tex>, то <tex>TAUT \le S</tex>, то есть <tex>\exists f \in \widetilde{P} : \phi \in TAUT \Leftrightarrow f(\phi) \in S</tex>. Поэтому, если в предыдущей программе заменить все обращения к <tex>memo[\phi]</tex>, на <tex>memo[f(\phi)]</tex>, то полученная программа по прежнему будет разрешать <tex>TAUT</tex>. | + | Так как <tex>TAUT \in coNPC</tex> и <tex>S \in coNPC</tex>, то <tex>TAUT \le S</tex>, то есть <tex>\exists f \in \widetilde{P} : \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>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> {{---}} полином. |
Версия 23:42, 27 апреля 2012
Лемма (1): |
Доказательство: |
Пусть . Тогда и .Рассмотрим произвольный язык лемме). . Тогда . Так как , то , следовательно (поПолучили, что В обратную сторону доказательство аналогично. и . Значит . |
Определение: |
— булева формула . |
Лемма (2): |
Доказательство: |
, то есть . Тогда по лемме (1) . |
Определение: |
полином . |
Теорема (Махэни, light): |
Доказательство: |
Пусть существует . Разрешим за полином.Для начала напишем программу, разрешающую :if return if return 0 if return 1 return Ответом будет .Так как и , то , то есть . Поэтому, если в предыдущей программе заменить все обращения к , на , то полученная программа по-прежнему будет разрешать .Оценим необходимый размер . Можно считать, что , где , а — монотонно возрастающий полином. Тогда . Так как , то , где — полином. Можно считать, что монотонно возрастает. Тогда размер можно оценить сверху: , где — полином.if //(1) return if return 0 if return 1 //(2) if exit return Рассмотрим двоичное дерево, получающееся в результате рекурсивных вызовов данной программы. Рассмотрим произвольный элемент Итого, данная программа разрешает . Заметим, что условие в ходе выполнения программы является ложным при обращении к элементу не более одного раза. Так как всего в не более элементов, то суммарно за все время выполнения программы условие принимает ложное значение не более раз. Отсюда следует, что присваивание выполняется не более раз, а значит в дереве не более внутренних вершин. Значит всего в дереве не более вершин, то есть данная программа работает за полиномиальное время. за полиномиальное время. А так как , то , то есть , откуда . |