36
правок
Изменения
Нет описания правки
Шаг 0.
Пусть формула <tex>\varphi</tex> каким -либо образом записана. Пусть формула <tex>\varphi</tex> имеет <tex>n</tex> переменных и степень <tex>d</tex>. Сделаем следующие замены и получим формулу <tex>A(x_1, x_2, ..., x_n)</tex>:
# <tex>x \land y \to x \cdot y</tex>
# <tex> \lnot x \to 1 - x</tex>
Итак, надо проверить следующее арифметическое уравнение: <tex>\sum_{x_1 = 0}^{1}\sum_{x_2 = 0}^{1}...\sum_{x_n = 0}^{1} A(x_1, x_2, ..., x_n) = k</tex>.
Попросим <tex>Prover</tex> 'а прислать <tex>Verifier</tex>'у простое число <tex>p > max(2^n, k_p)</tex> и сертификат о его простоте. Проверим простоту <tex>p</tex> по сертификату, и условие <tex>p > max(2^n, k_p)</tex>. Константу <tex>k_p</tex> определим позднее.
Пусть <tex>A_0(x_1) = \sum_{x_2 = 0}^{1}\sum_{x_3 = 0}^{1}...\sum_{x_n = 0}^{1} A(x_1, x_2, ..., x_n)</tex>.
Попросим <tex>Prover</tex> 'а прислать <tex>Verifier</tex>'у формулу <tex>A_0(x_1)</tex>. Её размер???.
Проверим следующее утверждение: <tex>A_0(0) + A_0(1) = k</tex>.
Заметим, что размер формулы <tex>A_0(x_1)</tex> будет полином от длинны входа <tex>Verifier</tex>'а. Этот факт следует из того, что формула имеет степень меньшую либо равную <tex>d</tex> и она от одной переменной. Поэтому её можно представить так: <tex>A_0(x) = \sum_{i = 0}^{d} C_i \cdot x ^ i</tex>, и попросить <tex>Prover</tex>'а прислать только сами коэффициенты <tex>C_i</tex> по модулю <tex>p</tex>.
Шаг 1.
Пусть <tex>A_1(x_2) = \sum_{x_3 = 0}^{1}\sum_{x_4 = 0}^{1}...\sum_{x_n = 0}^{1} A(r_1, x_2, ..., x_n)</tex>.
Попросим <tex>Prover</tex> 'а прислать <tex>Verifier</tex>'у формулу <tex>A_1(x_2)</tex>.
Проверим следующее утверждение: <tex>A_1(0) + A_1(1) = A_0(r_1)</tex>.
Пусть <tex>A_n() = A(r_1, r_2, ..., r_n)</tex>.
Попросим программу <tex>Prover </tex> прислать <tex>Verifier</tex>'у значение <tex>A_n()</tex>.
Проверим следующее утверждение: <tex>A_n() = A_{n-1}(r_n)</tex>.
А также сами подставим <tex>r_1, r_2, ..., r_n</tex> в <tex>A(x_1, x_2, ..., x_n)</tex> и проверим правильность присланного значения <tex>A_n()</tex>.
Итак, остается доказать, что написанный <tex>Verifier</tex> - корректный <tex>Verifier</tex> для языка <tex>\#SAT</tex>. То естьТаким образом, нужно доказать:
# Построенный <tex>Verifier</tex> - вероятностная машина Тьюринга, совершающая не более полинома от длинны входа действий.
# <tex><\varphi, k> \in \#SAT \Rightarrow \exists P Prover : P(VPVerifier^{Prover}(x)) \ge 2/3</tex>.# <tex><\varphi, k> \notin \#SAT \Rightarrow \forall P Prover : P(VPVerifier^{Prover}(x)) \le 1/3</tex>.
Доказательство:
# Из программы <tex>Verifier</tex> видно, что она работает за <tex>O(n \cdot |input|) = O(poly(|input|))</tex>.
# Если <tex>\varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов, то существует такая программа <tex>Prover</tex>, такая что <tex>P(VP(x)) = 1</tex>. Такая программа:## Присылает, например, первое простое число , большее <tex>max(2^n, k_p)</tex> , и сертификат.
## Считает сумму <tex>A_0(x_1)</tex> и присылает формулу.
## Получает <tex>r_1</tex>.
## Считает сумму <tex>A_1(x_2)</tex> и присылает формулу.
## ...
# Пусть <tex>\varphi</tex> имеет не <tex>k</tex> удовлетворяющих наборов. Тогда для того, что бы <tex>Verifier</tex> вернул <tex>true</tex>, необходимо <tex>Prover</tex>'у посылать такие <tex>A_i</tex>, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:
Шаг 1.
Во первых, отметим, что ситуация <tex>A_0(r_1) = \tilde{A}_0(r_1)</tex> происходит с вероятностью меньшей либо равной <tex>d / p</tex> для некоторого случайно выбранного <tex>r_1</tex>, что следует из [[Лемма_Шварца-Зиппеля|леммы Шварца-Зиппеля]]. То естьТаким образом, с вероятностью большей либо равной <tex>1 - d / p : A_0(r_1) != \ne \tilde{A}_0(r_1)</tex> и, ввиду того, что должно выполняться условие <tex>A_1(0) + A_1(1) = A_0(r_1)</tex>, получаем, что <tex>A_1</tex> тоже будет не правильноенеправильное, т.е. некоторое <tex>\tilde{A}_1</tex>. Шаг 2.
...
Шаг <tex>n</tex>.
С вероятностью <tex>1 - d / p : A_{n-1}(r_n) != \ne \tilde{A}_{n-1}(r_n)</tex> , и потому <tex>Verifier</tex> получит не <tex>A_n</tex>, а <tex>\tilde{A}_n</tex>.
Из этого процесса заметим, что с вероятностью большей либо равной <tex>(1 - d / p) ^ n</tex> мы дойдем до последнего шага и будем имееть <tex>\tilde{A}_n</tex> вместо <tex>A_n</tex>. Так как на шаге <tex>n</tex> <tex>Verifier</tex> вычисляет <tex>A_n</tex> и проверяет значение, то <tex>Verifier</tex> вернет <tex>false</tex>.
