Изменения

|definition=<tex>\mathrm{TQBF}</tex> расшифровывается как '''True Quantified Boolean Formula'''. Это язык верных булевых формул с кванторами.<br/><tex>\mathrm{TQBF}=\{Q_1 x_1 Q_2 x_2 \cdots 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 PSPASE\mathrm{PS}</tex>.

<tex>solve(Q_1 x_1 Q_2 x_2 \cdots ldots Q_n x_n \phi(x_1, x_2, \dotsldots, x_n))</tex> '''if''' n == 0 '''return''' <tex>\phi</tex> '''if''' <tex>Q_1 == \forall</tex> '''return''' <tex>solve(Q_2 x_2 Q_{2} x_{2} \cdots ldots Q_n x_n \phi(0, x_2x_{2}, \dotsldots, x_n)) \land solve(Q_2 x_2 Q_{2} x_{2} \cdots ldots Q_n x_n \phi(1, x_2x_{2}, \dotsldots, x_n))</tex> '''if''' <tex>Q_1 == \exists</tex> '''return''' <tex>solve(Q_2 x_2 Q_{2} x_{2} \cdots ldots Q_n x_n \phi(0, x_2x_{2}, \dotsldots, x_n)) \lor solve(Q_2 x_2 Q_{2} x_{2} \cdots dots Q_n x_n \phi(1, x_2x_{2}, \dotsldots, x_n))</tex>

|statement=<tex> \forall L mathrm{TQBF} \in PS , L \leq_p TQBFmathrm{PSH}</tex>.|proof=Рассмотрим какой-то язык <tex>L \in PSPACE\mathrm{PS}</tex>. Построим такую функцию <tex>f \colon \forall </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 PSPACE\mathrm{PS}</tex>, то существует какая-то детерминированная машина Тьюринга <tex>M</tex>, которая распознающая его распознаёт за полиномиальное от с использованием памяти полиномиального размера . Будем считать, что длина ленты машины <tex>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>I</tex> на <tex>i</tex>-том месте стоит символ <tex>c</tex>. Тогда размер конфигурации равен <tex>w r(n)</tex>. Следовательно всего конфигураций <tex>2^{w r(n)}</tex>. Под выражением <tex>\exists I</tex> будем понимать <tex> \exists x_{I, тогда 1,c_1} \, \exists x_{I,1,c_2} \ldots \exists x_{I,1,c_w} \, \exists x_{I,2,c_1} \ldots</tex> Аналогично выражение <tex>\exists forall I</tex> обозначает <tex> \forall x_{I,1,c_1} \, \forall x_{I,1,c_2} \ldots \forall x_{I,1,c_w} \, \forall x_{I,2,c_1} \ldots</tex> Рассмотрим функцию <tex>\phi(A, B, t)</tex>, проверяющую следующее условие: конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>2^t</tex> шагов. <tex>\exists x_1phi(A, B, 0) = (A = B) \lor (A \exists x_2vdash B)</tex>. <tex>\cdotsphi(A, B, t) = \exists x_nR \, [\phi(A, R, t-1)\land \phi(R, B, t-1)]</tex>. Общую длину получившейся формулы можно представить как <tex>L(t) = 2 L(t-1)+const</tex>. Заметим, где что из-за умножения на 2 на каждом шаге рекурсии <tex>\{x_i\}L(t)</tex> — все переменные мгновенного описания будет иметь экспоненциальный размер относительно <tex>Mt</tex>. Аналогично выражение Нас это не устраивает, так как нам необходимо полиномиальное сведение. Поэтому воспользуемся квантором <tex> \forall I</tex> обозначает и перепишем её следующим образом: <tex> \phi(A, B, t) = \exists R \,\forall U \,\forall x_1V \, \{[(U = A \land V = R) \lor (U = R \forall x_2land V = B)] \dotsrightarrow \phi(U, V, t-1)\forall x_n)}</tex>. Теперь рассмотрим два мгновенных описание  Получившаяся формула верна, если существует такая промежуточная конфигурация <tex>R</tex>, что для любых конфигураций <tex>M: AU</tex> и <tex>BV</tex>. Напишем рекурсивную функцию из того, что эти конфигурации нам интересны следует, что верно <tex>\phi(AU, BV, t-1)</tex>. А значит, которая будет переводить утверждение конфигурация <tex>B</tex> достижима из конфигурации <tex>A\vdash</tex> не более, чем за <tex>2^tBt</tex> в TQBF за полиномиальное относительно длины входа времяшагов.

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

Теперь мы можем записать функцию <tex>f(M, w) = (\exists I_s) (\exists I_f) (x_{I_s</tex>, 0} = start \land x_{I_s, 1} = которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w[1] \land \dots \land x_{I_s, |w|} = w[|w|]) \land ((\exists i) x_{I_f, i} = finish) \land </tex> в формулу из <tex>\phi(Start, Finish, 2^{log_2(c^mathrm{1+p(n)}TQBF})</tex>.

Докажем, что получившаяся булева формула с кванторами удовлетворима тогда и только тогда, когда <tex>f(M, w ) = \exists S \, \exists F \, (S - start) \land (F - accept) \in Lland \phi(S, F, log_2(2^{w r(n)})))</tex>.

Выражения <tex>S - start</tex> и <tex>F - accept</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, r(n) , B}</tex>. <tex>F - accept = x_{F, 1, \#_y} \lor \ldots \lor x_{F, r(n), \#_y}</tex>.  Докажем, что сведение <tex>f</tex> корректно. Если <tex>w \in L</tex>, то стартовое и финишное состояние заданы корректносуществует путь из стартовой конфигурации в финишную, длины не более, чем <tex>2^{w r(n)}</tex>, а значит формула <tex>f(M, w)</tex> верна. Также  Если формула <tex>f(M, w)</tex> оказалась верна, то существует путь из стартового состояния можно попасть стартовой конфигурации в финишное за полиномиальное времяфинишную длины не более, чем <tex>2^{w r(n)}</tex>. Значит, ДМТ <tex>M</tex> допускает слово <tex>w</tex>. Тогда <tex>w \in L</tex>. Таким образом, <tex>\mathrm{TQBF} \in \mathrm{PSH}</tex>. }}

Если {{Теорема|statement=<tex>w \notmathrm{TQBF} \in L\mathrm{PSC}</tex>, то если мы зададим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.|proof=Доказательство непосредственно следует из лемм.