70
правок
Изменения
Нет описания правки
|proof=Пусть <tex>L \in coNPC</tex>. Тогда <tex>L \in coNP</tex> и <tex>\overline L \in NP</tex>.
Рассмотрим произвольный язык <tex>L_1 \in NP</tex>. Тогда <tex>\overline {L_1} \in coNP</tex>. Так как <tex>L \in coNPC</tex>, то <tex>\overline {L_1} \le_f le L</tex>, следовательно <tex>L_1 \le_f le \overline L</tex>.
Получили, что <tex>\overline L \in NP</tex> и <tex>\forall L_1 \in NP \, L_1 \le_f le \overline L</tex>. Значит <tex>\overline L \in NPC</tex>.
В обратную сторону доказательство аналогично.
}}
<tex>memo[\phi] \leftarrow check(\phi|_{x_i=0}, i+1)\, \&\&\, check(\phi|_{x_i=1}, i+1)</tex>
'''return''' <tex>memo[\phi]</tex>
Ответом будет <tex>check(\phi, 1)</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>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>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>
'''return''' <tex>memo[f(\phi)]</tex>
}}
