Теорема Шамира

Теорема (Шамир):

[math]\mathrm{IP} = \mathrm{PS}[/math]

Доказательство:

[math]\triangleright[/math]

[math]\mathrm{IP} \subset \mathrm{PS}[/math] Рассмотрим язык [math]L \in \mathrm{IP}[/math]. Пусть [math]V[/math] — Verifier, соответствующий [math]L[/math], [math]p(n)[/math] — время его работы, [math]f(n)[/math] — количество его запросов к Prover 'у. Напишем программу, распознающую язык [math]L[/math] на полиномиальной памяти. [math]U(x)[/math] [math]n \leftarrow |x|[/math] for [math]P \leftarrow Prover[f(n), p(n)][/math] //(1) [math]count \leftarrow 0[/math] for [math]r \in \{0, 1\}^{p(n)}[/math] //(2) if [math]V(x, r)\bigm{|}_{P} = 1[/math] [math]count[/math]++ if [math]\frac{count}{2^{p(n)}} \ge \frac{2}{3}[/math] return 1 return 0 В цикле [math](1)[/math] перебираются все Prover 'ы, которые отвечают на [math]f(n)[/math] запросов, каждый ответ имеет размер [math]p(n)[/math]. В цикле [math](2)[/math] перебираются все вероятностные ленты размера [math]p(n)[/math]. Так как [math]V[/math] — корректен, то если нашелся Prover, при котором [math]V[/math] допускает слово с вероятностью, большей [math]\frac{2}{3}[/math], то данное слово принадлежит [math]L[/math], иначе — не принадлежит. Очевидно, что данная программа требует полином дополнительной памяти. Значит [math]L \in \mathrm{PS}[/math], следовательно [math]\mathrm{IP} \subset \mathrm{PS}[/math]. [math]\mathrm{PS} \subset \mathrm{IP}[/math]

[math]\triangleleft[/math]

Формулировка

IP = PS

Доказательство

IP ⊂ PS

Рассмотрим язык [math]L \in IP[/math]. Чтобы детерминированная машина Тьюринга [math]m[/math] могла установить принадлежность слова [math]x[/math] языку [math]L[/math], ей нужно перебрать все ответы [math]P[/math] и вероятностные ленты [math]V[/math], просимулировав [math]V[/math] с этими данными и посчитав вероятность допуска. Ясно, что эти действия потребуют не более [math]p(|x|)[/math] памяти, а значит [math]L \in PS[/math].

PS ⊂ IP

Докажем, что язык [math]TQBF \in IP[/math]. Этого достаточно, так как [math]TQBF \in PSC[/math].

Введем следующую арифметизацию булевых формул с кванторами:

• [math]\lnot x \to 1-X[/math]
• [math]x \land y \to XY[/math]x
• [math]x \lor y \to X+Y-XY = 1-(1-X)(1-Y)[/math]
• [math]\exists x \varphi(x) \to \sum\limits_{X=0}^{1} A_\varphi(X)[/math], где [math]A_\varphi[/math] — полином, получившийся в результате арифметизации [math]\varphi[/math]
• [math]\forall x \varphi(x) \to \prod\limits_{X=0}^{1} A_\varphi(X)[/math]

Результат этого выражения будет ненулевым в том и только в том случае, если исходная формула была истинна.

Рассмотрим пример:

[math]\varphi=\forall x_1 \forall x_2 \cdots \forall x_{k-1} \exists x_k (x_k \lor \lnot x_k)[/math]
[math]A_\varphi = \prod\limits_{X_1=0}^{1}\prod\limits_{X_2=0}^{1}\cdots \prod\limits_{X_{k-1}=0}^{1}\sum\limits_{X_k=0}^1(1-X_k(1-X_k)) = 2^{2^{(k-1)}}[/math]

Для записи этого числа нужно [math]2^{(k-1)}[/math] бит. Если [math]k \gg \log|\varphi|[/math], это число невозможно передать за полиномиальное относительно длины исходной формулы время. Чтобы избежать таких больших чисел, приходится проводить все операции по какому-нибудь простому модулю [math]p[/math].

Начало интерактивного протокола:

• P выбирает простое [math]p[/math] и [math]k \equiv A_\psi \pmod{p}[/math] и посылает их V ([math]p[/math] посылается вместе с его сертификатом простоты).
• V проверяет [math]p[/math] на простоту, а [math]k[/math] на неравенство нулю.

Хотелось бы воспользоваться протоколом из доказательства принадлежности #SAT к классу IP, проверяя [math]A_i(1)\cdot A_i(0)=A_{i-1}(r_{i})[/math] в случае, когда [math]x_i[/math] связан квантором [math]\forall[/math], и [math]A_i(1)+A_i(0)=A_{i-1}(r_{i})[/math] для квантора [math]\exists[/math]. К сожалению, сразу этот протокол применить нельзя, потому что произведение может увеличить степень полинома в два раза, а это может потребовать передачи по протоколу полиномов экспоненциальной длины, что не уложится по времени.

Поэтому потребуем, чтобы между появлением переменной и первым ее использованием было не более одного квантора [math]\forall[/math]. Для этого заменим все суффиксы вида [math]\forall x_{i+1} \tau(x_1, x_2, \ldots, x_i, x_{i+1})[/math] на [math]\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')\land \tau(x_1', x_2', \ldots, x_i', x_{i+1})[/math]. Это преобразование не изменит выполнимости формулы, количество ее переменных увеличится лишь в полином от их первоначального количества раз, а сама формула тоже увеличится не более, чем полиномиально. Теперь можно использовать протокол из #SAT для получившейся формулы, передаваться будут полиномы константной степени.