Истинная количественная логическая формула

В теории вычислительной сложности язык TQBF - это формальный язык, состоящий из истинных количественных булевых формул . (Полностью) количественная логическая формула - это формула в quantified логике высказываний, где каждая переменная количественно определена (или привязана ) с использованием либо экзистенциального или универсальные кванторы в начале предложения. Такая формула эквивалентна истинному или ложному (поскольку не существует свободных переменных). Если такая формула истинна, то эта формула написана на языке TQBF. Он также известен как QSAT (количественно SAT ).

• 1 Обзор
• 2 Предварительная нормальная форма
• 3 Решение
• 4 PSPACE-полнота
• 5 Разное
• 6 Примечания и ссылки
• 7 См. Также
• 8 Внешние ссылки

В теории сложности вычислений проблема квантифицированной логической формулы (QBF ) является обобщением проблемы логической выполнимости, в котором к каждой переменной могут применяться как кванторы существования, так и универсальные кванторы. Другими словами, он спрашивает, является ли количественная форма предложения по набору логических переменных истинным или ложным. Например, следующий пример QBF:

$\forall \; x\; \exists \; y\; \exists \; z\; ((x\; \vee \; z)\; \wedge \; y)\; \{\backslash \; displaystyle\; \backslash \; forall\; x\; \backslash \; exists\; y\; \backslash \; exists\; z\; \backslash \; ((x\; \backslash \; lor\; z))\; \backslash \; land\; y)\}$

QBF - это каноническая полная задача для PSPACE, класс задач, решаемых детерминированной или недетерминированной машиной Тьюринга в полиномиальном пространство и неограниченное время. Учитывая формулу в виде абстрактного синтаксического дерева, проблема может быть легко решена с помощью набора взаимно рекурсивных процедур, которые вычисляют формулу. Такой алгоритм использует пространство, пропорциональное высоте дерева, которое в худшем случае является линейным, но использует экспоненту времени в количестве кванторов.

При условии, что MA ⊊ PSPACE, что широко распространено, QBF не может быть решена, а данное решение даже не может быть проверено ни за детерминированное, ни за вероятностное полиномиальное время (на самом деле, в отличие от проблемы выполнимости, нет известного способа кратко указать решение). Его можно решить с помощью переменной машины Тьюринга за линейное время, поскольку AP = PSPACE, где AP - класс задач, которые альтернативные машины могут решить за полиномиальное время.

Когда был показан результативный результат IP = PSPACE (см. интерактивная система доказательств ), это было сделано путем демонстрации интерактивной системы доказательств, которая могла решить QBF путем решения конкретной арифметизации задачи..

Формулы QBF имеют ряд полезных канонических форм. Например, можно показать, что существует редукция «многие-один» за полиномиальное время, которая переместит все кванторы в начало формулы и заставит их чередоваться между универсальными и экзистенциальными кванторами. Есть еще одно сокращение, которое оказалось полезным в доказательстве IP = PSPACE, где не более одного универсального квантификатора помещается между использованием каждой переменной и квантором, связывающим эту переменную. Это было критически важно для ограничения количества продуктов в определенных подвыражениях арифметизации.

Можно предположить, что полностью квантифицированная логическая формула имеет очень специфическую форму, называемую предварительной нормальной формой. Он состоит из двух основных частей: части, содержащей только кванторы, и части, содержащей неквантифицированную логическую формулу, обычно обозначаемую как $\varphi \; \{\backslash \; displaystyle\; \backslash \; displaystyle\; \backslash \; phi\}$. Если есть $n\; \{\backslash \; displaystyle\; \backslash \; displaystyle\; n\}$логические переменные, всю формулу можно записать как

$\exists \; x\; 1\; \forall \; x\; 2\; \exists \; x\; 3\; \cdots \; Q\; nxn\; \varphi \; (x\; 1,\; x\; 2,\; x\; 3,\dots ,\; xn)\; \{\backslash \; displaystyle\; \backslash \; displaystyle\; \backslash \; exists\; x\_\; \{1\}\; \backslash \; forall\; x\_\; \{2\}\; \backslash \; exists\; x\_\; \{3\}\; \backslash \; cdots\; Q\_\; \{n\}\; x\_\; \{n\}\; \backslash \; phi\; (x\_\; \{1\}),\; x\_\; \{2\},\; x\_\; \{3\},\; \backslash \; dots,\; x\_\; \{n\})\}$

