Изменения
Нет описания правки
Для записи этого числа нужно <tex>2^{(k-1)}</tex> бит. Если <tex>k \gg \log|\varphi|</tex>, это число невозможно передать за полиномиальное относительно длины исходной формулы время. Чтобы избежать таких больших чисел, приходится проводить все операции по какому-нибудь простому модулю <tex>p</tex>.
* ''P'' выбирает простое <tex>p</tex> и <tex>k \equiv A_\psi \pmod{p}</tex> и посылает их ''V'' (<tex>p</tex> посылается вместе с его сертификатом простоты).
* ''V'' проверяет <tex>p</tex> на простоту, а <tex>k</tex> на неравенство нулю.
Хотелось бы воспользоваться протоколом из [[#SAT|доказательства принадлежности #SAT к классу IP]], лишь проверяя <tex>A_i(1)+A_i(0)=A_{i-1}(r_{i})</tex> в случае, когда по <tex>X_i</tex> произведение. К сожалению, сразу этот протокол применить нельзя, потому что произведение может увеличить степень полинома в два раза. Поэтому потребуем, чтобы между появлением переменной и первым ее использованием было не более одного квантора <tex>\forall</tex>. Для этого заменим все суффиксы вида <tex>\forall x_{i+1} \tau(x_1, x_2, \ldots, x_i, x_{i+1})</tex> на <tex>\forall x_{i+1} \exists x_1',\ldots,x_i'(x_1=x_1')\land(x_2=x_2')\land \ldots \land(x_i=x_i')\tau(x_1', x_2', \ldots, x_i', x_{i+1})</tex>. От такого преобразования количество переменных увеличится лишь в полином от их первоначального количества раз, сама формула тоже увеличится не более, чем полиномиально. Теперь после арифметизации по протоколу из [[#SAT]] будут передаваться полиномы не выше второй степени.
