Изменения

<tex>\mathrm{\#SAT}=\{\langle \varphi, k \rangle \bigm| mid \varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов <tex>\}</tex>.

|statement=<tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phivarphi(x_1, \ldots, x_m)=k \Leftrightarrow \langle\phivarphi,k\rangle \in \mathrm{\#SAT}</tex>.

Для доказательства леммы построим программы <tex>V</tex> (<tex>\mathit{Verifier}</tex> ) и <tex>P</tex> (<tex>\mathit{Prover}</tex> ) из [[Интерактивные протоколы. Класс IP. Класс AM#Класс IP|определения]] класса <tex>\mathrm{IP}</tex>.

Сперва арифметизуем формулу <tex>\phivarphi</tex>. Пусть полученный полином <tex>A(x_1, x_2, ...\ldots, x_m)</tex> имеет степень <tex>d</tex>.

По лемме (1) вместо условия <tex>\langle \phivarphi, k \rangle \in \mathrm{\#SAT}</tex>, можно проверять условие <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phiA(x_1, \ldots, x_m)=k</tex>.

Приступим к описанию <tex>\mathit{Verifier}</tex>'аинтерактивного протокола.

Если <tex>d=0</tex> или <tex>m=0</tex>, то <tex>\mathit{Verifier}V</tex> может проверить указанное выше условие сам и вернуть соответствующий результат.Иначе запросим у <tex>\mathit{Prover}P</tex>'а такое простое число <tex>p</tex>, что <tex>3dm \le leqslant p \le leqslant 6dm</tex> (такое <tex>p</tex> существует в силу [http://ru.wikipedia.org/wiki/Постулат_Бертрана постулата Бертрана]). Проверим <tex>p</tex> на простоту и на принадлежность заданному промежутку. Как мы [[Класс P#Примеры задач и языков из P|знаем]], <tex>\mathrm{Primes} \in \mathrm{P}</tex>, следовательно на эти операции у <tex>\mathit{Verifier}V</tex>'а уйдёт полиномиальное от размера входа время.

Далее будем проводить все вычисления модулю <tex>p</tex>, то есть над конечным полем <tex> \mathbb{F}_{p} </tex>, что не позволяет числам становиться слишком большими и упрощает анализ.

Попросим <tex>\mathit{Prover}P</tex> 'а прислать <tex>\mathit{Verifier}V</tex>'у формулу <tex>A_0(x_1)= \sum\limits_{x_2 = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(x_1, x_2, ...\ldots, x_m)</tex>. Заметим, что размер формулы <tex>A_0(x_1)</tex> будет полином от длины входа <tex>\mathit{Verifier}V</tex> 'а, так как <tex>A_0(x_1)</tex> — полином степени не выше, чем <tex>d</tex>, от одной переменной, а значит его можно представить в виде <tex>A_0(x) = \sum\limits_{i = 0}^{d} C_i \cdot x ^ i</tex>.

Проверим следующее утверждение: <tex>A_0(0) + A_0(1) = k</tex> (*) (здесь и далее под словом «проверим» будем подразумевать следующее: если утверждение верно, <tex>\mathit{Verifier}V</tex> продолжает свою работу, иначе он прекращает свою работу и возвращет '''false''').

Пусть <tex>r_i = random(0..\lbrace0, \ldots, p-1)\rbrace</tex>. Отправим <tex>r_i</tex> программе <tex>\mathit{Prover}P</tex>.

Попросим <tex>\mathit{Prover}P</tex> 'а прислать <tex>\mathit{Verifier}V</tex>'у формулу <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}, ...\ldots, x_m)</tex>.

Пусть <tex>r_m = random(0..\lbrace0, \ldots, p-1)\rbrace</tex>. Отправим <tex>r_m</tex> программе <tex>\mathit{Prover}P</tex>.

Попросим программу <tex>\mathit{Prover}P</tex> прислать <tex>\mathit{Verifier}V</tex>'у значение <tex>A_m()= A(r_1, r_2, ...\ldots, r_m)</tex>.

А также сами подставим <tex>r_1, r_2, ...\ldots, r_m</tex> в <tex>A(x_1, x_2, ...\ldots, x_m)</tex> и проверим правильность присланного значения <tex>A_m()</tex>.

Докажем теперь, что построенный таким образом <tex>\mathit{Verifier}</tex> интерактивны протокол — корректный. Для этого нужно доказать следующие утверждения:# Построенный <tex>\mathit{Verifier}V</tex> - вероятностная машина Тьюринга, совершающая не более полинома от длины входа действий.# <tex>\langle \varphi, k \rangle \in \mathrm{\#SAT} \Rightarrow \exists P : \mathitmathbb{ProverP} : \Pr[\mathit(V_{Verifier^{Prover}P}(\langle \varphi, k \rangle)=1] ) \ge geqslant 2/{3}</tex>(Completeness).# <tex>\langle \varphi, k \rangle \notin \mathrm{\#SAT} \Rightarrow \forall P :\mathitmathbb{ProverP} :\Pr[\mathit(V_{Verifier^{Prover}P}(\langle \varphi, k \rangle)=1] ) \le leqslant 1/{3}</tex>(Soundness).

#По [[Арифметизация булевых формул с кванторами | лемме (2)]], если <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phivarphi(x_1, \ldots, x_m)=k</tex>, то условия (*) выполнятются, следовательно существует такой <tex>\mathit{Prover}</tex>, что <tex>\Pr[\mathit{Verifier^{Prover}}(\langle\phivarphi,k\rangle) = 1] = 1</tex>, для любой пары <tex>\langle\phivarphi,k\rangle \in \mathrm{\#SAT}</tex>.#Пусть количество наборов, удовлетворяющих <tex>\phivarphi</tex>, не равно <tex>k</tex>. Для того, что бы <tex>\mathit{Verifier}</tex> вернул '''true''', <tex>\mathit{Prover}</tex> 'у необходимо посылать такие <tex>A_i</tex>, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:

:Так как количество наборов, удовлетворяющих <tex>\phivarphi</tex>, не равно <tex>k</tex>, то <tex>\mathit{Prover}</tex> не может послать правильное <tex>A_0</tex>, поскольку в этом случае не выполнится условие <tex>A_0(0) + A_0(1) = k</tex>. Поэтому он посылает не <tex>A_0</tex>, а некое <tex>\tilde{A}_0</tex>.

Сведём язык <tex>\mathrm{TAUT}</tex> к языку <tex>\mathrm{\#SAT}</tex> следующим образом: <tex>\phi varphi \mapsto \langle \phivarphi, 2^k \rangle </tex>, где <tex>k</tex> — количество различных переменных в формуле <tex>\phivarphi</tex>.

Очевидно, что <tex>\phi varphi \in \mathrm{TAUT} \Leftrightarrow \langle \phivarphi, 2^k \rangle \in \mathrm{\#SAT}</tex>.