PS-полнота языка верных булевых формул с кванторами (TQBF) — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 20: Строка 20:
 
|proof=Рассмотрим какой-то язык <tex>L \in PSPACE</tex>. Построим функцию <tex>f : \forall x \in L \Leftrightarrow f(x) \in TQBF</tex>
 
|proof=Рассмотрим какой-то язык <tex>L \in PSPACE</tex>. Построим функцию <tex>f : \forall x \in L \Leftrightarrow f(x) \in TQBF</tex>
 
Так как <tex>L \in PSPACE</tex>, то существует какая-то детерминированная машина Тьюринга <tex>M</tex>, которая его распознаёт за полиномиальное время на ленте полиномиального размера.
 
Так как <tex>L \in PSPACE</tex>, то существует какая-то детерминированная машина Тьюринга <tex>M</tex>, которая его распознаёт за полиномиальное время на ленте полиномиального размера.
Пусть <tex>I</tex> — мгновенное описание <tex>M</tex>, тогда выражение <tex>\exists I</tex> обозначает <tex> ( \exists x_1 )\land( \exists x_2 )\land\dots\land( \exists x_n ) </tex>, где <tex>\{x_i\}</tex> — все переменные мгновенного описания <tex>M</tex>. Теперь рассмотрим два мгновенных описание <tex>M : A</tex> и <tex>B</tex>. Напишем полиномиальную рекурсивную функцию <tex>\phi(A, B, t)</tex>, которая будет переводить утверждение <tex>A\vdash^tB</tex> в TQBF.  
+
Пусть <tex>I</tex> — мгновенное описание <tex>M</tex>, тогда выражение <tex>\exists I</tex> обозначает <tex> (\exists x_1) (\exists x_2)\cdots(\exists x_n)</tex>, где <tex>\{x_i\}</tex> — все переменные мгновенного описания <tex>M</tex>. Аналогично выражение <tex> \forall I</tex> обозначает <tex> (\forall x_1) (\forall x_2)\dots(\forall x_n)</tex>. Теперь рассмотрим два мгновенных описание <tex>M : A</tex> и <tex>B</tex>. Напишем полиномиальную рекурсивную функцию <tex>\phi(A, B, t)</tex>, которая будет переводить утверждение <tex>A\vdash^tB</tex> в TQBF.  
<tex>\phi(A, B, t) = (\exists R) (\forall U) (\forall V) (\neg(\phi(U, V, t/2)) \rightarrow ((U \neq S \lor V \neq R) \land (U \neq R \lor V \neq S))</tex>
+
 
 +
<tex>\phi(A, B, t) = (\exists R) (\forall U) (\forall V) (\neg\phi(U, V, t/2) \rightarrow [(U \neq S \lor V \neq R) \land (U \neq R \lor V \neq S)])</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>, то если мы задодим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.
 
}}
 
}}

Версия 15:05, 30 апреля 2012

Определение:
[math]TQBF[/math] расшивровывается как True Quantified Boolean Formula. Это язык верных булевых формул с кванторами. [math]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\}\}[/math]

Чтобы доказать, что [math]TQBF \in PSPACE-complete[/math] необходимо показать что:

Лемма (1):
[math]TQBF \in PSPACSE[/math]
Доказательство:
[math]\triangleright[/math]

Чтобы доказать это просто приведём программу, которая требует [math]O(n)[/math] дополнительной памяти и работает за конечное время.

[math]solve(Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n))[/math]
    if [math]Q_1 == \forall[/math]
        return [math]solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \land solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))[/math]
    if [math]Q_1 == \exists[/math]
        return [math]solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \lor solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))[/math]
Эта программа требует [math]O(n)[/math] дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — [math]n[/math]
[math]\triangleleft[/math]
Лемма (2):
[math] \forall L \in PS \Rightarrow L \leq_p TQBF[/math]
Доказательство:
[math]\triangleright[/math]

Рассмотрим какой-то язык [math]L \in PSPACE[/math]. Построим функцию [math]f : \forall x \in L \Leftrightarrow f(x) \in TQBF[/math] Так как [math]L \in PSPACE[/math], то существует какая-то детерминированная машина Тьюринга [math]M[/math], которая его распознаёт за полиномиальное время на ленте полиномиального размера. Пусть [math]I[/math] — мгновенное описание [math]M[/math], тогда выражение [math]\exists I[/math] обозначает [math] (\exists x_1) (\exists x_2)\cdots(\exists x_n)[/math], где [math]\{x_i\}[/math] — все переменные мгновенного описания [math]M[/math]. Аналогично выражение [math] \forall I[/math] обозначает [math] (\forall x_1) (\forall x_2)\dots(\forall x_n)[/math]. Теперь рассмотрим два мгновенных описание [math]M : A[/math] и [math]B[/math]. Напишем полиномиальную рекурсивную функцию [math]\phi(A, B, t)[/math], которая будет переводить утверждение [math]A\vdash^tB[/math] в TQBF.

[math]\phi(A, B, t) = (\exists R) (\forall U) (\forall V) (\neg\phi(U, V, t/2) \rightarrow [(U \neq S \lor V \neq R) \land (U \neq R \lor V \neq S)])[/math]

Заметим, что размер функции [math]\phi(a, B, t)[/math] равен размеру [math]\phi(A, B, t/2)[/math] с константной добавкой. Теперь мы можем записать функцию [math]f(M, w)[/math] которая будет переводить ДМТ [math]M[/math] и слово на ленте [math]w[/math] в [math]TQBF[/math].

[math]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)}})[/math] Докажем, что получившаяся булева формула с кванторами удовлетворима тогда и только тогда, когда [math]w \in L[/math] Если [math]w \in L[/math], то стартовое и финишное состояние задано корректно. Также из стартового состояния можно попасть в финишное за полиномиальное время.

Если [math]w \not\in L[/math], то если мы задодим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.
[math]\triangleleft[/math]