Теорема Шамира — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(PS ⊂ IP)
м (rollbackEdits.php mass rollback)
 
(не показано 9 промежуточных версий 3 участников)
Строка 1: Строка 1:
== Формулировка ==
+
{{Теорема
'''[[Класс IP|IP]]''' = '''[[Класс PS|PS]]'''
+
|author=Шамир
== Доказательство ==
+
|statement=<tex>\mathrm{IP} = \mathrm{PS}</tex>
=== IP PS ===
+
|proof=
Рассмотрим язык <tex>L \in IP</tex>. Чтобы детерминированная машина Тьюринга <tex>m</tex> могла установить принадлежность слова <tex>x</tex> языку <tex>L</tex>, ей нужно перебрать все ответы <tex>P</tex> и вероятностные ленты <tex>V</tex>, просимулировав <tex>V</tex> с этими данными и посчитав вероятность допуска. Ясно, что эти действия потребуют не более <tex>p(|x|)</tex> памяти, а значит <tex>L \in PS</tex>.
+
* <tex>\mathrm{IP} \subset \mathrm{PS}</tex>
=== PS ⊂ IP ===
+
Рассмотрим язык <tex>L \in \mathrm{IP}</tex>. Пусть <tex>V</tex> {{---}} ''Verifier'', соответствующий <tex>L</tex>, <tex>p(n)</tex> {{---}} время его работы, <tex>f(n)</tex> {{---}} количество его запросов к ''Prover'' 'у. Напишем программу, распознающую язык <tex>L</tex> на полиномиальной памяти.
Докажем, что язык <tex>TQBF \in IP</tex>. Этого достаточно, так как <tex>TQBF \in PSC</tex>.
+
<tex>U(x)</tex>
 +
    <tex>n \leftarrow |x|</tex>
 +
    '''for''' <tex>P \leftarrow Prover[f(n), p(n)]</tex>    //(1)
 +
        <tex>count \leftarrow 0</tex>
 +
        '''for''' <tex>r \in \{0, 1\}^{p(n)}</tex>   //(2)
 +
            '''if''' <tex>V(x, r)\bigm{|}_{P} = 1</tex>
 +
                <tex>count</tex>++
 +
        '''if''' <tex dpi = "160">\frac{count}{2^{p(n)}} \ge \frac{2}{3}</tex>
 +
            '''return''' 1
 +
    '''return''' 0
  
Введем следующую арифметизацию булевых формул с кванторами:
+
В цикле <tex>(1)</tex> перебираются все ''Prover'' 'ы, которые отвечают на <tex>f(n)</tex> запросов, каждый ответ имеет размер <tex>p(n)</tex>. В цикле <tex>(2)</tex> перебираются все вероятностные ленты размера <tex>p(n)</tex>. Так как <tex>V</tex> {{---}} корректен, то если нашелся ''Prover'', при котором <tex>V</tex> допускает слово с вероятностью, большей <tex>\frac{2}{3}</tex>, то данное слово принадлежит <tex>L</tex>, иначе {{---}} не принадлежит. Очевидно, что данная программа требует полином дополнительной памяти. Значит <tex>L \in \mathrm{PS}</tex>, следовательно <tex>\mathrm{IP} \subset \mathrm{PS}</tex>.
* <tex>\lnot x \to 1-X</tex>
+
* <tex>\mathrm{PS} \subset \mathrm{IP}</tex>
* <tex>x \land y \to XY</tex>
 
* <tex>x \lor y \to X+Y-XY = 1-(1-X)(1-Y)</tex>
 
* <tex>\exists x \varphi(x) \to \sum\limits_{X=0}^{1} A_\varphi(X)</tex>, где <tex>A_\varphi</tex> — полином, получившийся в результате арифметизации <tex>\varphi</tex>
 
* <tex>\forall x \varphi(x) \to \prod\limits_{X=0}^{1} A_\varphi(X)</tex>
 
Результат этого выражения будет ненулевым в том и только в том случае, если исходная формула была истинна.
 
  
Рассмотрим пример:
+
Докажем, что <tex>\mathrm{TQBF} \in \mathrm{IP}</tex>. Так как <tex>\mathrm{TQBF} \in \mathrm{PSC}</tex>, то из этого будет следовать, что <tex>\mathrm{PS} \subset \mathrm{IP}</tex>.
<tex>\varphi=\forall x_1 \forall x_2 \cdots \forall x_{k-1} \exists x_k (x_k \lor \lnot x_k)</tex>
 
<tex>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)}}</tex>
 
