Sharp SAT

Определение

[math]\#SAT = \{ \lt \varphi, k\gt | \varphi[/math] имеет [math]k[/math] удовлетворяющих наборов [math]\}[/math]

Утверждение

[math]\#SAT \in IP[/math]

Доказательство

Для доказательства будем строить вероятностную программу Verifier, которая хочет проверить, верно ли, что заданная формула фи имеет ровно к удовлетворяющих наборов. Программа Verifier может совершить не больше полинома от длины входа шагов, а также может обращаться к программе Prover, которая пытается любым возможным способом убедить нас (т.е. Verifier) в верности рассматриваемого утверждения.

Далее в программе Verifier будем писать "проверим ...", что означает проверку соответствующего условия, и, при ложности, программа Verifier будет сразу завершаться и возвращать false, т.к. Prover нас обманывает, а значит, нет правильного доказательства проверяемого утверждения.

Программа Verifier будет выполнять следующие шаги.

Шаг 0.

Пусть формула [math]\varphi[/math] каким либо образом записана. Пусть формула фи имеет n переменных и степень d. Сделаем следующие замены и получим формулу [math]A(x_1, x_2, ..., x_n)[/math]:

1. [math]x \land y \to x \cdot y[/math]
2. [math] \lnot x \to 1 - x[/math]
3. [math] x \lor y \to x + y - x \cdot y = 1 - (1 - x) \cdot (1 - y)[/math]

Заметим, что длина формулы возрастет не больше, чем в константу раз.

Итак, надо проверить следующее арифметическое уравнение: [math]\sum_{x_1 = 0}^{1}\sum_{x_2 = 0}^{1}...\sum_{x_n = 0}^{1} A(x_1, x_2, ..., x_n) = k[/math].

А надо ли отправлять получившуюся А Proverу, или может он видит input и сам сделает такое преобразование?

Попросим программу Prover прислать нам простое число p > max(2^n, p_k) и сертификат о его простоте. Проверим простоту p по сертификату, и условие p > max(2^n, p_k). Константу p_k определим позднее.

Будем проверять уравнение по модулю p.

Пусть [math]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)[/math].

Попросим программу Prover прислать нам формулу A_0(x_1). Её размер???. Проверим следующее утверждение: A0(0) + A0(1) = k.

Шаг 1.

Пусть r_1 = random(p). Отправим r_1 программе Prover.

Пусть [math]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)[/math].

Попросим программу Prover прислать нам формулу A_1(x_2). Проверим следующее утверждение: A_1(0) + A_1(1) = A_0(r_1).

Шаг 2.

...

Шаг n.

Пусть r_n = random(p). Отправим r_n программе Prover.

Пусть [math]A_n() = A(r_1, r_2, ..., r_n)[/math].

Попросим программу 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. То есть, нужно доказать:

1. Построенный Verifier - вероятностная машина Тьюринга, совершающая не более полинома от длинны входа действий.
2. [math]\lt \varphi, k\gt \in \#SAT \Rightarrow \exists P : P(VP(x)) \ge 2/3[/math].
3. [math]\lt \varphi, k\gt \notin \#SAT \Rightarrow \forall P : P(VP(x)) \le 1/3[/math].

Доказательство:

1. Из программы Verifier видно, что она работает за O(n * |input|) = O(poly(|input|)).
2. Если фи имеет ровно k удовлетворяющих наборов, то существует программа Prover, такая что P(VP(x)) = 1. Такой Prover:
   1. Присылает, например, первое простое число большее 2^n и сертификат.
   2. Считает сумму A_0(x_1) и присылает формулу.
   3. Получает r_1.
   4. Считает сумму A_1(x_2) и присылает формулу.
   5. ...

Ввиду того, что Prover все делает хорошо и нигде не ошибается, то Verifier дойдет до конца программы и вернет true.

1. Пусть фи имеет не 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.

Утверждение доказано.