где каждая переменная попадает в область некоторого квантификатора. Путем введения фиктивных переменных любую формулу в предваренной нормальной форме можно преобразовать в предложение, в котором чередуются экзистенциальные и универсальные кванторы. Используя фиктивную переменную $y\; 1\; \{\backslash \; displaystyle\; \backslash \; displaystyle\; y\_\; \{1\}\}$,

$\exists \; x\; 1\; \exists \; x\; 2\; \varphi \; (x\; 1,\; x\; 2)\; \mapsto \; \exists \; x\; 1\; \forall \; y\; 1\; \exists \; x\; 2\; \varphi \; (x\; 1\; Икс\; 2)\; \{\backslash \; Displaystyle\; \backslash \; Displaystyle\; \backslash \; существует\; x\_\; \{1\}\; \backslash \; exists\; x\_\; \{2\}\; \backslash \; phi\; (x\_\; \{1\},\; x\_\; \{2\})\; \backslash \; quad\; \backslash \; mapsto\; \backslash \; quad\; \backslash \; exists\; x\_\; \{1\}\; \backslash \; forall\; y\_\; \{\; 1\}\; \backslash \; exists\; x\_\; \{2\}\; \backslash \; phi\; (x\_\; \{1\},\; x\_\; \{2\})\}$

Второе предложение имеет то же значение истинности , но следует ограниченному синтаксису. Принятие полностью квантифицированных булевых формул в предваренной нормальной форме - частая особенность доказательств.

Существует простой рекурсивный алгоритм для определения того, находится ли QBF в TQBF (т.е. истинно). Для некоторого QBF

$Q\; 1\; x\; 1\; Q\; 2\; x\; 2\; \cdots \; Q\; n\; x\; n\; \varphi \; (x\; 1,\; x\; 2,\dots ,\; x\; n).\; \{\backslash \; Displaystyle\; Q\_\; \{1\}\; x\_\; \{1\}\; Q\_\; \{2\}\; x\_\; \{2\}\; \backslash \; cdots\; Q\_\; \{n\}\; x\_\; \{n\}\; \backslash \; phi\; (x\_\; \{1\},\; x\_\; \{2\},\; \backslash \; dots,\; x\_\; \{n\}).\}$

Если формула не содержит квантификаторов, мы можем просто вернуть формулу. В противном случае мы снимаем первый квантор и проверяем оба возможных значения для первой переменной:

$A\; =\; Q\; 2\; x\; 2\; \cdots \; Q\; nxn\; \varphi \; (0,\; x\; 2,\dots ,\; xn),\; \{\backslash \; displaystyle\; A\; =\; Q\_\; \{2\; \}\; x\_\; \{2\}\; \backslash \; cdots\; Q\_\; \{n\}\; x\_\; \{n\}\; \backslash \; phi\; (0,\; x\_\; \{2\},\; \backslash \; dots,\; x\_\; \{n\}),\}$

$B\; =\; Q\; 2\; x\; 2\; \cdots \; Q\; nxn\; \varphi \; (1,\; x\; 2,\dots ,\; xn).\; \{\backslash \; displaystyle\; B\; =\; Q\_\; \{2\}\; x\_\; \{2\}\; \backslash \; cdots\; Q\_\; \{n\}\; x\_\; \{n\}\; \backslash \; phi\; (1,\; x\_\; \{2\},\; \backslash \; dots,\; x\_\; \{n\}).\}$

