211
правок
Изменения
м
Нет описания правки
}}
Введём понятие арифмитизации арифметизации булевых формул. Пусть нам дана формула <tex>\phi(x_1 \ldots x_n)</tex>. Сделаем следующие преобразования и получим формулу <tex>A_\phi(x_1, x_2, \ldots, x_n)</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>.
Заметим, что длина формулы при этом возрастёт не более, чем в константу раз.
{{Лемма
{{Лемма
|about=2
|statement=<tex>\sum\limits_{x_1,= 0}^1 \ldots, \sum\limits_{x_n= 0} ^1 A_\phi(x_1, \ldots, x_n)=k \iff \langle\phi,k\rangle \in \#SAT</tex>.
|proof=Следует из леммы (1).
}}
|statement=<tex>\#SAT \in \mathrm{IP}</tex>.
|proof=
Для доказательства леммы построим программы ''Verifier'' и ''Prover'' из определения класса <tex>\mathrm{IP}</tex>.
Сперва арифметизуем формулу <tex>\phi</tex>. Пусть полученный полином <tex>A(x_1, x_2, ..., x_n)</tex> имеет степень <tex>d</tex>.
}}
