68
правок
Изменения
м
Нет описания правки
|statement=<tex>\mathrm{TQBF} \in \mathrm{PS}</tex>.
|proof=Чтобы доказать это, просто приведём программу <tex>solve</tex>, решающую булеву формулу с кванторами на <tex>O(n)</tex> дополнительной памяти и работающую за конечное время.
<tex>solve(k, Q_k x_k Q_1 x_1 \ldots Q_n x_n \phi(x_kx_1, \ldots, x_n))</tex> '''if''' <tex>k =n = n</tex> '''if''' <tex>Q_k = \forall</tex> '''return''' <tex>\phi(0) \land \phi(1)</tex> '''if''' <tex>Q_k = \exists</tex> '''return''' <tex>\phi(0) \lor \phi(1)</tex> '''if''' <tex>Q_k Q_1 = \forall</tex> '''return''' <tex>solve(Q_{k+12} x_{k+12} \ldots Q_n x_n \phi(0, x_{k+12}, \ldots, x_n)) \land solve(Q_{k+12} x_{k+12} \ldots Q_n x_n \phi(1, x_{k+12}, \ldots, x_n))</tex> '''if''' <tex>Q_k Q_1 = \exists</tex> '''return''' <tex>solve(Q_{k+12} x_{k+12} \ldots Q_n x_n \phi(0, x_{k+12}, \ldots, x_n)) \lor solve(Q_{k+12} x_{k+12} \dots Q_n x_n \phi(1, x_{k+12}, \ldots, x_n))</tex>
Эта программа требует <tex>O(n)</tex> дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — <tex>n</tex>.
}}
Общую длину получившейся формулы можно представить как <tex>L(t) = 2 L(t-1)+const</tex>. Заметим, что из-за умножения на 2 на каждом шаге рекурсии <tex>L(t)</tex> будет иметь экспоненциальный размер относительно <tex>t</tex>. Нас это не устраивает, так как нам необходимо полиномиальное сведение. Поэтому воспользуемся квантором <tex>\forall</tex> и перепишем её следующим образом:
<tex>\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{\phi(U, V, t-1) \lor \neg [(U = A \land V = R) \lor (U = R \land V = B)]\rightarrow \phi(U, V, t-1)\}</tex>.
Получившаяся в фигурых скобках формула верна только когда верно <tex>\phi(U, V, t-1)</tex> или <tex>\neg[(U = A \land V = R) \lor (U = R \land V = B)]</tex>. Это равносильно тому, что если существует такая промежуточная конфигурация <tex>R</tex>, что для любых конфигураций <tex>U</tex> и <tex>V</tex> либо верна формула <tex>\phi(Uиз того, V, t-1)</tex>, либо те конигурации для которых вызывается наша формула нас не интересуют. Если описания <tex>U</tex> и <tex>V</tex> что эти конфигурации нам подходятинтересны следует, то чтобы вся формула была верна необходимо чтобы что верно <tex>\phi(U, V, t-1)</tex> выполялось. А значит, конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>2^t</tex> шагов.
За один шаг рекурсии длина максимального пути между конфигурациями уменьшается в два раза. Поэтому общую длину получившейся формулы можно представить как <tex>L(t) = L(t-1)+const</tex>, где <tex>const = \|\exists R \,\forall U \,\forall V \, \{\| + \|\land [(U = A \land V = R) \lor (U = R \land V = B)]\}\|</tex>.