Если $Q\; 1\; =\; \exists \; \{\backslash \; displaystyle\; Q\_\; \{1\}\; =\; \backslash \; exists\}$, затем возвращаем $A\; \vee \; B\; \{\backslash \; displaystyle\; A\; \backslash \; lor\; B\}$. Если $Q\; 1\; =\; \forall \; \{\backslash \; displaystyle\; Q\_\; \{1\}\; =\; \backslash \; forall\}$, тогда возвращаем $A\; \wedge \; B\; \{\backslash \; displaystyle\; A\; \backslash \; land\; B\}$.

Насколько быстро работает этот алгоритм. бегать? Для каждого квантора в исходной QBF алгоритм выполняет два рекурсивных вызова только для линейно меньшей подзадачи. Это дает алгоритму экспоненциальное время выполнения O (2).

Сколько места использует этот алгоритм? При каждом вызове алгоритма ему необходимо сохранять промежуточные результаты вычисления A и B. Каждый рекурсивный вызов снимает один квантор, поэтому общая рекурсивная глубина линейна по количеству кванторов. Формулы, в которых отсутствуют кванторы, можно вычислить в пространстве, логарифмическом по количеству переменных. Первоначальный QBF был полностью определен количественно, поэтому количественных показателей было не меньше, чем переменных. Таким образом, этот алгоритм использует пространство O (n + log n) = O (n). Это делает язык TQBF частью PSPACE класса сложности.

Язык TQBF служит в теории сложности как канонический PSPACE-полная проблема. Полная PSPACE означает, что язык находится в PSPACE, и что язык также PSPACE-hard. Приведенный выше алгоритм показывает, что TQBF находится в PSPACE. Чтобы показать, что TQBF является жестким для PSPACE, необходимо показать, что любой язык класса сложности PSPACE может быть сокращен до TQBF за полиномиальное время. То есть,

$\forall \; L\; \in \; P\; S\; P\; A\; C\; E,\; L\; \le \; p\; T\; Q\; B\; F.\; \{\backslash \; displaystyle\; \backslash \; forall\; L\; \backslash \; in\; \{\backslash \; mathsf\; \{PSPACE\}\},\; L\; \backslash \; leq\; \_\; \{p\}\; \backslash \; mathrm\; \{TQBF\}.\}$

Это означает, что для языка PSPACE L, находится ли вход x в L можно решить, проверив, находится ли $f\; (x)\; \{\backslash \; displaystyle\; f\; (x)\}$в TQBF, для некоторой функции f, которая требуется для выполнения за полиномиальное время (относительно длины ввод). Символически

$x\; \in \; L\; ⟺\; f\; (x)\; \in \; T\; Q\; B\; F.\; \{\backslash \; displaystyle\; x\; \backslash \; in\; L\; \backslash \; iff\; f\; (x)\; \backslash \; in\; \backslash \; mathrm\; \{TQBF\}.\}$

Доказательство того, что TQBF является жестким для PSPACE, требует указания f.

Итак, предположим, что L - это язык PSPACE. Это означает, что L может быть определено детерминированной машиной Тьюринга (DTM) в полиномиальном пространстве. Это очень важно для сокращения L до TQBF, потому что конфигурации любой такой машины Тьюринга могут быть представлены в виде булевых формул с логическими переменными, представляющими состояние машины, а также содержимое каждой ячейки на ленте машины Тьюринга, с позицией головы машины Тьюринга, закодированной в формуле по порядку формулы. В частности, наша редукция будет использовать переменные $c\; 1\; \{\backslash \; displaystyle\; c\_\; \{1\}\}$и $c\; 2\; \{\backslash \; displaystyle\; c\_\; \{2\}\}$, которые представляют две возможные конфигурации DTM для L и натуральное число t при построении QBF $\varphi \; c\; 1,\; c\; 2,\; t\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{1\},\; c\_\; \{2\},\; t\}\; \}$который истинен тогда и только тогда, когда DTM для L может перейти от конфигурации, закодированной в $c\; 1\; \{\backslash \; displaystyle\; c\_\; \{1\}\}$, к конфигурации, закодированной в $c\; 2\; \{\backslash \; displaystyle\; c\_\; \{2\}\}$не более чем за t шагов. Затем функция f построит из DTM для L a QBF $\varphi \; cstart,\; caccept,\; T\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{start\},\; c\_\; \{accept\},\; T\}\}$, где $cstart\; \{\backslash \; displaystyle\; c\_\; \{start\}\}$- это начальная конфигурация DTM, $caccept\; \{\backslash \; displaystyle\; c\_\; \{accept\}\}$- принимающая конфигурация DTM, и T - максимальное количество шагов, которое может потребоваться DTM для перехода от одной конфигурации к другой. Мы знаем, что T = O (exp (n)), где n - длина ввода, поскольку это ограничивает общее количество возможных конфигураций соответствующего DTM. Конечно, для достижения $caccept\; \{\backslash \; displaystyle\; c\; \_\; \{\backslash \; mathrm\; \{accept\}\}\}$DTM не может потребоваться больше шагов, чем есть в возможных конфигурациях, если он не входит в цикл, и в этом случае он в любом случае никогда не достигать $caccept\; \{\backslash \; displaystyle\; c\; \_\; \{\backslash \; mathrm\; \{accept\}\}\}$.

