70
правок
Изменения
Нет описания правки
|about=light
|statement=<tex>coNPC \cap SPARSE = \varnothing \Rightarrow P = NP</tex>
|proof=Пусть существует <tex>S \in coNPC \cap SPARSE</tex>. Решим Разрешим <tex>TAUT</tex> за полином. Для начала напишем программу, разрешающую <tex>TAUT</tex>:
<tex>check(\phi, i)</tex>
'''if''' <tex>memo[\phi] \ne -1</tex>
'''return''' <tex>memo[\phi]</tex>
'''if''' <tex>\phi=0</tex>
'''return''' 0
'''return''' 1
<tex>memo[\phi] \leftarrow check(\phi|_{x_i=0}, i+1)\, \&\&\, check(\phi|_{x_i=1}, i+1)</tex>
'''return''' <tex>memo[\phi]</tex> blablablaОтветом будет <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>check(\phi, i)</tex>
