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

Материал из Викиконспекты
Перейти к: навигация, поиск
(не показано 36 промежуточных версий 8 участников)
Строка 1: Строка 1:
 
{{Определение
 
{{Определение
|definition=<tex>TQBF</tex> расшифровывается как True Quantified Boolean Formula. Это язык верных булевых формул с кванторами.
+
|definition=<tex>\mathrm{TQBF}</tex> расшифровывается как '''True Quantified Boolean Formula'''. Это язык верных булевых формул с кванторами.<br/>
<tex>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\}\}</tex>.
+
<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> — это пропозициональная формула с кванторами. Кванторы для каждой переменной записываются в начале выражения.
 
}}
 
}}
 
Чтобы доказать, что <tex>TQBF \in \mathrm{PSC}</tex>, необходимо показать, что <tex>TQBF \in \mathrm{PS}</tex> и <tex>TQBF \in \mathrm{PSH}</tex>.
 
 
{{Лемма
 
{{Лемма
 
|about=1
 
|about=1
|statement=<tex>TQBF \in \mathrm{PS}</tex>.
+
|statement=<tex>\mathrm{TQBF} \in \mathrm{PS}</tex>.
 
|proof=Чтобы доказать это, просто приведём программу <tex>solve</tex>, решающую булеву формулу с кванторами на <tex>O(n)</tex> дополнительной памяти и работающую за конечное время.
 
|proof=Чтобы доказать это, просто приведём программу <tex>solve</tex>, решающую булеву формулу с кванторами на <tex>O(n)</tex> дополнительной памяти и работающую за конечное время.
  <tex>solve(Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n))</tex>
+
  <tex>solve(Q_1 x_1 \ldots Q_n x_n \phi(x_1, \ldots, x_n))</tex>
 +
    '''if''' n == 0
 +
        '''return''' <tex>\phi</tex>  
 
     '''if''' <tex>Q_1 = \forall</tex>
 
     '''if''' <tex>Q_1 = \forall</tex>
         '''return''' <tex>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))</tex>
+
         '''return''' <tex>solve(Q_{2} x_{2} \ldots Q_n x_n \phi(0, x_{2}, \ldots, x_n)) \land solve(Q_{2} x_{2} \ldots Q_n x_n \phi(1, x_{2}, \ldots, x_n))</tex>
 
     '''if''' <tex>Q_1 = \exists</tex>
 
     '''if''' <tex>Q_1 = \exists</tex>
         '''return''' <tex>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))</tex>
+
         '''return''' <tex>solve(Q_{2} x_{2} \ldots Q_n x_n \phi(0, x_{2}, \ldots, x_n)) \lor solve(Q_{2} x_{2} \dots Q_n x_n \phi(1, x_{2}, \ldots, x_n))</tex>
 
Эта программа требует <tex>O(n)</tex> дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — <tex>n</tex>.
 
Эта программа требует <tex>O(n)</tex> дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — <tex>n</tex>.
 
}}
 
}}
 
