36
правок
Изменения
Нет описания правки
== Доказательство ==
Для доказательства будем строить вероятностную программу Verifier, которая хочет проверить, верно ли, что заданная формула фи имеет ровно к удовлетворяющих наборов. Программа Verifier может совершить не больше полинома от длины входа шагов, а также может обращаться к программе Prover, которая пытается любым возможным способом убедить нас (т.е. Verifier) в верности рассматриваемого утверждения.
Далее в программе Verifier будем писать "проверим ...", что означает проверку соответствующего условия, и, при ложности, программа Verifier будет сразу завершаться и возвращать false, т.к. Prover нас обманывает, а значит, нет правильного доказательства проверяемого утверждения.
Программа Verifier будет выполнять следующие шаги.
Шаг 0. Пусть формула <tex>\varphi</tex> каким либо образом записана. Пусть формула фи имеет n переменных и степень d. Сделаем следующие замены и получим формулу <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>.
Будем проверять уравнение по модулю p.
Пусть <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>.
Попросим программу Prover прислать нам формулу A_0(x_1). Её размер???.Проверим следующее утверждение: A0(0) + A0(1) = k???. Шаг 1. Пусть r_1 = random(p). Отправим r_1 программе Prover.
Пусть <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>.
Проверим следующее утверждение: A_1(0) + A_1(1) = A_0(r_1).
Пусть <tex>A_n() = A(r_1, r_2, ..., r_n)</tex>.
Попросим программу Prover прислать нам формулу значение A_n().Проверим следующее утверждение: A_n () = A_n-1(r_n). А также сами подставим r_1, r_2, ..., r_n в А(x_1, x_2, ..., x_n) и проверим правильность присланного значения A_n(). Возвращаем true. Итак, остается доказать, что написанный Verifier - корректный Verifier для языка #SAT. То есть, нужно доказать:# Построенный Verifier - вероятностная машина Тьюринга, совершающая не более полинома от длинны входа действий.# <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>. Доказательство:# Из программы Verifier видно, что она работает за O(n * |input|) = O(poly(|input|)).# Если фи имеет ровно k удовлетворяющих наборов, то существует программа Prover, такая что P(VP(x)) = 1. Такой Prover:## Присылает, например, первое простое число большее 2^n и сертификат.## Считает сумму A_0(x_1) и присылает формулу.## Получает r_1.## Считает сумму A_1(x_2) и присылает формулу.## ...Ввиду того, что Prover все делает хорошо и нигде не ошибается, то Verifier дойдет до конца программы и вернет true. # Пусть фи имеет не k удовлетворяющих наборов. Тогда для того, что бы Verifier вернул true, необходимо Prover'у посылать такие A_i, чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать: Шаг 0. Так как фи имеет не k удовлетворяющих наборов, то Prover не может послать правильное А_0 - не выполнится условие A0(0) + A0(1) = k. Поэтому он посылает не А_0, а некое A~_0. Шаг 1. Во первых, отметим, что ситуация А_0(r_1) == A_~0(r_1) происходит с вероятностью меньшей либо равной d / p для некоторого случайно выбранного r_1, что следует из леммы Шварца-Зиппеля. То есть, с вероятностью большей либо равной 1 - d / p : А_0(r_1) != A_~0(r_1) и, ввиду того, что должно выполняться условие A_1(0) + A_1(1) = A_0(r_1), получаем, что A_1 тоже будет не правильное, т.е. некоторое A~_1. ... Шаг n. С вероятностью 1 - d / p А_n-1(r_n) != A_~n-1(r_n) и потому Verifier получает не A_n, а A~_n. Из этого процесса заметим, что с вероятностью большей либо равной (1 - d / p) ^ n мы дойдем до последнего шага и будем имееть А~_n вместо A_n. Так как на шаге n Verifier вычисляет A_n и проверяет значение, то Verifier вернет false. Так как мы хотим сделать вероятность возврата false большую либо равную 2/3, то выберем k_p так, чтобы (1 - d / k_p) ^ n >= 2/3.
