1632
правки
Изменения
м
Введём понятие арифметизации булевых формул. Пусть нам дана формула <tex>\phi(x_1 \ldots x_m)</tex>. Сделаем следующие преобразования и получим формулу <tex>A_\phi(x_1, x_2, \ldots, x_m)</tex>:
# <tex> x_i \to x_i</tex>;
# <tex> \lnot x \to 1 - x</tex>;
# <tex>\Phi \land \Psi \to A_\Phi \cdot A_\Psi</tex>;
# <tex>\Phi \lor \Psi \to 1 - (1 - A_\Phi) \cdot (1 - A_\Psi)</tex>.
Заметим, что длина формулы при этом возрастёт не более, чем в константу раз.
Запросим Если <tex>d=0</tex> или <tex>m=0</tex>, то ''Verifier'' может проверить указанное выше условие сам и вернуть соответствующий результат.Иначе запросим у ''Prover'''а такое простое число <tex>p</tex>, что <tex>max(2^m+1, k_p) 3dm \le p \le 2 \cdot max(2^m+1, k_p)6dm</tex>. Проверим простоту (такое <tex>p</tex> и условие существует в силу [http://ru.wikipedia.org/wiki/Постулат_Бертрана постулата Бертрана]). Проверим <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>\mathrm{Primes } \in \mathrm{P}</tex>, следовательно на эти операции у ''Verifier'''а уйдёт полиномиальное от размера входа время.
Пусть Попросим ''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>.Проверим следующее утверждение: <tex>A_i(0) + A_i(1) = A_{i-1}(r_i)</tex>(*).
Из построения ''Verifier'' 'а видно, что он работает за <tex>O(poly(|input|))</tex>Докажем эти утверждения.
rollbackEdits.php mass rollback
{{В разработке}}
{{Определение
|definition=
<tex>\mathrm{\#SAT}=\{\langle \varphi, k \rangle \bigm| \varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов <tex>\}</tex>.
}}
{{Лемма
|about=1
|statement=<tex>\phi(sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m) = 0}^1 A_\phi(x_1, \ldots, x_m)=k \Leftrightarrow \langle\phi,k\rangle \in \mathrm{\#SAT}</tex>.|proof=Следует из [[Арифметизация булевых формул с кванторами | леммы (1)]].
}}
{{Лемма
|about=2
|statement=<tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_mathrm{x_m = 0}^1 A_\phi(x_1, \ldots, x_m)=k \iff \langle\phi,k\rangle \in \#SAT</tex>.|proof=Следует из леммы (1).}} {{Лемма|about=3|statement=<tex>\#SAT \in \mathrm{IP}</tex>.
|proof=
Для доказательства леммы построим программы ''Verifier'' и ''Prover'' из [[Интерактивные протоколы. Класс IP. Класс AM#Класс IP|определения ]] класса <tex>\mathrm{IP}</tex>.
Сперва арифметизуем формулу <tex>\phi</tex>. Пусть полученный полином <tex>A(x_1, x_2, ..., x_m)</tex> имеет степень <tex>d</tex>.
По лемме (21) вместо условия <tex>\langle \phi, k \rangle \in \mathrm{\#SAT}</tex>, можно проверять условие <tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phi(x_1, \ldots, x_m)=k</tex>.
Приступим к описанию ''Verifier'''а.
'''Шаг 0'''
Далее будем проводить все вычисления модулю <tex>p</tex>.
Попросим ''Prover'' 'а прислать ''Verifier'' 'у формулу <tex>A_0(x_1)= \sum\limits_{x_2 = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(x_1, x_2, ..., x_m)</tex>.
Заметим, что размер формулы <tex>A_0(x_1)</tex> будет полином от длины входа ''Verifier'' 'а, так как <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> (*) (здесь и далее под словом «проверим» будем подразумевать следующее: если утверждение верно, ''Verifier'' продолжает свою работу, иначе он прекращает свою работу и возвращет '''false''').
'''Шаг i'''
Пусть <tex>r_i = random(0..p-1)</tex>. Отправим <tex>r_i</tex> программе ''Prover''.
'''Шаг m'''
Пусть <tex>r_m = random(0..p-1)</tex>. Отправим <tex>r_m</tex> программе ''Prover''.
Попросим программу ''Prover'' прислать ''Verifier'' 'у значение <tex>A_m()= A(r_1, r_2, ..., r_m)</tex>.
Проверим следующее утверждение: <tex>A_m() = A_{m-1}(r_m)</tex>(*).
А также сами подставим <tex>r_1, r_2, ..., r_m</tex> в <tex>A(x_1, x_2, ..., x_m)</tex> и проверим правильность присланного значения <tex>A_m()</tex>.
Возвращаем '''true'''.
Докажем теперь, что построенный таким образом ''Verifier'' — корректный. Таким образом, Для этого нужно доказатьследующие утверждения:
# Построенный ''Verifier'' - вероятностная машина Тьюринга, совершающая не более полинома от длины входа действий.
# <tex>\langle \varphi, k \rangle \in \mathrm{\#SAT } \Rightarrow \exists \mathit{Prover } : P(\mathit{Verifier^{Prover}}(x\langle \varphi, k \rangle)=1) \ge 2/3</tex>.# <tex>\langle \varphi, k \rangle \notin \mathrm{\#SAT } \Rightarrow \forall \mathit{Prover } : P(\mathit{Verifier^{Prover}}(x\langle \varphi, k \rangle)=1) \le 1/3</tex>.
#Первый факт следует из построения ''Verifier'' 'а.
#По [[Арифметизация булевых формул с кванторами | лемме (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(\mathit{Verifier^{Prover}}(\langle\phi,k\rangle)) = 1</tex>, для любой пары <tex>\langle\phi,k\rangle \in \mathrm{\#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>.
:<tex>\ldots</tex>
:'''Шаг i'''
:Заметим, что если на каком-то шаге <tex>A_{i-1}(r_i) = \tilde{A}_{i-1}(r_i)</tex>, то начиная со следующего шага ''Prover'' может посылать правильные <tex>A_j</tex> и в итоге ''Verifier'' вернёт '''true'''.
:Для некоторого случайно выбранного <tex>r_i</tex> вероятность того, что <tex>A_{i-1}(r_i) = \tilde{A}_{i-1}(r_i)</tex>, то есть <tex>r_i</tex> — корень полинома <tex>(A_{i-1} - \tilde{A}_{i-1})(r_i)</tex>, имеющего степень не больше <tex>d</tex>, не превосходит <tex>\frac{d}{p}</tex>.
:<tex>\ldots</tex>
:'''Шаг m'''
:Так как на последнем шаге ''Verifier'' полученным от ''Prover'' значение с непосредственно вычисленным, слово будет допущено только в том случае, когда ''Prover'' смог прислать верное значение, что в свою очередь возможно лишь если на одном из предыдущих шагов был верно угадан корень полинома.
:
:Вычислим вероятность того, что хотя бы раз корень был угадан.
:<tex>P(\mathit{Verifier^{Prover}}(\langle \varphi, k \rangle)=1) = 1 - (1 - \frac d p)^m \le 1 - (1 - \frac d {3dm})^m \le \frac 1 3</tex>.
:В последнем переходе мы воспользовались [http://ru.wikipedia.org/wiki/Ряд_Тейлора формулой Тейлора] для логарифма и экспоненты, а также тем, что <tex>m>0</tex>.
Таким образом, построенный нами ''Verifier'' корректен, а значит лемма доказана.
}}
{{Лемма
|about=43
|statement=<tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.
|proof=
Сведём язык <tex>\mathrm{TAUT}</tex> к языку <tex>\mathrm{\#SAT}</tex> следующим образом: <tex>\phi \mapsto \langle \phi, 2^k \rangle </tex>, где <tex>k</tex> — количество различных переменных в формуле <tex>\phi</tex>.
Очевидно, что <tex>\phi \in \mathrm{TAUT } \iff Leftrightarrow \langle \phi, 2^k \rangle \in \mathrm{\#SAT}</tex>.
По лемме (32) <tex>\mathrm{\#SAT } \in \mathrm{IP}</tex>. Тогда <tex>\mathrm{TAUT } \in \mathrm{IP}</tex>. Так как <tex>\mathrm{TAUT } \in \mathrm{coNPC}</tex>, то <tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.
}}
[[Категория: Теория сложности]]