На этом этапе доказательства мы уже уменьшили вопрос о том, является ли входная формула w (закодированной, конечно, в $cstart\; \{\backslash \; displaystyle\; c\_\; \{start\}\}$) находится в L на вопрос, является ли QBF $\varphi \; cstart,\; caccept,\; T\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{start\},\; c\_\; \{accept\},\; T\}\}$, т. е. $f\; (w)\; \{\backslash \; displaystyle\; f\; (w)\}$, находится в TQBF. Оставшаяся часть этого доказательства доказывает, что f можно вычислить за полиномиальное время.

Для $t\; =\; 1\; \{\backslash \; displaystyle\; t\; =\; 1\}$, вычисление $\varphi \; c\; 1,\; c\; 2,\; t\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{1\; \},\; c\_\; \{2\},\; t\}\}$прост - либо одна из конфигураций меняется на другой на одном шаге, либо нет. Поскольку машина Тьюринга, которую представляет наша формула, является детерминированной, это не представляет проблемы.

Для $t>1\; \{\backslash \; displaystyle\; t>1\}$, вычисление $\varphi \; c\; 1,\; c\; 2,\; t\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{1\},\; c\_\; \{2\},\; t\; \}\}$включает рекурсивное вычисление, ищущее так называемую "среднюю точку" $m\; 1\; \{\backslash \; displaystyle\; m\_\; \{1\}\}$. В этом случае мы переписываем формула следующим образом:

$\varphi \; c\; 1,\; c\; 2,\; t\; =\; \exists \; m\; 1\; (\varphi \; c\; 1,\; m\; 1,\; \lceil \; t\; /\; 2\; \rceil \; \wedge \; \varphi \; m\; 1,\; c\; 2,\; \lceil \; t\; /\; 2\; \rceil ).\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{1\},\; c\_\; \{2\},\; t\}\; =\; \backslash \; exists\; m\_\; \{1\}\; (\backslash \; phi\; \_\; \{c\_\; \{1\},\; m\_\; \{1\},\; \backslash \; lceil\; t\; /\; 2\; \backslash \; rceil\}\; \backslash \; wedge\; \backslash \; phi\; \_\; \{m\_\; \{1\},\; c\_\; \{2\},\; \backslash \; lceil\; t\; /\; 2\; \backslash \; rceil\}).\}$

Это преобразует вопрос о том, $c\; 1\; \{\backslash \; displaystyle\; c\_\; \{1\}\}$может достичь $c\; 2\; \{\backslash \; displaystyle\; c\_\; \{2\}\}$за t шагов на вопрос о том, достигает ли $c\; 1\; \{\backslash \; displaystyle\; c\_\; \{1\}\}$средняя точка $m\; 1\; \{\backslash \; displaystyle\; m\_\; \{1\}\}$в $t\; /\; 2\; \{\backslash \; displaystyle\; t\; /\; 2\}$шагов, elf достигает $c\; 2\; \{\backslash \; displaystyle\; c\_\; \{2\}\}$за $t\; /\; 2\; \{\backslash \; displaystyle\; t\; /\; 2\}$шагов. Ответ на последний вопрос, конечно же, дает ответ на первый.

