| Определение: |
| [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 PSPACE-complete[/math] необходимо показать что:
| Лемма (1): |
[math]TQBF \in PSPACSE[/math] |
| Доказательство: |
| [math]\triangleright[/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] \forall L \in PS \Rightarrow L \leq_p TQBF[/math] |
| Доказательство: |
| [math]\triangleright[/math] |
|
Рассмотрим какой-то язык [math]L \in PSPACE[/math]. Построим функцию [math]f : \forall x \in L \Leftrightarrow f(x) \in TQBF[/math]
Так как [math]L \in PSPACE[/math], то существует какая-то детерминированная машина Тьюринга [math]M[/math], которая его распознаёт за полиномиальное время на ленте полиномиального размера.
Пусть [math]I[/math] — мгновенное описание [math]M[/math], тогда выражение [math]\exists I[/math] обозначает [math] ( \exists x_1 )\land( \exists x_2 )\land\dots\land( \exists x_n ) [/math], где [math]\{x_i\}[/math] — все переменные мгновенного описания [math]M[/math]. Теперь рассмотрим два мгновенных описание [math]M : A[/math] и [math]B[/math]. Напишем полиномиальную рекурсивную функцию [math]\phi(A, B, t)[/math], которая будет переводить утверждение [math]A\vdash^tB[/math] в TQBF.
[math]\phi(A, B, t) = (\exists R) (\forall U) (\forall V) (\neg(\phi(U, V, t/2)) \rightarrow ((U \neq S \lor V \neq R) \land (U \neq R \lor V \neq S))[/math] |
| [math]\triangleleft[/math] |
