Изменения

|definition=<tex>\mathrm{TQBF}</tex> расшифровывается как '''True Quantified Boolean Formula. Это '''. Это язык верных булевых формул с кванторами'''.<br/><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> — это пропозициональная формула с кванторами. Кванторы для каждой переменной записываются в начале выражения.

|statement=<tex>\mathrm{TQBF } \in \mathrm{PS}</tex>.

<tex>solve(Q_1 x_1 Q_2 x_2 \ldots Q_n x_n \phi(x_1, x_2, \ldots, x_n))</tex> '''if''' n == 0 '''return''' <tex>\phi</tex>

'''return''' <tex>solve(Q_2 x_2 Q_{2} x_{2} \ldots Q_n x_n \phi(0, x_2x_{2}, \ldots, x_n)) \land solve(Q_2 x_2 Q_{2} x_{2} \ldots Q_n x_n \phi(1, x_2x_{2}, \ldots, x_n))</tex>

'''return''' <tex>solve(Q_2 x_2 Q_{2} x_{2} \ldots Q_n x_n \phi(0, x_2x_{2}, \ldots, x_n)) \lor solve(Q_2 x_2 Q_{2} x_{2} \dots Q_n x_n \phi(1, x_2x_{2}, \ldots, x_n))</tex>

|statement=<tex>\mathrm{TQBF } \in \mathrm{PSH}</tex>.

Построим такую функцию <tex>f</tex>, что <tex>x \in L \Leftrightarrow f(x) \in \mathrm{TQBF}</tex> и <tex>T(f, x) \le p(|x|)</tex>, где <tex>p</tex> — полином.

Так как <tex>L \in \mathrm{PS}</tex>, то существует детерминированная машина Тьюринга <tex>M</tex>, распознающая его с использованием памяти полиномиального размера. Пусть Будем считать, что длина ленты машины <tex>\Omega = |\Sigma \cup Q|M</tex>есть <tex>r(n)</tex>, где <tex>r</tex> — полином, а <tex>n</tex> — длина входа.

Пусть <tex>w = |\Sigma \cup Q|</tex>, <tex>I</tex> — конфигурация <tex>M</tex>. Размер Конфигурация задаётся позицией и содержанием рабочей ленты. Введём обозначение <tex>x_{I,i,c}</tex> — в конфигурации равен <tex>\Omega nI</tex> на <tex>i</tex>-том месте стоит символ <tex>c</tex>, где . Тогда размер конфигурации равен <tex>w r(n)</tex> длина входа. Тогда Следовательно всего конфигураций <tex>2^{\Omega w r(n)}</tex>.

Введём обозначение <tex>x_{I,i,c}</tex> — в конфигурации <tex>I</tex> на <tex>i</tex>-том месте стоит символ <tex>c</tex>.Тогда выражение Под выражением <tex>\exists I</tex> обозначает будем понимать <tex> \exists x_{I,1,c_1} \, \exists x_{I,1,c_2} \ldots \exists x_{I,1,c_\Omegac_w} \, \exists x_{I,2,c_1} \ldots</tex> Аналогично выражение <tex> \forall I</tex> обозначает <tex> \forall x_{I,1,c_1} \, \forall x_{I,1,c_2} \ldots \forall x_{I,1,c_\Omegac_w} \, \forall x_{I,2,c_1} \ldots</tex>

<tex>\phi(A, B, t) = \exists R \, [\phi(A, R, t-1) \land \phi(R, B, t-1)]</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) \land \neglor (U = R \land V = B)]\rightarrow \phi(U, V, t-1)\}</tex>.

Размер полученной функции Получившаяся формула верна, если существует такая промежуточная конфигурация <tex>R</tex>, что для любых конфигураций <tex>U</tex> и <tex>V</tex> из того, что эти конфигурации нам интересны следует, что верно <tex>\phi(AU, BV, t-1)</tex> полиномиален относительно . А значит, конфигурация <tex>B</tex>nдостижима из конфигурации <tex>A</tex> не более, чем за <tex>2^t</tex>шагов.

Теперь мы можем записать функцию За один шаг рекурсии длина максимального пути между конфигурациями уменьшается в два раза. Поэтому общую длину получившейся формулы можно представить как <tex>fL(M, wt) = L(t-1)+const</tex>, которая будет переводить ДМТ где <tex>Mconst = \|\exists R \,\forall U \,\forall V \, \{\| + \|\land [(U = A \land V = R) \lor (U = R \land V = B)]\}\|</tex> и слово на ленте .Следовательно, размер полученной функции <tex>w\phi(A, B, t)</tex> в формулу из полиномиален относительно <tex>TQBFt</tex>.

Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в формулу из <tex>\mathrm{TQBF}</tex>. <tex>f(M, w) = \exists S \, \exists F \, (S - start) \land (F - accept) \land \phi(S, F, log_2(2^{\Omega w r(n)})))</tex>.

<tex>S - start = x_{S, 1, w[1]} \land x_{S, 2, w[2]} \land \ldots \land x_{S, |w|, w[|w|]} \land x_{S, |w| + 1, B} \ldots \land x_{S, \Omega r(n) , B}</tex>.

<tex>F - accept = x_{SF, |w| + 1, \#_y} \lor \ldots \lor x_{SF, \Omegar(n), \#_y}</tex>.

Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, причём длины не более, чем <tex>2^{\Omega w r(n)}</tex>, а значит формула <tex>\phif(M, w)</tex> верна.

Если формула <tex>f(M, w)</tex> оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем <tex>2^{\Omega w r(n)}</tex>. Значит, ДМТ <tex>M</tex> допускает слово <tex>w</tex>. Тогда <tex>w \in L</tex>. Таким образом, <tex>\mathrm{TQBF} \in \mathrm{PSH}</tex>.}}

Таким образом, {{Теорема|statement=<tex>\mathrm{TQBF } \in \mathrm{PSHPSC}</tex>.|proof=Доказательство непосредственно следует из лемм.