Теперь t ограничено только T, которое является экспоненциальным (а значит, не полиномиальным) по длине ввода. Кроме того, каждый рекурсивный слой практически удваивает длину формулы. (Переменная $m\; 1\; \{\backslash \; displaystyle\; m\_\; \{1\}\}$- это только одна средняя точка - для большего t, так сказать, будет больше остановок на пути.) Итак, время, необходимое для рекурсивного выполнения оценить $\varphi \; c\; 1,\; c\; 2,\; t\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{1\},\; c\_\; \{2\},\; t\}\}$таким образом, также может быть экспоненциальным, просто потому что формула может стать экспоненциально большой. Эта проблема решается путем универсального количественного определения с использованием переменных $c\; 3\; \{\backslash \; displaystyle\; c\_\; \{3\}\}$и $c\; 4\; \{\backslash \; displaystyle\; c\_\; \{4\}\}$над пары конфигурации (например, $\{(c\; 1,\; m\; 1),\; (m\; 1,\; c\; 2)\}\; \{\backslash \; displaystyle\; \backslash \; \{(c\_\; \{1\},\; m\_\; \{1\}),\; (m\_\; \{1\},\; c\_\; \{\; 2\})\; \backslash \}\}$), что предотвращает увеличение длины формулы из-за рекурсивных слоев. Это дает следующую интерпретацию $\varphi \; c\; 1,\; c\; 2,\; t\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{1\},\; c\_\; \{2\},\; t\}\}$:

$\varphi \; c\; 1,\; c\; 2,\; t\; =\; \exists \; m\; 1\; \forall \; (c\; 3,\; c\; 4)\; \in \; \{(c\; 1,\; m\; 1),\; (m\; 1,\; c\; 2)\}\; (\varphi \; c\; 3,\; c\; 4,\; \lceil \; t\; /\; 2\; \rceil ).\; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{1\},\; c\_\; \{2\},\; t\}\; =\; \backslash \; exists\; m\_\; \{1\}\; \backslash \; forall\; (c\_\; \{3\},\; c\_\; \{4\})\; \backslash \; in\; \backslash \; \{(c\_\; \{1\},\; m\_\; \{1\}),\; (m\_\; \{1\},\; c\_\; \{2\})\; \backslash \}\; (\backslash \; phi\; \_\; \{c\_\; \{3\},\; c\_\; \{4\},\; \backslash \; lceil\; t\; /\; 2\; \backslash \; rceil\}).\}$

Эта версия формула действительно может быть вычислена за полиномиальное время, поскольку любой ее экземпляр может быть вычислен за полиномиальное время. Универсально определенная упорядоченная пара просто говорит нам, что какой бы выбор не был $(c\; 3,\; c\; 4)\; \{\backslash \; displaystyle\; (c\_\; \{3\},\; c\_\; \{4\})\}$, $\varphi \; c\; 1,\; c\; 2,\; t\; ⟺\; \varphi \; c\; 3,\; c\; 4,\; \lceil \; t\; /\; 2\; \rceil \; \{\backslash \; displaystyle\; \backslash \; phi\; \_\; \{c\_\; \{1\},\; c\_\; \{2\},\; t\}\; \backslash \; iff\; \backslash \; phi\; \_\; \{c\_\; \{3\},\; c\_\; \{4\},\; \backslash \; lceil\; t\; /\; 2\; \backslash \; rceil\}\}$.

Таким образом, $\forall \; L\; \in \; PSPACE,\; L\; \le \; p\; TQBF\; \{\backslash \; displaystyle\; \backslash \; forall\; L\; \backslash \; in\; \{\backslash \; mathsf\; \{PSPACE\}\},\; L\; \backslash \; leq\; \_\; \{p\}\; \backslash \; mathrm\; \{TQBF\}\}$, поэтому TQBF сложен для PSPACE. Вместе с приведенным выше результатом, что TQBF находится в PSPACE, это завершает доказательство того, что TQBF является PSPACE-полным языком.

