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

2012-06-01T16:40:25Z

91.122.24.175:

{{Определение
|definition=<tex>TQBF</tex> расшифровывается как True Quantified Boolean Formula. Это язык верных булевых формул с кванторами.
<tex>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\}\}</tex>
}}
Чтобы доказать, что <tex>TQBF \in PSPACE-complete</tex>, необходимо показать, что эта задача принадлежит <tex>PSPACE</tex> и что она <tex>PSPACE</tex>-трудная.
{{Лемма
|about=1
|statement=<tex>TQBF \in PSPASE</tex>
|proof=Чтобы доказать это, просто приведём программу <tex>solve</tex>, решающую булеву формулу с кванторами на <tex>O(n)</tex> дополнительной памяти и работающую за конечное время.
<tex>solve(Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n))</tex>
'''if''' <tex>Q_1 == \forall</tex>
'''return''' <tex>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))</tex>
'''if''' <tex>Q_1 == \exists</tex>
'''return''' <tex>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))</tex>
Эта программа требует <tex>O(n)</tex> дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — <tex>n</tex>.
}}
{{Лемма
|about=2
|statement=<tex> \forall L \in PS , L \leq_p TQBF</tex>
|proof=Рассмотрим какой-то язык <tex>L \in PSPACE</tex>.
Построим функцию <tex>f \colon \forall x \in L \Leftrightarrow f(x) \in TQBF</tex>.
Так как <tex>L \in PSPACE</tex>, то существует какая-то детерминированная машина Тьюринга <tex>M</tex>, которая его распознаёт за полиномиальное от размера входа время.
Пусть <tex>I</tex> — мгновенное описание <tex>M</tex>, тогда выражение <tex>\exists I</tex> обозначает <tex> (\exists x_1) (\exists x_2)\cdots(\exists x_n)</tex>, где <tex>\{x_i\}</tex> — все переменные мгновенного описания <tex>M</tex>. Аналогично выражение <tex> \forall I</tex> обозначает <tex> (\forall x_1) (\forall x_2)\dots(\forall x_n)</tex>. Теперь рассмотрим два мгновенных описание <tex>M: A</tex> и <tex>B</tex>. Напишем рекурсивную функцию <tex>\phi(A, B, t)</tex>, которая будет переводить утверждение <tex>A\vdash^tB</tex> в TQBF за полиномиальное относительно длины входа время.

<tex>\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)]\}</tex>
:Переменые <tex> U </tex> и <tex>V</tex> важно рассмотреть только в двух случаях: когда первое из них стартовое, второе — промежуточное, или первое — промежуточное, а второе — финишное. Поэтому для всех остальных вариантов выражение <tex>[\neg(A = U \land R = V) \land \neg(R = U \land B = V)]</tex> будет истинно. Если <tex>A = U \land R = V</tex> то, чтобы <tex>\phi(A, B, t)</tex> было истинно, необходимо наличие такого мгновенного описания <tex>R</tex>, чтобы было выполненно утверждение: <tex>A\vdash^{t/2}R</tex>. Если <tex>R = U \land B = V</tex> то, нас интересует мгновенное описание <tex>R</tex> такое, что <tex>R\vdash^{t/2}B</tex>.
Заметим, что размер функции <tex>\phi(A, B, t)</tex> равен размеру <tex>\phi(A, B, t/2)</tex> с константной добавкой <tex>(\exists R) (\forall U) (\forall V) \ \{\ * \lor [\neg(A = U \land B = R) \land \neg(A = R \land B = V)]\}</tex> .
Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в <tex>TQBF</tex>.

<tex>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)}})</tex>

Докажем, что получившаяся булева формула с кванторами удовлетворима тогда и только тогда, когда <tex>w \in L</tex>.

Если <tex>w \in L</tex>, то стартовое и финишное состояние заданы корректно. Также из стартового состояния можно попасть в финишное за полиномиальное время.

Если <tex>w \not\in L</tex>, то если мы зададим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.
}}

[[Категория: Теория сложности]]

Викиконспекты - Вклад участника [ru]

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