PS-полнота языка верных булевых формул с кванторами (TQBF) — различия между версиями
Kasetkin (обсуждение | вклад) м |
м (rollbackEdits.php mass rollback) |
||
(не показано 13 промежуточных версий 4 участников) | |||
Строка 10: | Строка 10: | ||
|statement=<tex>\mathrm{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( | + | <tex>solve(Q_1 x_1 \ldots Q_n x_n \phi(x_1, \ldots, x_n))</tex> |
− | '''if''' | + | '''if''' n == 0 |
− | '''return''' <tex>\phi</tex> | + | '''return''' <tex>\phi</tex> |
− | '''if''' <tex> | + | '''if''' <tex>Q_1 = \forall</tex> |
− | '''return''' <tex>solve(Q_{ | + | '''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> | + | '''if''' <tex>Q_1 = \exists</tex> |
− | '''return''' <tex>solve(Q_{ | + | '''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>. | ||
}} | }} | ||
Строка 27: | Строка 27: | ||
Так как <tex>L \in \mathrm{PS}</tex>, то существует детерминированная машина Тьюринга <tex>M</tex>, распознающая его с использованием памяти полиномиального размера. Будем считать, что длина ленты машины <tex>M</tex> есть <tex>r(n)</tex>, где <tex>r</tex> — полином, а <tex>n</tex> — длина входа. | Так как <tex>L \in \mathrm{PS}</tex>, то существует детерминированная машина Тьюринга <tex>M</tex>, распознающая его с использованием памяти полиномиального размера. Будем считать, что длина ленты машины <tex>M</tex> есть <tex>r(n)</tex>, где <tex>r</tex> — полином, а <tex>n</tex> — длина входа. | ||
− | Пусть <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, | + | Под выражением <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> шагов. | ||
Строка 37: | Строка 37: | ||
<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) = L(t-1) | + | Общую длину получившейся формулы можно представить как <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 \, \{ | + | <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>L(t) = L(t-1)+const</tex>, где <tex>const = \|\exists R \,\forall U \,\forall V \, \{\| + \|\ | + | За один шаг рекурсии длина максимального пути между конфигурациями уменьшается в два раза. Поэтому общую длину получившейся формулы можно представить как <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)</tex> полиномиален относительно <tex>t</tex>. | ||
Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в формулу из <tex>\mathrm{TQBF}</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^{ | + | <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>S - start</tex> и <tex>F - accept</tex> можно записать следующим образом: | Выражения <tex>S - start</tex> и <tex>F - accept</tex> можно записать следующим образом: | ||
Строка 54: | Строка 54: | ||
<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>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_{ | + | <tex>F - accept = x_{F, 1, \#_y} \lor \ldots \lor x_{F, r(n), \#_y}</tex>. |
Докажем, что сведение <tex>f</tex> корректно. | Докажем, что сведение <tex>f</tex> корректно. | ||
− | Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, | + | Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, длины не более, чем <tex>2^{w r(n)}</tex>, а значит формула <tex>f(M, w)</tex> верна. |
− | Если формула <tex>f(M, w)</tex> оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем <tex>2^{ | + | Если формула <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>\mathrm{TQBF} \in \mathrm{PSH}</tex>. |
Текущая версия на 19:13, 4 сентября 2022
Определение: |
. | расшифровывается как True Quantified Boolean Formula. Это язык верных булевых формул с кванторами.
Определение: |
— это пропозициональная формула с кванторами. Кванторы для каждой переменной записываются в начале выражения. |
Лемма (1): |
. |
Доказательство: |
Чтобы доказать это, просто приведём программу , решающую булеву формулу с кванторами на дополнительной памяти и работающую за конечное время.Эта программа требует if n == 0 return if return if return дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — . |
Лемма (2): |
. |
Доказательство: |
Рассмотрим язык . Построим такую функцию , что и , где — полином.Так как , то существует детерминированная машина Тьюринга , распознающая его с использованием памяти полиномиального размера. Будем считать, что длина ленты машины есть , где — полином, а — длина входа.Пусть , — конфигурация . Конфигурация задаётся позицией и содержанием рабочей ленты. Введём обозначение — в конфигурации на -том месте стоит символ . Тогда размер конфигурации равен . Следовательно всего конфигураций .Под выражением будем понимать Аналогично выражение обозначаетРассмотрим функцию , проверяющую следующее условие: конфигурация достижима из конфигурации не более, чем за шагов.. . Общую длину получившейся формулы можно представить как . Заметим, что из-за умножения на 2 на каждом шаге рекурсии будет иметь экспоненциальный размер относительно . Нас это не устраивает, так как нам необходимо полиномиальное сведение. Поэтому воспользуемся квантором и перепишем её следующим образом:. Получившаяся формула верна, если существует такая промежуточная конфигурация , что для любых конфигураций и из того, что эти конфигурации нам интересны следует, что верно . А значит, конфигурация достижима из конфигурации не более, чем за шагов.За один шаг рекурсии длина максимального пути между конфигурациями уменьшается в два раза. Поэтому общую длину получившейся формулы можно представить как , где . Следовательно, размер полученной функции полиномиален относительно .Теперь мы можем записать функцию , которая будет переводить ДМТ и слово на ленте в формулу из .. Выражения и можно записать следующим образом:. .
Если , то существует путь из стартовой конфигурации в финишную, длины не более, чем , а значит формула верна.Если формула Таким образом, оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем . Значит, ДМТ допускает слово . Тогда . . |
Теорема: |
. |
Доказательство: |
Доказательство непосредственно следует из лемм. |