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 будет выполнять следующие шаги.

Пусть формула [math]\varphi[/math] каким либо образом записана. Сделаем следующие замены и получим формулу [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 прислать нам простое число p > 2^n, и сертификат о его простоте. Проверим простоту p по сертификату, и условие p > 2^n.

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

Будем проверять уравнение по модулю 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???.

Пусть r_1 = random(p). Пусть [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).

Продолжим так делать.

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

Попросим программу Prover прислать нам формулу A_n(). Проверим следующее утверждение: A_n = A_n-1(r_n).

Вероятность ... .