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

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 31: Строка 31:
 
Под выражением <tex>\exists I</tex> будем понимать <tex> \exists x_{I,1,c_1} \, \exists x_{I,1,c_2} \ldots \exists x_{I,1,c_\Omega}  \, \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_\Omega}  \, \forall x_{I,2,c_1} \ldots</tex>
 
Под выражением <tex>\exists I</tex> будем понимать <tex> \exists x_{I,1,c_1} \, \exists x_{I,1,c_2} \ldots \exists x_{I,1,c_\Omega}  \, \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_\Omega}  \, \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>\phi(A, B, t)</tex>, проверяющую следующее условие: конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>t</tex> шагов.
  
 
<tex>\phi(A, B, 0) = (A = B) \lor (A \vdash B)</tex>.
 
<tex>\phi(A, B, 0) = (A = B) \lor (A \vdash B)</tex>.
Строка 41: Строка 41:
 
<tex>\phi(A, B, t) =  \exists R \,\forall U \,\forall V \, \{\phi(U, V, \lceil t/2\rceil) \nrightarrow \neg[(U = A \land V = R) \lor (U = R \land V = B)]\}</tex>.
 
<tex>\phi(A, B, t) =  \exists R \,\forall U \,\forall V \, \{\phi(U, V, \lceil t/2\rceil) \nrightarrow \neg[(U = A \land V = R) \lor (U = R \land V = B)]\}</tex>.
  
 +
Получившаяся формула верна только когда верно <tex>\phi(U, V, \lceil t/2\rceil)</tex> и ложно <tex>\neg[(U = A \land V = R) \lor (U = R \land V = B)]</tex>. Это равносильно тому, что <tex>V</tex> достижима из <tex>U</tex> не более, чем за <tex>\lceil t/2\rceil</tex> шагов, и либо <tex>U = A \land V = R</tex>, либо <tex>U = R \land V = B</tex>. А если верно и то, и другое, то конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>t</tex> шагов.
 
Размер полученной функции <tex>\phi(A, B, t)</tex> полиномиален относительно <tex>n</tex>.
 
Размер полученной функции <tex>\phi(A, B, t)</tex> полиномиален относительно <tex>n</tex>.
  

Версия 18:14, 24 июня 2012

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


Определение:
[math]Quantified Boolean Formula[/math] это пропозициональная формула с кванторами. Кванторы для каждой переменной записываются в начале выражения.
Лемма (1):
[math]\mathrm{TQBF} \in \mathrm{PS}[/math].
Доказательство:
[math]\triangleright[/math]

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

[math]solve(Q_k x_k \ldots Q_n x_n \phi(x_k, \ldots, x_n))[/math]
    if [math]k \gt  n[/math]
        return [math]\phi[/math]
    if [math]Q_k = \forall[/math]
        return [math]solve(Q_{k+1} x_{k+1} \ldots Q_n x_n \phi(0, x_{k+1}, \ldots, x_n)) \land solve(Q_{k+1} x_{k+1} \ldots Q_n x_n \phi(1, x_{k+1}, \ldots, x_n))[/math]
    if [math]Q_k = \exists[/math]
        return [math]solve(Q_{k+1} x_{k+1} \ldots Q_n x_n \phi(0, x_{k+1}, \ldots, x_n)) \lor solve(Q_{k+1} x_{k+1} \dots Q_n x_n \phi(1, x_{k+1}, \ldots, x_n))[/math]
Эта программа требует [math]O(n)[/math] дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — [math]n[/math].
[math]\triangleleft[/math]
Лемма (2):
[math]\mathrm{TQBF} \in \mathrm{PSH}[/math].
Доказательство:
[math]\triangleright[/math]

Рассмотрим язык [math]L \in \mathrm{PS}[/math]. Построим такую функцию [math]f[/math], что [math]x \in L \Leftrightarrow f(x) \in \mathrm{TQBF}[/math] и [math]T(f, x) \le p(|x|)[/math], где [math]p[/math] — полином.

Так как [math]L \in \mathrm{PS}[/math], то существует детерминированная машина Тьюринга [math]M[/math], распознающая его с использованием памяти полиномиального размера. Будем считать, что длина ленты машины [math]M[/math] есть [math]r(n)[/math], где [math]r[/math] — полином, а [math]n[/math] — длина входа.

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

Под выражением [math]\exists I[/math] будем понимать [math] \exists x_{I,1,c_1} \, \exists x_{I,1,c_2} \ldots \exists x_{I,1,c_\Omega} \, \exists x_{I,2,c_1} \ldots[/math] Аналогично выражение [math] \forall I[/math] обозначает [math] \forall x_{I,1,c_1} \, \forall x_{I,1,c_2} \ldots \forall x_{I,1,c_\Omega} \, \forall x_{I,2,c_1} \ldots[/math]

Рассмотрим функцию [math]\phi(A, B, t)[/math], проверяющую следующее условие: конфигурация [math]B[/math] достижима из конфигурации [math]A[/math] не более, чем за [math]t[/math] шагов.

[math]\phi(A, B, 0) = (A = B) \lor (A \vdash B)[/math].

[math]\phi(A, B, t) = \exists R \, [\phi(A, R, t-1) \land \phi(R, B, t-1)][/math].

Заметим, что данная формула имеет экспоненциальный размер, так как за один шаг рекурсии длина пути уменьшается на одни, а размер формулы удваивается. Поэтому воспользуемся квантором [math]\forall[/math] и перепишем её следующим образом:

[math]\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{\phi(U, V, \lceil t/2\rceil) \nrightarrow \neg[(U = A \land V = R) \lor (U = R \land V = B)]\}[/math].

Получившаяся формула верна только когда верно [math]\phi(U, V, \lceil t/2\rceil)[/math] и ложно [math]\neg[(U = A \land V = R) \lor (U = R \land V = B)][/math]. Это равносильно тому, что [math]V[/math] достижима из [math]U[/math] не более, чем за [math]\lceil t/2\rceil[/math] шагов, и либо [math]U = A \land V = R[/math], либо [math]U = R \land V = B[/math]. А если верно и то, и другое, то конфигурация [math]B[/math] достижима из конфигурации [math]A[/math] не более, чем за [math]t[/math] шагов. Размер полученной функции [math]\phi(A, B, t)[/math] полиномиален относительно [math]n[/math].

Теперь мы можем записать функцию [math]f(M, w)[/math], которая будет переводить ДМТ [math]M[/math] и слово на ленте [math]w[/math] в формулу из [math]\mathrm{TQBF}[/math].

[math]f(M, w) = \exists S \, \exists F \, (S - start) \land (F - accept) \land \phi(S, F, log_2(2^{\Omega r(n)})))[/math].

Выражения [math]S - start[/math] и [math]F - accept[/math] можно записать следующим образом:

[math]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}[/math].

[math]F - accept = x_{S, |w| + 1, \#_y} \lor \ldots \lor x_{S, r(n), \#_y}[/math].


Докажем, что сведение [math]f[/math] корректно.

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

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

Таким образом, [math]\mathrm{TQBF} \in \mathrm{PSH}[/math].
[math]\triangleleft[/math]
Теорема:
[math]\mathrm{TQBF} \in \mathrm{PSC}[/math].
Доказательство:
[math]\triangleright[/math]
Доказательство непосредственно следует из лемм.
[math]\triangleleft[/math]