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

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 1: Строка 1:
 
== Определение ==
 
== Определение ==
  
<tex>\#SAT = \{ <\varphi, k> | \varphi</tex> имеет <tex>k</tex> удовлетворяющих наборов <tex>\}</tex>
+
<tex>\#SAT = \{ \langle \varphi, k \rangle | \varphi</tex> имеет <tex>k</tex> удовлетворяющих наборов <tex>\}</tex>
  
 
== Утверждение ==
 
== Утверждение ==
Строка 28: Строка 28:
 
Проверим простоту <tex>p</tex> по сертификату и условие <tex>p > max(2^n, k_p)</tex>. Константу <tex>k_p</tex> определим позднее.
 
Проверим простоту <tex>p</tex> по сертификату и условие <tex>p > max(2^n, k_p)</tex>. Константу <tex>k_p</tex> определим позднее.
  
Далее будем вычислять и проверять равенства по модулю <tex>p</tex>.
+
Далее будем вычислять значения и проверять равенства по модулю <tex>p</tex>.
  
 
Пусть <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>.
 
Пусть <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>.
Строка 71: Строка 71:
  
 
# Из программы ''Verifier'' видно, что она работает за <tex>O(poly(|input|))</tex>.
 
# Из программы ''Verifier'' видно, что она работает за <tex>O(poly(|input|))</tex>.
# Если <tex>\varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов, то существует такая программа ''Prover'', что <tex>P(VP(x)) = 1</tex>. Такая программа:
+
# Если <tex>\varphi</tex> имеет ровно <tex>k</tex> удовлетворяющих наборов, то существует такая программа ''Prover'', что <tex>P(Verifier^{Prover}(x)) = 1</tex>. Такая программа:
 
## Присылает, например, первое простое число, большее <tex>max(2^n, k_p)</tex>, и сертификат.
 
## Присылает, например, первое простое число, большее <tex>max(2^n, k_p)</tex>, и сертификат.
 
## Считает сумму <tex>A_0(x_1)</tex> и присылает формулу.
 
## Считает сумму <tex>A_0(x_1)</tex> и присылает формулу.
Строка 97: Строка 97:
 
Из этого процесса заметим, что с вероятностью большей либо равной <tex>(1 - d / p) ^ n</tex> мы дойдем до последнего шага и будем имееть <tex>\tilde{A}_n</tex> вместо <tex>A_n</tex>. Так как на шаге <tex>n</tex> ''Verifier'' вычисляет <tex>A_n</tex> и проверяет значение, то ''Verifier'' вернет ''false''.  
 
Из этого процесса заметим, что с вероятностью большей либо равной <tex>(1 - d / p) ^ n</tex> мы дойдем до последнего шага и будем имееть <tex>\tilde{A}_n</tex> вместо <tex>A_n</tex>. Так как на шаге <tex>n</tex> ''Verifier'' вычисляет <tex>A_n</tex> и проверяет значение, то ''Verifier'' вернет ''false''.  
  
Так как мы хотим сделать вероятность возврата ''false'' большую либо равную <tex>2/3</tex>, то выберем <tex>k_p</tex> так, чтобы <tex>(1 - d / k_p) ^ n \ge 2/3</tex>.  
+
Так как мы хотим сделать вероятность возврата ''false'' большую либо равную <tex>2/3</tex>, то выберем <tex>k_p</tex> так, чтобы <tex>(1-d/k_p)^n \ge 2/3</tex>. Возьмем <tex>k_p = 3 d \cdot n</tex>. Заметим, что длина <tex>k_p</tex> есть <tex>poly(|input|)</tex>. Из разложения функции по Тейлору получаем: <tex>(1-d/k_p)^n = (1 - 1/(3n))^n = 1 - 1/3 + \frac{n(n - 1)}{2 (3n)^2} - \frac{n(n-1)(n-2)}{6 (3n)^3} + ... \ge</tex><tex>\ge 2/3 + \frac{n(n-1)}{n^2}(\frac{1}{2 \cdot 3^2} - \frac{1}{6 \cdot 3^3}) + ... \ge 2/3</tex>.  
  
 
Утверждение доказано.
 
Утверждение доказано.

Версия 17:32, 27 апреля 2010

Определение

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

Утверждение

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

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

Для доказательства будем строить вероятностную программу Verifier, которая хочет проверить, верно ли, что заданная формула [math]\varphi[/math] имеет ровно [math]k[/math] удовлетворяющих наборов. Программа Verifier может совершить не больше полинома от длины входа действий, а также может обращаться к программе Prover, которая пытается любым возможным способом убедить Verifier в верности рассматриваемого утверждения.

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

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

Шаг 0.