Для записи этого числа нужно <tex>2^{(k-1)}</tex> бит. Если <tex>k \gg \log|\varphi|</tex>, это число невозможно передать за полиномиальное относительно длины исходной формулы время. Чтобы избежать таких больших чисел, приходится проводить все операции по какому-нибудь простому модулю <tex>p</tex>.
 
  
Начало интерактивного протокола:
+
Пусть дана формула <tex>Q_1 \ldots Q_m \phi(x_1, \ldots ,x_m)</tex>. В процессе [[Арифметизация булевых формул с кванторами|арифметизации]] она перейдет в <tex>R_1 \ldots R_m A_\phi(x_1,\ldots,x_m)</tex>. Воспользуемся протоколом, описанным в [[Лемма о соотношении coNP и IP|доказательстве принадлежности #SAT к классу IP]]. Для этого необходимо, чтобы степень полиномов <tex>A_i(x_{i+1})</tex> была полиномиальной относительно длины входа. Преобразуем выражение с помощью оператора линеаризации к виду <tex>R_1 L_1 \ldots R_i L_1 L_2 \ldots L_i \ldots R_m L_1 L_2 \ldots L_m A_\phi(x_1,\ldots,x_m)</tex>. Размер новой формулы не превосходит квадрата исходной, степень полиномов не превосходит двух. Тогда, используя условия, описанные в [[Арифметизация булевых формул с кванторами|леммах 2 и 3]], для проверки ответов, присылаемых ''Prover'' 'ом, можно построить искомый протокол. Значит <tex>\mathrm{TQBF} \in \mathrm{IP}</tex>, следовательно <tex>\mathrm{PS} \subset \mathrm{IP}</tex>.
 
+
}}
* ''P'' выбирает простое <tex>p</tex> и <tex>k \equiv A_\psi \pmod{p}</tex> и посылает их ''V'' (<tex>p</tex> посылается вместе с его сертификатом простоты).
 
* ''V'' проверяет <tex>p</tex> на простоту, а <tex>k</tex> на неравенство нулю.
 
Хотелось бы воспользоваться протоколом из [[Sharp SAT|доказательства принадлежности #SAT к классу IP]], лишь проверяя <tex>A_i(1)\cdot 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>. От такого преобразования количество переменных увеличится лишь в полином от их первоначального количества раз, сама формула тоже увеличится не более, чем полиномиально. Теперь можно использовать протокол из [[Sharp SAT|#SAT]], передаваться будут полиномы не выше второй степени.
 

Текущая версия на 19:20, 4 сентября 2022

Теорема (Шамир):
[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]\mathrm{TQBF} \in \mathrm{IP}[/math]. Так как [math]\mathrm{TQBF} \in \mathrm{PSC}[/math], то из этого будет следовать, что [math]\mathrm{PS} \subset \mathrm{IP}[/math].

Пусть дана формула [math]Q_1 \ldots Q_m \phi(x_1, \ldots ,x_m)[/math]. В процессе арифметизации она перейдет в [math]R_1 \ldots R_m A_\phi(x_1,\ldots,x_m)[/math]. Воспользуемся протоколом, описанным в доказательстве принадлежности #SAT к классу IP. Для этого необходимо, чтобы степень полиномов [math]A_i(x_{i+1})[/math] была полиномиальной относительно длины входа. Преобразуем выражение с помощью оператора линеаризации к виду [math]R_1 L_1 \ldots R_i L_1 L_2 \ldots L_i \ldots R_m L_1 L_2 \ldots L_m A_\phi(x_1,\ldots,x_m)[/math]. Размер новой формулы не превосходит квадрата исходной, степень полиномов не превосходит двух. Тогда, используя условия, описанные в леммах 2 и 3, для проверки ответов, присылаемых Prover 'ом, можно построить искомый протокол. Значит [math]\mathrm{TQBF} \in \mathrm{IP}[/math], следовательно [math]\mathrm{PS} \subset \mathrm{IP}[/math].
[math]\triangleleft[/math]