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

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

Обзор

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

∀ х   ∃ у   ∃ з   ( ( х ∨ з ) ∧ у ) {\displaystyle \forall x\ \exists y\ \exists z\ ((x\or z)\land y)}

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

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

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

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

Нормальная предварительная форма

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

∃ х 1 ∀ х 2 ∃ х 3 ⋯ В н х н ϕ ( х 1 , х 2 , х 3 , … , х н ) {\displaystyle \displaystyle \exists x_{1}\forall x_{2}\exists x_{3}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},x_{3},\dots ,x_{n})}

где каждая переменная попадает в область действия некоторого квантификатора. Вводя фиктивные переменные, любую формулу в предваренной нормальной форме можно преобразовать в предложение, где чередуются квантификаторы существования и всеобщности. Используя фиктивную переменную , у 1 {\displaystyle \displaystyle y_{1}}

∃ х 1 ∃ х 2 ϕ ( х 1 , х 2 ) ↦ ∃ х 1 ∀ у 1 ∃ х 2 ϕ ( х 1 , х 2 ) {\displaystyle \displaystyle \exists x_{1}\exists x_{2}\phi (x_{1},x_{2})\quad \mapsto \quad \exists x_{1}\forall y_{1}\exists x_{2}\phi (x_{1},x_{2})}

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

QBF-решатели

Наивный

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

В 1 х 1 В 2 х 2 ⋯ В н х н ϕ ( х 1 , х 2 , … , х н ) . {\displaystyle Q_{1}x_{1}Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},\dots ,x_{n}).}

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

А = В 2 х 2 ⋯ В н х н ϕ ( 0 , х 2 , … , х н ) , {\displaystyle A=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (0,x_{2},\dots ,x_{n}),}
Б = В 2 х 2 ⋯ В н х н ϕ ( 1 , х 2 , … , х н ) . {\displaystyle B=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (1,x_{2},\dots ,x_{n}).}

Если , то вернуть . Если , то вернуть . [4] В 1 = ∃ {\displaystyle Q_{1}=\существует} А ∨ Б {\displaystyle A\или B} В 1 = ∀ {\displaystyle Q_{1}=\forall } А ∧ Б {\displaystyle А\и Б}

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

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

Уровень развития

Несмотря на полноту QBF по PSPACE, было разработано много решателей для решения этих примеров. (Это аналогично ситуации с SAT , версией с одним квантором существования; даже несмотря на то, что она является NP-полной , все еще возможно решить многие примеры SAT эвристически.) [5] [6] Случай, когда есть только 2 квантора, известный как 2QBF, привлек особое внимание. [7] [ weasel words ]

Соревнование решателей QBF QBFEVAL проводится более или менее ежегодно с 2004 года; [5] [6] решатели должны читать экземпляры в формате QDIMACS и либо в форматах QCIR, либо в QAIGER. [8] Высокопроизводительные решатели QBF обычно используют QDPLL (обобщение DPLL ) или CEGAR. [5] [6] [7] Исследования в области решения QBF начались с разработки обратного отслеживания DPLL для QBF в 1998 году, за которым последовало введение обучения предложениям и исключения переменных в 2002 году; [9] таким образом, по сравнению с решением SAT, которое разрабатывалось с 1960-х годов, QBF является относительно молодой областью исследований по состоянию на 2017 год. [9] [ weasel words ]

Некоторые известные решатели QBF включают в себя:

  • CADET, который решает квантифицированные булевы формулы, ограниченные одним чередованием квантификаторов (с возможностью вычисления функций Сколема ), на основе инкрементальной детерминизации [ необходимо разъяснение ] и с возможностью доказывать свои ответы. [10]
  • CAQE — решатель на основе CEGAR для квантифицированных булевых формул; победитель последних выпусков QBFEVAL. [11]
  • DepQBF — поисковый решатель для квантифицированных булевых формул [12]
  • sKizzo — первый решатель, который использовал символическую сколемизацию, извлекал сертификаты выполнимости, использовал гибридный механизм вывода, реализовал абстрактное ветвление, работал с ограниченными квантификаторами и перечислял допустимые назначения, а также стал победителем QBFEVAL 2005, 2006 и 2007 гг. [13]

Приложения

Решатели QBF могут применяться для планирования (в искусственном интеллекте), включая безопасное планирование; последнее имеет решающее значение в приложениях робототехники. [14] Решатели QBF также могут применяться для проверки ограниченной модели , поскольку они обеспечивают более короткое кодирование, чем это было бы необходимо для решателя на основе SAT. [14]

