211
правок
Изменения
м
Пусть Попросим ''Prover'' 'а прислать ''Verifier'' 'у формулу <tex>A_i(x_{i+1}) = \sum\limits_{x_{i+2} = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(r_1,\ldots, r_i, x_{i+1}, ..., x_m)</tex>.
Попросим ''Prover'' 'а прислать ''Verifier'' 'у формулу <tex>A_i(x_{i+1})</tex>.
Нет описания правки
'''Шаг 0'''
Запросим у ''Prover'''а такое простое число <tex>p</tex>, что <tex>max(2^m+1, k_p3dm) \le p \le 2 \cdot max(2^m+1, k_p3dm)</tex>. Проверим простоту <tex>p</tex> на простоту и условие <tex>max(2^m+1, k_p) \le p \le 2 \cdot max(2^m+1, k_p)</tex> (константу <tex>k_p</tex> определим позднее)на принадлежность заданному промежутку. Как мы [[Класс P#Примеры задач и языков из P|знаем]], <tex>Primes \in \mathrm{P}</tex>, следовательно на эти операции у ''Verifier'''а уйдёт полиномиальное от размера входа время.
Далее будем проводить все вычисления модулю <tex>p</tex>.
Пусть <tex>r_i = random(p)</tex>. Отправим <tex>r_i</tex> программе ''Prover''.
Проверим следующее утверждение: <tex>A_i(0) + A_i(1) = A_{i-1}(r_i)</tex>.
# <tex>\langle \varphi, k \rangle \notin \#SAT \Rightarrow \forall Prover : P(Verifier^{Prover}(x)) \le 1/3</tex>.
#Из Первый факт следует из построения ''Verifier'' 'а видно, что он работает за <tex>O(poly(|input|))</tex>.
#По [[Арифметизация булевых формул с кванторами | лемме (2)]], если <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phi(x_1, \ldots, x_m)=k</tex>, то условия (*) выполнятются, следовательно существует такой ''Prover'', что <tex>P(Verifier^{Prover}(\langle\phi,k\rangle)) = 1</tex>, для любой пары <tex>\langle\phi,k\rangle \in \#SAT</tex>.
#Пусть количество наборов, удовлетворяющих <tex>\phi</tex>, не равно <tex>k</tex>. Для того, что бы ''Verifier'' вернул ''true'', ''Prover'' 'у необходимо посылать такие <tex>A_i</tex>, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:
:'''Шаг 0'''
:Так как количество наборов, удовлетворяющих <tex>\phi</tex>, не равно <tex>k</tex>, то ''Prover'' не может послать правильное <tex>A_0</tex> – не выполнится условие <tex>A_0(0) + A_0(1) = k</tex>. Поэтому он посылает не <tex>A_0</tex>, а некое <tex>\tilde{A}_0</tex>.
:'''Шаг 1'''
:По [[Лемма Шварца-Зиппеля|лемме Шварца-Зиппеля]] <tex>P(A_0(r_1) = \tilde{A}_0(r_1)) \le \frac d p</tex> для некоторого случайно выбранного <tex>r_1</tex>. Тогда <tex>P(A_0(r_1) \ne \tilde{A}_0(r_1)) \ge 1 - \frac d p</tex>, при этом должно выполняться равенство <tex>A_1(0) + A_1(1) = A_0(r_1)</tex>. Значит с вероятностью не меньше, чем <tex>1 - \frac d p</tex>, ''Prover'' отправит ''Verifier'' 'у <tex>\tilde{A}_1</tex> вместо <tex>A_1</tex>.
:<tex>\ldots</tex>
:'''Шаг m'''
: <tex>P(A_{m-1}(r_m) \ne \tilde{A}_{m-1}(r_m)) \ge 1 - \frac d p</tex>. Значит с такой вероятностью ''Verifier'' получит <tex>\tilde{A}_m</tex> вместо <tex>A_m</tex>. Но так как на шаге <tex>m</tex> ''Verifier'' вычисляет <tex>A_m</tex> и сравнивает его с полученным от ''Prover'' 'а, то в этом случае ''Verifier'' вернет ''false''.
}}
