PS-полнота языка верных булевых формул с кванторами (TQBF)

Определение:

[math]TQBF[/math] расшифровывается как True Quantified Boolean Formula. Это язык верных булевых формул с кванторами. [math]TQBF=\{Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n), Q_i \in \{\forall, \exists\}\}[/math].

Чтобы доказать, что [math]TQBF \in \mathrm{PSC}[/math], необходимо показать, что [math]TQBF \in \mathrm{PSH}[/math] и [math]TQBF \in \mathrm{PS}[/math].

Лемма (1):

[math]TQBF \in \mathrm{PS}[/math].

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

[math]\triangleright[/math]

Чтобы доказать это, просто приведём программу [math]solve[/math], решающую булеву формулу с кванторами на [math]O(n)[/math] дополнительной памяти и работающую за конечное время. [math]solve(Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n))[/math] if [math]Q_1 = \forall[/math] return [math]solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \land solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))[/math] if [math]Q_1 = \exists[/math] return [math]solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \lor solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))[/math] Эта программа требует [math]O(n)[/math] дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — [math]n[/math].

[math]\triangleleft[/math]

Лемма (2):

[math]TQBF \in \mathrm{PSH}[/math].

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

[math]\triangleright[/math]

Рассмотрим язык [math]L \in \mathrm{PS}[/math]. Построим такую функцию [math]f[/math], что [math]x \in L \Leftrightarrow f(x) \in TQBF[/math] и [math]T(f, x) \le p(|x|)[/math]. Так как [math]L \in \mathrm{PS}[/math], то существует детерминированная машина Тьюринга [math]M[/math], распознающая его с использованием памяти полиномиального размера. Пусть [math]I[/math] — конфигурация [math]M[/math]. Размер конфигурации есть [math]r(n)[/math], где [math]n[/math] — длина входа, [math]r[/math] — некоторый полином. Тогда выражение [math]\exists I[/math] обозначает [math] \exists x_0^I \, \exists x_1^I \dots \exists x_{r(n)}^I[/math], где [math]\{x_i^I\}[/math] — все переменные конфигурации [math]I[/math]. Аналогично выражение [math] \forall I[/math] обозначает [math] \forall x_0^I \, \forall x_1^I \dots \forall x_{r(n)}^I[/math]. Всего конфигураций у ДМТ [math]M \, 2^{O(p(n))}[/math], где [math]p[/math] — некоторый полином. Рассмотрим функцию [math]\phi(A, B, t)[/math], проверяющую следующее условие: конфигурация [math]B[/math] достижима из конфигурации [math]A[/math] не более, чем за [math]2^t[/math] шагов. [math]\phi(A, B, 0) = (A = B) \lor (A \vdash B)[/math]. [math]\phi(A, B, t) = \exists R \, \phi(A, R, t-1) \land \phi(R, B, t-1)[/math]. Заметим, что данная формула имеет экспоненциальный размер, поэтому воспользуемся квантором [math]\forall[/math] и перепишем её следующим образом: [math]\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{\phi(U, V, t-1) \lor [\neg(U = A \land V = R) \land \neg(U = R \land V = B)]\}[/math]. Размер полученной функции [math]\phi(A, B, t)[/math] полиномиален относительно [math]n[/math]. Теперь мы можем записать функцию [math]f(M, w)[/math], которая будет переводить ДМТ [math]M[/math] и слово на ленте [math]w[/math] в формулу из [math]TQBF[/math]. [math]f(M, w) = (\exists I_{st}) (\exists I_{fin}) (x_0^{I_{st}} = start \land x_1^{I_{st}} = w[1] \land \dots \land x_{|w|}^{I_{st}} = w[|w|]) \land (\exists i \, x_i^{I_{fin}} = finish) \land \phi(I_{st}, I_{fin}, log_2(2^{O(p(n))})))[/math]. Докажем, что сведение [math]f[/math] корректно. Если [math]w \in L[/math], то существует путь из стартовой конфигурации в финишную, причём длины не более, чем [math]2^{O(p(n))}[/math], а значит формула [math]\phi[/math] верна. Если формула [math]f(M, w)[/math] оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем [math]2^{O(p(n))}[/math]. Значит, ДМТ [math]M[/math] допускает слово [math]w[/math]. Тогда [math]w \in L[/math]. Таким образом, [math]TQBF \in \mathrm{PSH}[/math].

[math]\triangleleft[/math]