Оценку QBF можно рассматривать как игру двух игроков между игроком, который контролирует экзистенциально квантифицированные переменные, и игроком, который контролирует универсально квантифицированные переменные. Это делает QBF пригодными для кодирования задач реактивного синтеза . [14] Аналогично решатели QBF могут использоваться для моделирования состязательных игр в теории игр . Например, решатели QBF могут использоваться для поиска выигрышных стратегий для географических игр , которые затем могут автоматически воспроизводиться в интерактивном режиме. [15]

Решатели QBF могут использоваться для формальной проверки эквивалентности , а также для синтеза булевых функций. [14]

Другие типы проблем, которые можно кодировать как QBF, включают:

Расширения

В QBFEVAL 2020 был представлен «DQBF Track», в котором экземплярам разрешалось иметь квантификаторы Хенкина (выраженные в формате DQDIMACS). [8]

PSPACE-полнота

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

∀ Л ∈ П С П А С Э , Л ≤ п Т В Б Ф . {\displaystyle \forall L\in {\mathsf {PSPACE}},L\leq _{p}\mathrm {TQBF} .}

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

х ∈ Л ⟺ ф ( х ) ∈ Т В Б Ф . {\displaystyle x\in L\ifl f(x)\in \mathrm {TQBF} .}

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

Итак, предположим, что L — язык PSPACE. Это означает, что L может быть определен полиномиальной пространственной детерминированной машиной Тьюринга (DTM). Это очень важно для сведения L к TQBF, поскольку конфигурации любой такой машины Тьюринга могут быть представлены в виде булевых формул с булевыми переменными, представляющими состояние машины, а также содержимое каждой ячейки на ленте машины Тьюринга, с положением головки машины Тьюринга, закодированным в формуле упорядочением формулы. В частности, наше сведение будет использовать переменные и , которые представляют две возможные конфигурации DTM для L, и натуральное число t, при построении QBF, которая истинна тогда и только тогда, когда DTM для L может перейти от конфигурации, закодированной в , к конфигурации, закодированной в не более чем за t шагов. Функция f , тогда, построит из DTM для L QBF , где — начальная конфигурация DTM, — принимающая конфигурация DTM, а T — максимальное количество шагов, которое может потребоваться DTM для перехода от одной конфигурации к другой. Мы знаем, что T = O (exp( n k )) для некоторого k , где n — длина входа, поскольку это ограничивает общее количество возможных конфигураций соответствующей DTM. Конечно, DTM не может сделать больше шагов, чем возможных конфигураций для достижения, если только он не войдет в цикл, в этом случае он никогда не достигнет его в любом случае. с 1 {\displaystyle c_{1}} с 2 {\displaystyle c_{2}} ϕ с 1 , с 2 , т {\displaystyle \phi _{c_{1},c_{2},t}} c 1 {\displaystyle c_{1}} c 2 {\displaystyle c_{2}} ϕ c start , c accept , T {\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}} c s t a r t {\displaystyle c_{start}} c accept {\displaystyle c_{\text{accept}}} c a c c e p t {\displaystyle c_{\mathrm {accept} }} c a c c e p t {\displaystyle c_{\mathrm {accept} }}

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

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

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

ϕ c 1 , c 2 , t = ∃ m 1 ( ϕ c 1 , m 1 , ⌈ t / 2 ⌉ ∧ ϕ m 1 , c 2 , ⌈ t / 2 ⌉ ) . {\displaystyle \phi _{c_{1},c_{2},t}=\exists m_{1}(\phi _{c_{1},m_{1},\lceil t/2\rceil }\wedge \phi _{m_{1},c_{2},\lceil t/2\rceil }).}

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

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

ϕ c 1 , c 2 , t = ∃ m 1 ∀ ( c 3 , c 4 ) ∈ { ( c 1 , m 1 ) , ( m 1 , c 2 ) } ( ϕ c 3 , c 4 , ⌈ t / 2 ⌉ ) . {\displaystyle \phi _{c_{1},c_{2},t}=\exists m_{1}\forall (c_{3},c_{4})\in \{(c_{1},m_{1}),(m_{1},c_{2})\}(\phi _{c_{3},c_{4},\lceil t/2\rceil }).}

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

Таким образом, , поэтому TQBF является PSPACE-трудным. Вместе с приведенным выше результатом, что TQBF находится в PSPACE, это завершает доказательство того, что TQBF является PSPACE-полным языком. ∀ L ∈ P S P A C E , L ≤ p T Q B F {\displaystyle \forall L\in {\mathsf {PSPACE}},L\leq _{p}\mathrm {TQBF} }

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