Пусть формула [math]\varphi[/math] каким-либо образом записана. Пусть формула [math]\varphi[/math] имеет [math]n[/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]A(x_1, x_2, ..., x_n)[/math] имеет степень [math]d[/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 'а прислать Verifier 'у простое число [math]p \gt max(2^n, k_p)[/math] и сертификат о его простоте. Проверим простоту [math]p[/math] по сертификату и условие [math]p \gt max(2^n, k_p)[/math]. Константу [math]k_p[/math] определим позднее.

Далее будем вычислять значения и проверять равенства по модулю [math]p[/math].

Пусть [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 'а прислать Verifier 'у формулу [math]A_0(x_1)[/math]. Проверим следующее утверждение: [math]A_0(0) + A_0(1) = k[/math].

Заметим, что размер формулы [math]A_0(x_1)[/math] будет полином от длинны входа Verifier 'а. Этот факт следует из того, что формула имеет степень меньшую либо равную [math]d[/math], и она от одной переменной. Поэтому её можно представить так: [math]A_0(x) = \sum_{i = 0}^{d} C_i \cdot x ^ i[/math], и попросить Prover 'а прислать только сами коэффициенты [math]C_i[/math] по модулю [math]p[/math].

Шаг 1.

Пусть [math]r_1 = random(p)[/math]. Отправим [math]r_1[/math] программе 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 'а прислать Verifier 'у формулу [math]A_1(x_2)[/math]. Проверим следующее утверждение: [math]A_1(0) + A_1(1) = A_0(r_1)[/math].

Шаг 2.

...

Шаг [math]n[/math].

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

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

Попросим программу Prover прислать Verifier 'у значение [math]A_n()[/math]. Проверим следующее утверждение: [math]A_n() = A_{n-1}(r_n)[/math]. А также сами подставим [math]r_1, r_2, ..., r_n[/math] в [math]A(x_1, x_2, ..., x_n)[/math] и проверим правильность присланного значения [math]A_n()[/math].

Возвращаем true.


Итак, остается доказать, что написанный Verifier - корректный Verifier для языка [math]\#SAT[/math]. Таким образом, нужно доказать:

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

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

  1. Из программы Verifier видно, что она работает за [math]O(poly(|input|))[/math].
  2. Если [math]\varphi[/math] имеет ровно [math]k[/math] удовлетворяющих наборов, то существует такая программа Prover, что [math]P(Verifier^{Prover}(x)) = 1[/math]. Такая программа:
    1. Присылает, например, первое простое число, большее [math]max(2^n, k_p)[/math], и сертификат.
    2. Считает сумму [math]A_0(x_1)[/math] и присылает формулу.
    3. Получает [math]r_1[/math].
    4. Считает сумму [math]A_1(x_2)[/math] и присылает формулу.
    5. ...
  3. Пусть [math]\varphi[/math] имеет не [math]k[/math] удовлетворяющих наборов. Тогда для того, что бы Verifier вернул true, необходимо Prover 'у посылать такие [math]A_i[/math], чтобы выполнялись все проверяемые условия. Посмотрим на то, что он может послать:

Шаг 0.

Так как [math]\varphi[/math] имеет не [math]k[/math] удовлетворяющих наборов, то Prover не может послать правильное [math]A_0[/math] – не выполнится условие [math]A_0(0) + A_0(1) = k[/math]. Поэтому он посылает не [math]A_0[/math], а некое [math]\tilde{A}_0[/math].

Шаг 1.

Во первых, отметим, что ситуация [math]A_0(r_1) = \tilde{A}_0(r_1)[/math] происходит с вероятностью меньшей либо равной [math]d / p[/math] для некоторого случайно выбранного [math]r_1[/math], что следует из леммы Шварца-Зиппеля. Таким образом, с вероятностью большей либо равной [math]1 - d / p : A_0(r_1) \ne \tilde{A}_0(r_1)[/math] и, ввиду того, что должно выполняться условие [math]A_1(0) + A_1(1) = A_0(r_1)[/math], получаем, что [math]A_1[/math] тоже будет неправильное, т.е. некоторое [math]\tilde{A}_1[/math].

Шаг 2.

...

Шаг [math]n[/math].

С вероятностью [math]1 - d / p : A_{n-1}(r_n) \ne \tilde{A}_{n-1}(r_n)[/math], и потому Verifier получит не [math]A_n[/math], а [math]\tilde{A}_n[/math].

Из этого процесса заметим, что с вероятностью большей либо равной [math](1 - d / p) ^ n[/math] мы дойдем до последнего шага и будем имееть [math]\tilde{A}_n[/math] вместо [math]A_n[/math]. Так как на шаге [math]n[/math] Verifier вычисляет [math]A_n[/math] и проверяет значение, то Verifier вернет false.

Так как мы хотим сделать вероятность возврата false большую либо равную [math]2/3[/math], то выберем [math]k_p[/math] так, чтобы [math](1-d/k_p)^n \ge 2/3[/math]. Возьмем [math]k_p = 3 d \cdot n[/math]. Заметим, что длина [math]k_p[/math] есть [math]poly(|input|)[/math]. Из разложения функции по Тейлору получаем: [math](1-d/k_p)^n = (1 - 1/(3n))^n = 1 - 1/3 + \frac{n(n - 1)}{2 (3n)^2} - \frac{n(n-1)(n-2)}{6 (3n)^3} + ... \ge[/math][math]\ge 2/3 + \frac{n(n-1)}{n^2}(\frac{1}{2 \cdot 3^2} - \frac{1}{6 \cdot 3^3}) + ... \ge 2/3[/math].

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