68
правок
Изменения
м
Нет описания правки
{{Определение
|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 PSPACSE</tex>
|proof=Чтобы доказать это , просто приведём программу, которая требует <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>
Заметим, что размер функции <tex>\phi(a, B, t)</tex> равен размеру <tex>\phi(A, B, t/2)</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>, то если мы задодим зададим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.
}}