Разное

  • Одной из важных подзадач в TQBF является проблема выполнимости булевых уравнений . В этой задаче вы хотите узнать, можно ли сделать заданную булеву формулу истинной с помощью некоторого назначения переменных. Это эквивалентно TQBF, использующему только квантификаторы существования: Это также пример большего результата NP ⊆ PSPACE, который следует непосредственно из наблюдения, что полиномиальный верификатор времени для доказательства языка, принимаемого NTM ( недетерминированной машиной Тьюринга ), требует полиномиального пространства для хранения доказательства. ϕ {\displaystyle \phi } ∃ x 1 ⋯ ∃ x n ϕ ( x 1 , … , x n ) {\displaystyle \exists x_{1}\cdots \exists x_{n}\phi (x_{1},\ldots ,x_{n})}
  • Любой класс в полиномиальной иерархии ( PH ) имеет TQBF как сложную проблему. Другими словами, для класса, включающего все языки L, для которых существует поливременная TM V, верификатор, такой что для всех входных данных x и некоторой константы i, которая имеет конкретную формулировку QBF, которая задается как таковая, что где 's являются векторами булевых переменных. x ∈ L ⇔ ∃ y 1 ∀ y 2 ⋯ Q i y i   V ( x , y 1 , y 2 , … , y i )   =   1 {\displaystyle x\in L\Leftrightarrow \exists y_{1}\forall y_{2}\cdots Q_{i}y_{i}\ V(x,y_{1},y_{2},\dots ,y_{i})\ =\ 1} ∃ ϕ {\displaystyle \exists \phi } ∃ x 1 → ∀ x 2 → ⋯ Q i x i →   ϕ ( x 1 → , x 2 → , … , x i → )   =   1 {\displaystyle \exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1} x i → {\displaystyle {\vec {x_{i}}}}
  • Важно отметить, что хотя язык TQBF определяется как набор истинных квантифицированных булевых формул, аббревиатура TQBF часто используется (даже в этой статье) для обозначения полностью квантифицированной булевой формулы, часто называемой просто QBF (квантифицированная булева формула, понимаемая как «полностью» или «полностью» квантифицированная). Важно различать контекстуально два использования аббревиатуры TQBF при чтении литературы.
  • TQBF можно рассматривать как игру, в которую играют два игрока с чередующимися ходами. Экзистенциально квантифицированные переменные эквивалентны понятию, что ход доступен игроку на ходу. Универсально квантифицированные переменные означают, что исход игры не зависит от того, какой ход игрок делает на этом ходу. Кроме того, TQBF, первый квантификатор которого является экзистенциальным, соответствует игре-формуле , в которой у первого игрока есть выигрышная стратегия.
  • TQBF, для которой квантифицированная формула находится в 2-CNF , может быть решена за линейное время с помощью алгоритма, включающего сильный анализ связности ее графа импликации . Проблема 2-выполнимости является частным случаем TQBF для этих формул, в которых каждый квантификатор является экзистенциальным. [17] [18]
  • Систематическое рассмотрение ограниченных версий квантифицированных булевых формул (дающих классификации типа Шефера) представлено в пояснительной статье Хуби Чена. [19]
  • Планарный TQBF, обобщающий планарный SAT , был доказан как PSPACE-полный Д. Лихтенштейном. [20]

