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 PSPACE-complete[/math], необходимо показать, что эта задача принадлежит [math]PSPACE[/math] и что она [math]PSPACE[/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 , L \leq_p TQBF[/math]

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

[math]\triangleright[/math]

Рассмотрим какой-то язык [math]L \in PSPACE[/math]. Построим функцию [math]f \colon \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) (\exists x_2)\cdots(\exists x_n)[/math], где [math]\{x_i\}[/math] — все переменные мгновенного описания [math]M[/math]. Аналогично выражение [math] \forall I[/math] обозначает [math] (\forall x_1) (\forall x_2)\dots(\forall x_n)[/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) \ \{\phi(U, V, t/2) \lor [\neg(A = U \land R = V) \land \neg(R = U \land B = V)]\}[/math] Переменые [math] U [/math] и [math]V[/math] важно рассмотреть только в двух случаях: когда первое из них стартовое, второе — промежуточное, или первое — промежуточное, а второе — финишное. Поэтому для всех остальных вариантов выражение [math][\neg(A = U \land R = V) \land \neg(R = U \land B = V)][/math] будет истинно. Если [math]A = U \land R = V[/math] то, чтобы [math]\phi(A, B, t)[/math] было истинно, необходимо наличие такого мгновенного описания [math]R[/math], чтобы было выполненно утверждение: [math]A\vdash^{t/2}R[/math]. Если [math]R = U \land B = V[/math] то, нас интересует мгновенное описание [math]R[/math] такое, что [math]R\vdash^{t/2}B[/math]. Заметим, что размер функции [math]\phi(a, B, t)[/math] равен размеру [math]\phi(A, B, t/2)[/math] с константной добавкой [math](\exists R) (\forall U) (\forall V) \ \{\ * \lor [\neg(A = U \land B = R) \land \neg(A = R \land B = V)]\}[/math] . Теперь мы можем записать функцию [math]f(M, w)[/math], которая будет переводить ДМТ [math]M[/math] и слово на ленте [math]w[/math] в [math]TQBF[/math]. [math]f(M, w) = (\exists I_s) (\exists I_f) (x_{I_s, 0} = start \land x_{I_s, 1} = w[1] \land \dots \land x_{I_s, |w|} = w[|w|]) \land ((\exists i) x_{I_f, i} = finish) \land \phi(Start, Finish, 2^{log_2(c^{1+p(n)}})[/math] Докажем, что получившаяся булева формула с кванторами удовлетворима тогда и только тогда, когда [math]w \in L[/math]. Если [math]w \in L[/math], то стартовое и финишное состояние заданы корректно. Также из стартового состояния можно попасть в финишное за полиномиальное время. Если [math]w \not\in L[/math], то если мы зададим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.

[math]\triangleleft[/math]