Изменения

Перейти к: навигация, поиск

Sharp SAT

2580 байт добавлено, 23:10, 17 апреля 2010
Нет описания правки
== Доказательство ==
Для доказательства будем строить вероятностную программу Verifier, которая хочет проверить, верно ли, что заданная формула фи имеет ровно к удовлетворяющих наборов. Программа Verifier может совершить не больше полинома от длины входа шагов, а также может обращаться к программе Prover, которая пытается любым возможным способом убедить нас (т.е. Verifier) в верности рассматриваемого утверждения. Программа Verifier будет выполнять следующие шаги. Пусть формула <tex>\varphi</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> x \lor y \to x + y - x \cdot y = 1 - (1 - x) \cdot (1 - y)</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>. Попросим программу Prover прислать нам простое число p > 2^n, и сертификат о его простоте.Проверим простоту p по сертификату, и условие p > 2^n. Заметим, что если какое-либо проверяемое условие не выполнено, то программа Verifier сразу завершается и возвращает false, т.к. Prover нас обманывает, а значит, нет правильного доказательства проверяемого утверждения. Будем проверять уравнение по модулю 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???. Пусть r_1 = random(p).Пусть <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>. Попросим программу Prover прислать нам формулу A_1(x_2).Проверим следующее утверждение: A_1(0) + A_1(1) = A_0(r_1). Продолжим так делать. Пусть r_n = random(p).Пусть <tex>A_n() = A(r_1, r_2, ..., r_n)</tex>. Попросим программу Prover прислать нам формулу A_n().Проверим следующее утверждение: A_n = A_n-1(r_n).
Итак, надо проверить следующее уравнение: <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>.
36
правок

Навигация