Примечания и ссылки

  1. ^ M. Garey & D. Johnson (1979). Компьютеры и неразрешимость: Руководство по теории NP-полноты . WH Freeman, Сан-Франциско, Калифорния. ISBN 0-7167-1045-5.
  2. ^ А. Чандра, Д. Козен и Л. Стокмейер (1981). «Alternation». Журнал ACM . 28 (1): 114–133. doi : 10.1145/322234.322243 . S2CID  238863413.{{cite journal}}: CS1 maint: multiple names: authors list (link)
  3. ^ Ади Шамир (1992). «Ip = Pspace». Журнал ACM . 39 (4): 869–877. doi : 10.1145/146585.146609 . S2CID  315182.
  4. ^ Арора, Санджив; Барак, Боаз (2009), «Пространственная сложность», Computational Complexity , Кембридж: Cambridge University Press, стр. 78–94, doi :10.1017/cbo9780511804090.007, ISBN 978-0-511-80409-0, S2CID  262800930 , получено 2021-05-26
  5. ^ abc "QBFEVAL Home Page". www.qbflib.org . Получено 2021-02-13 .
  6. ^ abc "QBF Solvers | Beyond NP". beyondnp.org . Получено 2021-02-13 .
  7. ^ ab Балабанов, Валерий; Роланд Цзян, Цзе-Хонг; Шолль, Кристоф; Мищенко, Алан; К. Брайтон, Роберт (2016). "2QBF: Проблемы и решения" (PDF) . Международная конференция по теории и применению тестирования выполнимости : 453–459. Архивировано (PDF) из оригинала 13 февраля 2021 г. – через SpringerLink.
  8. ^ ab "QBFEVAL'20". www.qbflib.org . Получено 29.05.2021 .
  9. ^ abcdefghi Lonsing, Florian (декабрь 2017 г.). «Введение в решение QBF» (PDF) . www.florianlonsing.com . Получено 29 мая 2021 г. .
  10. ^ Рабе, Маркус Н. (15 апреля 2021 г.), MarkusRabe/кадет , получено 6 мая 2021 г.
  11. ^ Тентруп, Леандер (06 мая 2021 г.), ltentrup/caqe , получено 6 мая 2021 г.
  12. ^ "DepQBF Solver". lonsing.github.io . Получено 2021-05-06 .
  13. ^ "sKizzo - решатель QBF". www.skizzo.site . Получено 2021-05-06 .
  14. ^ abcd Шукла, Анкит; Бире, Армин; Зайдл, Мартина; Пулина, Лука (2019). Обзор приложений квантифицированных булевых формул (PDF) . 2019 IEEE 31st International Conference on Tools for Artificial Intelligence. стр. 78–84. doi :10.1109/ICTAI.2019.00020 . Получено 29 мая 2021 г.
  15. ^ Шэнь, Чжихэ. Использование решателей QBF для решения игр и головоломок (PDF) (диссертация). Бостонский колледж.
  16. ^ ab Janota, Mikoláš; Marques-Silva, Joao (2011). On Dedication MUS Membership with QBF. Principles and Practice of Constraint Programming – CP 2011. Vol. 6876. pp. 414–428. doi :10.1007/978-3-642-23786-7_32. ISBN 978-3-642-23786-7.
  17. ^ Кром, Мелвен Р. (1967). «Проблема решения для класса формул первого порядка, в которых все дизъюнкции являются двоичными». Zeitschrift für Mathematische Logik und Grundlagen der Mathematik . 13 (1–2): 15–20. дои : 10.1002/malq.19670130104..
  18. ^ Аспвалл, Бенгт; Пласс, Майкл Ф.; Тарьян, Роберт Э. (1979). «Линейный алгоритм проверки истинности некоторых квантифицированных булевых формул» (PDF) . Information Processing Letters . 8 (3): 121–123. doi :10.1016/0020-0190(79)90002-4..
  19. ^ Чен, Хуби (декабрь 2009 г.). «Встреча логики, сложности и алгебры». ACM Computing Surveys . 42 (1). ACM: 1–32. arXiv : cs/0611018 . doi : 10.1145/1592451.1592453. S2CID  11975818.
  20. ^ Лихтенштейн, Дэвид (1 мая 1982 г.). «Планарные формулы и их использование». Журнал SIAM по вычислениям . 11 (2): 329–343. doi :10.1137/0211025. ISSN  0097-5397. S2CID  207051487.
  • Фортнау и Хомер (2003) приводят некоторую историческую справку о PSPACE и TQBF.
  • Чжан (2003) приводит некоторые исторические сведения о булевых формулах.
  • Арора, Санджив. (2001). COS 522: Computational Complexity. Lecture Notes, Princeton University. Получено 10 октября 2005 г.
  • Fortnow, Lance & Steve Homer. (2003, июнь). Краткая история вычислительной сложности. Бюллетень Европейской ассоциации теоретической информатики , Колонка вычислительной сложности, 80. Получено 14 мая 2024 г.
  • Пападимитриу, CH (1994). Вычислительная сложность. Чтение: Addison-Wesley.
  • Сипсер, Майкл. (2006). Введение в теорию вычислений. Бостон: Томсон Курс Технологии.
  • Чжан, Линьтао. (2003). Поиск истины: методы выполнимости булевых формул. Получено 10 октября 2005 г.

Смотрите также

  • Библиотека квантифицированных булевых формул (QBFLIB)
  • Международный семинар по количественным булевым формулам
Retrieved from "https://en.wikipedia.org/w/index.php?title=True_quantified_Boolean_formula&oldid=1223886439"