Изменения
Нет описания правки
<tex>\mathrm{TQBF}=\{Q_1 x_1 Q_2 x_2 \ldots Q_n x_n \phi(x_1, x_2, \dots, x_n), Q_i \in \{\forall, \exists\}\}</tex>.
}}
{{Определение|definition=<tex>Quantified Boolean Formula</tex> это пропозициональная формула с кванторами. Кванторы для каждой переменной записываются в начале выражения.}}
{{Лемма
|about=1
|statement=<tex>\mathrm{TQBF} \in \mathrm{PS}</tex>.
|proof=Чтобы доказать это, просто приведём программу <tex>solve</tex>, решающую булеву формулу с кванторами на <tex>O(n)</tex> дополнительной памяти и работающую за конечное время.
<tex>solve(Q_1 Q_k x_k \ldots Q_n x_n \phi(x_1 Q_2 , x_2 , \ldots Q_n , x_n ))</tex> '''if''' <tex>k == n</tex> '''return''' <tex>\phi(x_1, x_2, \ldots, x_n))</tex> '''if''' <tex>Q_1 Q_k = \forall</tex> '''return''' <tex>solve(Q_2 x_2 Q_{k+1} x_{k+1} \ldots Q_n x_n \phi(0, x_2x_{k+1}, \ldots, x_n)) \land solve(Q_2 x_2 Q_{k+1} x_{k+1} \ldots Q_n x_n \phi(1, x_2x_{k+1}, \ldots, x_n))</tex> '''if''' <tex>Q_1 Q_k = \exists</tex> '''return''' <tex>solve(Q_2 x_2 Q_{k+1} x_{k+1} \ldots Q_n x_n \phi(0, x_2x_{k+1}, \ldots, x_n)) \lor solve(Q_2 x_2 Q_{k+1} x_{k+1} \dots Q_n x_n \phi(1, x_2x_{k+1}, \ldots, x_n))</tex>
Эта программа требует <tex>O(n)</tex> дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — <tex>n</tex>.
}}
