Sharp SAT — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 7: Строка 7:
  
 
== Доказательство ==
 
== Доказательство ==
Пусть формула <tex>\varphi</tex> как-то записана. Сделаем следующие замены:
+
Для доказательства будем строить вероятностную программу 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>x \land y \to x \cdot y</tex>
 
# <tex> \lnot x \to 1 - x</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> 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>.
+
Вероятность ... .

Версия 23:10, 17 апреля 2010

Определение

[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).

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