211
правок
Изменения
м
Введём понятие арифметизации булевых формул. Пусть нам дана формула <tex>\phi(x_1 \ldots x_m)</tex>. Сделаем следующие преобразования и получим формулу <tex>A_\phi(x_1, x_2, \ldots, x_m)</tex>:
# <tex> x_i \to x_i</tex>;
# <tex> \lnot x \to 1 - x</tex>;
# <tex>\Phi \land \Psi \to A_\Phi \cdot A_\Psi</tex>;
# <tex>\Phi \lor \Psi \to 1 - (1 - A_\Phi) \cdot (1 - A_\Psi)</tex>.
Заметим, что длина формулы при этом возрастёт не более, чем в константу раз.
|statement=<tex>\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)</tex>.
|proof=
}}
{{Лемма
|about=2
Нет описания правки
}}
{{Лемма
|about=1
|statement=<tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phi(x_1, \ldots, x_m)=k \iff \langle\phi,k\rangle \in \#SAT</tex>.
|proof=Следует из [[Арифметизация булевых формул с кванторами | леммы (1)]].
}}
{{Лемма
|about=32
|statement=<tex>\#SAT \in \mathrm{IP}</tex>.
|proof=
Для доказательства леммы построим программы ''Verifier'' и ''Prover'' из [[Интерактивные протоколы. Класс IP. Класс AM#Класс IP|определения ]] класса <tex>\mathrm{IP}</tex>.
Сперва арифметизуем формулу <tex>\phi</tex>. Пусть полученный полином <tex>A(x_1, x_2, ..., x_m)</tex> имеет степень <tex>d</tex>.
По лемме (21) вместо условия <tex>\langle \phi, k \rangle \in \#SAT</tex>, можно проверять условие <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phi(x_1, \ldots, x_m)=k</tex>.
Приступим к описанию ''Verifier'''а.
{{Лемма
|about=43
|statement=<tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.
|proof=
Очевидно, что <tex>\phi \in TAUT \iff \langle \phi, 2^k \rangle \in \#SAT</tex>.
По лемме (32) <tex>\#SAT \in \mathrm{IP}</tex>. Тогда <tex>TAUT \in \mathrm{IP}</tex>. Так как <tex>TAUT \in \mathrm{coNPC}</tex>, то <tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.
}}
[[Категория: Теория сложности]]