(Это доказательство следует за Sipser 2006 pp. 310–313 во всех основных положениях. Papadimitriou 1994 также включает доказательство.)

• Одной из важных подзадач в TQBF является логическое значение проблема выполнимости. В этой задаче вы хотите знать, может ли заданная логическая формула $\varphi \; \{\backslash \; displaystyle\; \backslash \; phi\}$быть истинной с некоторым назначением переменных. Это эквивалентно TQBF с использованием только экзистенциальных кванторов:

$\exists \; x\; 1\; \cdots \; \exists \; xn\; \varphi \; (x\; 1,\dots ,\; xn)\; \{\backslash \; displaystyle\; \backslash \; exists\; x\_\; \{1\}\; \backslash \; cdots\; \backslash \; exists\; x\_\; \{n\}\; \backslash \; phi\; (x\_\; \{1\},\; \backslash \; ldots,\; x\_\; \{n\})\}$

Это также пример большего результата NP $\subseteq \; \{\backslash \; displaystyle\; \backslash \; substeq\}$PSPACE, который непосредственно следует из наблюдения, что верификатор полиномиального времени для доказательства языка, принятого NTM (недетерминированная машина Тьюринга ), требует полиномиального пространства для хранения доказательства.

• Любой класс в иерархии полиномов (PH ) TQBF представляет собой серьезную проблему. Другими словами, для класса, включающего все языки L, для которых существует поливременной TM V, верификатор, такой, что для всех входных x и некоторой константы i,

$x\; \in \; L\; \iff \; \exists \; y\; 1\; \forall \; y\; 2\; \cdots \; Q\; iyi\; V\; (x,\; y\; 1,\; y\; 2,\dots ,\; yi)\; =\; 1\; \{\backslash \; displaystyle\; x\; \backslash \; in\; L\; \backslash \; Leftrightarrow\; \backslash \; exists\; y\_\; \{1\}\; \backslash \; forall\; y\_\; \{2\}\; \backslash \; cdots\; Q\_\; \{i\}\; y\_\; \{i\}\; \backslash \; V\; (x,\; y\_\; \{1\},\; y\_\; \{2\},\; \backslash \; dots,\; y\_\; \{i\})\; \backslash \; =\; \backslash \; 1\}$

, который имеет определенную формулировку QBF, которая задается как

$\exists \; \varphi \; \{\backslash \; displaystyle\; \backslash \; exists\; \backslash \; phi\}$такой, что $\exists \; x\; 1\; \to \; \forall \; x\; 2\; \to \; \cdots \; Q\; ixi\; \to \; \varphi \; (x\; 1\; \to ,\; x\; 2\; \to ,\dots ,\; xi\; \to )\; =\; 1\; \{\backslash \; displaystyle\; \backslash \; exists\; \{\backslash \; vec\; \{x\_\; \{1\}\}\}\; \backslash \; forall\; \{\backslash \; vec\; \{x\_\; \{2\}\}\}\; \backslash \; cdots\; Q\_\; \{i\}\; \{\backslash \; vec\; \{x\_\; \{i\}\}\}\; \backslash \; \backslash \; phi\; (\{\backslash \; vec\; \{x\_\; \{1\}\}\},\; \{\backslash \; vec\; \{x\_\; \{2\}\}\},\; \backslash \; dots,\; \{\backslash \; vec\; \{x\_\; \{i\}\}\})\; \backslash \; =\; \backslash \; 1\}$

, где $xi\; \to \; \{\backslash \; displaystyle\; \{\backslash \; vec\; \{x\_\; \{\; i\}\}\}\}$являются векторами логических переменных.