{{Лемма
 
{{Лемма
 
|about=2
 
|about=2
|statement=<tex>TQBF \in \mathrm{PSH}</tex>.
+
|statement=<tex>\mathrm{TQBF} \in \mathrm{PSH}</tex>.
 
|proof=Рассмотрим язык <tex>L \in \mathrm{PS}</tex>.  
 
|proof=Рассмотрим язык <tex>L \in \mathrm{PS}</tex>.  
Построим такую функцию <tex>f</tex>, что <tex>x \in L \Leftrightarrow f(x) \in TQBF</tex> и <tex>T(f, x) \le p(|x|)</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>L \in \mathrm{PS}</tex>, то существует детерминированная машина Тьюринга <tex>M</tex>, распознающая его с использованием памяти полиномиального размера. Будем считать, что длина ленты машины <tex>M</tex> есть <tex>r(n)</tex>, где <tex>r</tex> — полином, а <tex>n</tex> — длина входа.  
  
Пусть <tex>I</tex> — конфигурация <tex>M</tex>. Размер конфигурации есть <tex>p(n)</tex>, где  <tex>n</tex> — длина входа, <tex>p</tex> — некоторый полином. Тогда выражение <tex>\exists I</tex> обозначает <tex> \exists x_0^I \, \exists x_1^I \dots \exists x_{r(n)}^I</tex>, где <tex>\{x_i^I\}</tex> — все переменные конфигурации <tex>I</tex>. Аналогично выражение <tex> \forall I</tex> обозначает <tex> \forall x_0^I \, \forall x_1^I \dots \forall x_{r(n)}^I</tex>. Всего конфигураций у ДМТ <tex>M \, 2^{O(p(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> \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>\phi(A, B, t)</tex>, проверяющую следующее условие: конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>2^t</tex> шагов.
Строка 30: Строка 35:
 
<tex>\phi(A, B, 0) = (A = B) \lor (A \vdash B)</tex>.
 
<tex>\phi(A, B, 0) = (A = B) \lor (A \vdash B)</tex>.
  
<tex>\phi(A, B, t) = \exists R \, \phi(A, R, t-1) \land \phi(R, B, t-1)</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 \, \{[(U = A \land V = R) \lor (U = R \land V = B)] \rightarrow \phi(U, V, t-1)\}</tex>.
 +
 
 +
Получившаяся формула верна, если существует такая промежуточная конфигурация <tex>R</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>\forall</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>.
 +
Следовательно, размер полученной функции <tex>\phi(A, B, t)</tex> полиномиален относительно <tex>t</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 \neg(U = R \land V = B)]\}</tex>.
+
Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в формулу из <tex>\mathrm{TQBF}</tex>.
  
Размер полученной функции <tex>\phi(A, B, t)</tex> полиномиален относительно <tex>n</tex>.
+
<tex>f(M, w) = \exists S \, \exists F \, (S - start) \land (F - accept) \land \phi(S, F, log_2(2^{w r(n)})))</tex>.
  
Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в формулу из <tex>TQBF</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(M, w) = (\exists I_{st}) (\exists I_{fin}) (x_0^{I_{st}} = start \land x_1^{I_{st}} = w[1] \land \dots \land x_{|w|}^{I_{st}} = w[|w|]) \land (\exists i \, x_i^{I_{fin}} = finish) \land \phi(I_{st}, I_{fin}, log_2(2^{O(p(n))})))</tex>.
 
  
 
Докажем, что сведение <tex>f</tex> корректно.
 
Докажем, что сведение <tex>f</tex> корректно.
  
Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, причём длины не более, чем <tex>2^{O(p(n))}</tex>, а значит формула <tex>\phi</tex> верна.
+
Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, длины не более, чем <tex>2^{w r(n)}</tex>, а значит формула <tex>f(M, w)</tex> верна.
  
Если формула <tex>f(M, w)</tex> оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем <tex>2^{O(p(n))}</tex>. Значит, ДМТ <tex>M</tex> допускает слово <tex>w</tex>. Тогда <tex>w \in L</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>.
 +
}}
  
Таким образом, <tex>TQBF \in \mathrm{PSH}</tex>.
+
{{Теорема
 +
|statement=<tex>\mathrm{TQBF} \in \mathrm{PSC}</tex>.
 +
|proof=Доказательство непосредственно следует из лемм.  
 
}}
 
}}
  
 
[[Категория: Теория сложности]]
 
[[Категория: Теория сложности]]

Версия 19:25, 4 июня 2013

Определение:
[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_1 x_1 \ldots Q_n x_n \phi(x_1, \ldots, x_n))[/math]
    if n == 0
        return [math]\phi[/math] 
    if [math]Q_1 = \forall[/math]
        return [math]solve(Q_{2} x_{2} \ldots Q_n x_n \phi(0, x_{2}, \ldots, x_n)) \land solve(Q_{2} x_{2} \ldots Q_n x_n \phi(1, x_{2}, \ldots, x_n))[/math]
    if [math]Q_1 = \exists[/math]
        return [math]solve(Q_{2} x_{2} \ldots Q_n x_n \phi(0, x_{2}, \ldots, x_n)) \lor solve(Q_{2} x_{2} \dots Q_n x_n \phi(1, x_{2}, \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]w = |\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]w r(n)[/math]. Следовательно всего конфигураций [math]2^{w 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_w} \, \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_w} \, \forall x_{I,2,c_1} \ldots[/math]

Рассмотрим функцию [math]\phi(A, B, t)[/math], проверяющую следующее условие: конфигурация [math]B[/math] достижима из конфигурации [math]A[/math] не более, чем за [math]2^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]L(t) = 2 L(t-1)+const[/math]. Заметим, что из-за умножения на 2 на каждом шаге рекурсии [math]L(t)[/math] будет иметь экспоненциальный размер относительно [math]t[/math]. Нас это не устраивает, так как нам необходимо полиномиальное сведение. Поэтому воспользуемся квантором [math]\forall[/math] и перепишем её следующим образом:

[math]\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{[(U = A \land V = R) \lor (U = R \land V = B)] \rightarrow \phi(U, V, t-1)\}[/math].

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

За один шаг рекурсии длина максимального пути между конфигурациями уменьшается в два раза. Поэтому общую длину получившейся формулы можно представить как [math]L(t) = L(t-1)+const[/math], где [math]const = \|\exists R \,\forall U \,\forall V \, \{\| + \|\land [(U = A \land V = R) \lor (U = R \land V = B)]\}\|[/math]. Следовательно, размер полученной функции [math]\phi(A, B, t)[/math] полиномиален относительно [math]t[/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^{w 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_{F, 1, \#_y} \lor \ldots \lor x_{F, r(n), \#_y}[/math].


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

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

Если формула [math]f(M, w)[/math] оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем [math]2^{w 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]