Лемма о соотношении coNP и IP

Материал из Викиконспекты
Перейти к: навигация, поиск
Определение:
[math]\#SAT=\{\langle \varphi, k \rangle | \varphi[/math] имеет ровно [math]k[/math] удовлетворяющих наборов [math]\}[/math].


Введём понятие арифметизации булевых формул. Пусть нам дана формула [math]\phi(x_1 \ldots x_m)[/math]. Сделаем следующие преобразования и получим формулу [math]A_\phi(x_1, x_2, \ldots, x_m)[/math]:

  1. [math] x_i \to x_i[/math];
  2. [math] \lnot x \to 1 - x[/math];
  3. [math]\Phi \land \Psi \to A_\Phi \cdot A_\Psi[/math];
  4. [math]\Phi \lor \Psi \to 1 - (1 - A_\Phi) \cdot (1 - A_\Psi)[/math].

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

Лемма (1):
[math]\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)[/math].
Лемма (2):
[math]\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phi(x_1, \ldots, x_m)=k \iff \langle\phi,k\rangle \in \#SAT[/math].
Доказательство:
[math]\triangleright[/math]
Следует из леммы (1).
[math]\triangleleft[/math]


Лемма (3):
[math]\#SAT \in \mathrm{IP}[/math].
Доказательство:
[math]\triangleright[/math]

Для доказательства леммы построим программы Verifier и Prover из определения класса [math]\mathrm{IP}[/math].

Сперва арифметизуем формулу [math]\phi[/math]. Пусть полученный полином [math]A(x_1, x_2, ..., x_m)[/math] имеет степень [math]d[/math].

По лемме (2) вместо условия [math]\langle \phi, k \rangle \in \#SAT[/math], можно проверять условие [math]\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phi(x_1, \ldots, x_m)=k[/math].

Приступим к описанию Verifier'а.

Шаг 0

Запросим у Prover'а такое простое число [math]p[/math], что [math]max(2^m+1, k_p) \le p \le 2 \cdot max(2^m+1, k_p)[/math]. Проверим простоту [math]p[/math] и условие [math]max(2^m+1, k_p) \le p \le 2 \cdot max(2^m+1, k_p)[/math] (константу [math]k_p[/math] определим позднее). Как мы знаем, [math]Primes \in \mathrm{P}[/math], следовательно на эти операции у Verifier'а уйдёт полиномиальное от размера входа время.

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

Попросим Prover 'а прислать Verifier 'у формулу [math]A_0(x_1)= \sum\limits_{x_2 = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(x_1, x_2, ..., x_m)[/math]. Заметим, что размер формулы [math]A_0(x_1)[/math] будет полином от длины входа Verifier 'а, так как [math]A_0(x_1)[/math] полином от одной переменной степени не выше, чем [math]d[/math], а значит его можно представить в виде [math]A_0(x) = \sum\limits_{i = 0}^{d} C_i \cdot x ^ i[/math].

Проверим следующее утверждение: [math]A_0(0) + A_0(1) = k[/math] (здесь и далее под словом «проверим» будем подразумевать следующее: если утверждение верно, Verifier продолжает свою работу, иначе он прекращает свою работу и возвращет false).

Шаг i

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

Пусть [math]A_i(x_{i+1}) = \sum\limits_{x_{i+2} = 0}^{1}\ldots\sum\limits_{x_m = 0}^{1} A(r_1,\ldots, r_i, x_{i+1}, ..., x_m)[/math].

Попросим Prover 'а прислать Verifier 'у формулу [math]A_i(x_{i+1})[/math]. Проверим следующее утверждение: [math]A_i(0) + A_i(1) = A_{i-1}(r_i)[/math].

Шаг m

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

Попросим программу Prover прислать Verifier 'у значение [math]A_m()= A(r_1, r_2, ..., r_m)[/math].

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

Возвращаем true.
[math]\triangleleft[/math]


Лемма (4):
[math]\mathrm{coNP} \subset \mathrm{IP}[/math].
Доказательство:
[math]\triangleright[/math]

Сведём язык [math]TAUT[/math] к языку [math]\#SAT[/math] следующим образом: [math]\phi \mapsto \langle \phi, 2^k \rangle [/math], где [math]k[/math] — количество различных переменных в формуле [math]\phi[/math].

Очевидно, что [math]\phi \in TAUT \iff \langle \phi, 2^k \rangle \in \#SAT[/math].

По лемме (3) [math]\#SAT \in \mathrm{IP}[/math]. Тогда [math]TAUT \in \mathrm{IP}[/math]. Так как [math]TAUT \in \mathrm{coNPC}[/math], то [math]\mathrm{coNP} \subset \mathrm{IP}[/math].
[math]\triangleleft[/math]