• Важно отметить, что хотя язык TQBF определен как набор истинных количественных булевых формул, часто используется аббревиатура TQBF ( даже в этой статье), чтобы обозначить полностью количественно Логическая формула, часто называемая просто QBF (количественная логическая формула, понимаемая как «полностью» или «полностью» количественно определенная). Важно различать контекстуально два использования аббревиатуры TQBF при чтении литературы.
• TQBF можно рассматривать как игру между двумя игроками с чередованием ходов. Переменные, определяемые количественно, эквивалентны представлению о том, что игрок может сделать ход в свой ход. Универсальные количественные переменные означают, что исход игры не зависит от того, какой ход игрок делает в этот ход. Кроме того, TQBF, первый квантификатор которого является экзистенциальным, соответствует игре по формуле, в которой первый игрок имеет выигрышную стратегию.
• TQBF, для которого количественная формула находится в 2- CNF может быть решена за линейное время с помощью алгоритма, включающего анализ сильной связности его графа импликации. Проблема 2-выполнимости является частным случаем TQBF для этих формул, в которых каждый квантор является экзистенциальным.
• Существует систематическая обработка ограниченных версий квантифицированных булевых формул (что дает Шеферу- классификации типов), представленные в пояснительной статье Хуби Чена.
• Planar TQBF, обобщающий Planar SAT, был доказан Д. Лихтенштейном как PSPACE-полный.

1. ^М. Гэри и Д. Джонсон (1979). Компьютеры и несговорчивость: Руководство по теории NP-полноты. У. Х. Фриман, Сан-Франциско, Калифорния. ISBN 0-7167-1045-5.
2. ^А. Чандра, Д. Козен и Л. Стокмейер (1981). "Чередование". Журнал ACM. 28 (1): 114–133. doi : 10.1145 / 322234.322243. CS1 maint: несколько имен: список авторов (ссылка )
3. ^Ади Шамир (1992). "Ip = Pspace. Журнал ACM. 39 (4): 869–877. doi : 10.1145 / 146585.146609.
4. ^Кром, Мелвен Р. (1967). «Проблема решения для класса формул первого порядка, в которых все дизъюнкции двоичны». Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 13 (1-2): 15-20. doi : 10.1002 / malq.19670130104..
5. ^Аспвалл, Бенгт; Пласс, Майкл Ф.; Тарджан, Роберт Э. (1979). "Алгоритм линейного времени для проверки истинности определенных количественных булевых формул » (PDF). Письма об обработке информации. 8(3): 121–123. doi : 10.1016 / 0020-0190 (79) 90002-4..
6. ^Чен, Хуби (декабрь 2009 г.). «Свидание логики, сложности и алгебры». ACM Computing Surveys. ACM. 42 (1): 1–32. arXiv : cs / 0611018. doi : 10.1145 / 1592451.1592453.
7. ^Лихтенст Эйн, Дэвид (1982-05-01). «Планарные формулы и их использование». SIAM Journal on Computing. 11 (2): 329–343. doi : 10.1137 / 0211025. ISSN 0097-5397.

• Fortnow Homer (2003) дает некоторую историческую справку о PSPACE и TQBF.
• Чжан (2003) дает некоторую историческую справку о булевых формулах.
• Арора, Санджив. (2001). COS 522: вычислительная сложность. Конспект лекций, Принстонский университет. Получено 10 октября 2005 г.
• Фортноу, Лэнс и Стив Гомер. (2003, июнь). Краткая история вычислительной сложности. Колонка вычислительной сложности, 80. Получено 9 октября 2005 г.
• Пападимитриу, К. Х. (1994). Вычислительная сложность. Читает: Эддисон-Уэсли.
• Сипсер, Майкл. (2006). Введение в теорию вычислений. Бостон: Thomson Course Technology.
• Чжан, Линтао. (2003). В поисках истины: методы выполнимости булевых формул. Получено 10 октября 2005 г.

• теорему Кука – Левина, в которой говорится, что SAT является NP-полным
• Обобщенная география

• Библиотека квантифицированных булевых формул (QBFLIB)
• Международный семинар по квантифицированным булевым формулам
• DepQBF - решатель на основе поиска для квантифицированных логических формул
• CAQE - на основе CEGAR решатель для количественных булевых формул; победитель недавних выпусков ежегодного конкурса решателей QBF QBFEVAL.
• CADET - решатель для количественных булевых формул, ограниченный одним чередованием кванторов, с возможностью вычисления функций Сколема