36
правок
Изменения
Нет описания правки
== Доказательство ==
Для доказательства будем строить вероятностную программу <tex>Verifier</tex>, которая хочет проверить, верно ли, что заданная формула фи <tex>\varphi</tex> имеет ровно к <tex>k</tex> удовлетворяющих наборов. Программа <tex>Verifier </tex> может совершить не больше полинома от длины входа шаговдействий, а также может обращаться к программе <tex>Prover</tex>, которая пытается любым возможным способом убедить нас (т.е. <tex>Verifier) </tex> в верности рассматриваемого утверждения.
Далее в программе <tex>Verifier </tex> будем писать "проверим ...", что означает проверку соответствующего условия, и, при ложности, программа <tex>Verifier </tex> будет сразу завершаться и возвращать <tex>false</tex>, т.к. <tex>Prover нас </tex> её обманывает, а значит, нет правильного доказательства проверяемого утверждения.
Шаг 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>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>. Её размер???.Проверим следующее утверждение: A0<tex>A_0(0) + A0A_0(1) = k</tex>.
Шаг 1.
Пусть <tex>r_1 = random(p)</tex>. Отправим <tex>r_1 </tex> программе <tex>Prover</tex>.
Пусть <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>.
Шаг 2.
...
Шаг <tex>n</tex>.
Пусть <tex>r_n = random(p)</tex>. Отправим <tex>r_n </tex> программе <tex>Prover</tex>.
Пусть <tex>A_n() = A(r_1, r_2, ..., r_n)</tex>.
Попросим программу Prover прислать нам <tex>Verifier</tex>'у значение <tex>A_n()</tex>.Проверим следующее утверждение: <tex>A_n() = A_nA_{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>true</tex>.
Итак, остается доказать, что написанный <tex>Verifier </tex> - корректный <tex>Verifier </tex> для языка <tex>\#SAT</tex>. То есть, нужно доказать:# Построенный <tex>Verifier </tex> - вероятностная машина Тьюринга, совершающая не более полинома от длинны входа действий.
# <tex><\varphi, k> \in \#SAT \Rightarrow \exists P : P(VP(x)) \ge 2/3</tex>.
# <tex><\varphi, k> \notin \#SAT \Rightarrow \forall P : P(VP(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>. Такой ProverТакая программа:## Присылает, например, первое простое число большее <tex>max(2^n , k_p)</tex> и сертификат.## Считает сумму <tex>A_0(x_1) </tex> и присылает формулу.## Получает <tex>r_1</tex>.## Считает сумму <tex>A_1(x_2) </tex> и присылает формулу.
## ...
Ввиду того, что <tex>Prover </tex> все делает хорошо и нигде не ошибается, то <tex>Verifier </tex> дойдет до конца программы и вернет <tex>true</tex>.
# Пусть фи <tex>\varphi</tex> имеет не <tex>k </tex> удовлетворяющих наборов. Тогда для того, что бы <tex>Verifier </tex> вернул <tex>true</tex>, необходимо <tex>Prover</tex>'у посылать такие <tex>A_i</tex>, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:
Шаг 0.
Так как фи <tex>\varphi</tex> имеет не <tex>k </tex> удовлетворяющих наборов, то <tex>Prover </tex> не может послать правильное А_0 - <tex>A_0</tex> – не выполнится условие A0<tex>A_0(0) + A0A_0(1) = k</tex>. Поэтому он посылает не А_0<tex>A_0</tex>, а некое <tex>\tilde{A~}_0</tex>.
Шаг 1.
Во первых, отметим, что ситуация А_0<tex>A_0(r_1) == A_~0\tilde{A}_0(r_1) </tex> происходит с вероятностью меньшей либо равной <tex>d / p </tex> для некоторого случайно выбранного <tex>r_1</tex>, что следует из [[Лемма_Шварца-Зиппеля|леммы Шварца-Зиппеля]]. То есть, с вероятностью большей либо равной <tex>1 - d / p : А_0A_0(r_1) != A_~0\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>.
...
Шаг <tex>n</tex>.
С вероятностью <tex>1 - d / p А_n: A_{n-1}(r_n) != A_~\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>.
Так как мы хотим сделать вероятность возврата <tex>false </tex> большую либо равную <tex>2/3</tex>, то выберем <tex>k_p </tex> так, чтобы <tex>(1 - d / k_p) ^ n >= \ge 2/3</tex>.
Утверждение доказано.
