Истинная количественная логическая формула - True quantified Boolean formula

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

Обзор

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

{\ Displaystyle \ forall x \ \ существует y \ \ существует z \ ((x \ lor z) \ земля y)}

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

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

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

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

Prenex нормальная форма

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

{\ displaystyle \ displaystyle \ exists x_ {1} \ forall x_ {2} \ exists x_ {3} \ cdots Q_ {n} x_ {n} \ phi (x_ {1}, x_ {2}, x_ {3}) , \ точки, x_ {n})}

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

{\ Displaystyle \ Displaystyle \ существует 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

{\ Displaystyle Q_ {1} x_ {1} Q_ {2} x_ {2} \ cdots Q_ {n} x_ {n} \ phi (x_ {1}, x_ {2}, \ dots, x_ {n}) .}

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

{\ displaystyle A = Q_ {2} x_ {2} \ cdots Q_ {n} x_ {n} \ phi (0, x_ {2}, \ dots, x_ {n}),}

{\ displaystyle B = Q_ {2} x_ {2} \ cdots Q_ {n} x_ {n} \ phi (1, x_ {2}, \ dots, x_ {n}).}

Если , то вернись . Если , то вернись . ${\ Displaystyle Q_ {1} = \ существует}$ ${\ Displaystyle A \ lor B}$ ${\ Displaystyle Q_ {1} = \ forall}$ ${\ displaystyle A \ land B}$

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

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

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

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

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

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

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

Приложения

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

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

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

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

Определение того, принадлежит ли предложение в невыполнимой формуле в конъюнктивной нормальной форме некоторому минимально невыполнимому подмножеству и принадлежит ли предложение в выполнимой формуле максимально выполнимому подмножеству
Кодировки согласованного планирования
Проблемы, связанные с ASP
Абстрактная аргументация
Проверка модели линейной темпоральной логики
Недетерминированное включение языка конечных автоматов
Синтез и надежность распределенных систем

Расширения

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

PSPACE-полнота

В теории сложности язык TQBF служит канонической задачей PSPACE-complete . Полная 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 \ iff f (x) \ in \ mathrm {TQBF}.}

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

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

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

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

Ведь вычисление включает рекурсивную оценку, ищущую так называемую «среднюю точку» . В этом случае перепишем формулу следующим образом: ${\ displaystyle t> 1}$ ${\ displaystyle \ phi _ {c_ {1}, c_ {2}, t}}$ ${\ displaystyle m_ {1}}$

{\ displaystyle \ phi _ {c_ {1}, c_ {2}, t} = \ exists m_ {1} (\ phi _ {c_ {1}, m_ {1}, \ lceil t / 2 \ rceil} \ клин \ phi _ {m_ {1}, c_ {2}, \ lceil t / 2 \ rceil}).}

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

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

{\ 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}).}

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

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

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

Разное

Одной из важных подзадач в TQBF является проблема логической выполнимости . В этой задаче вы хотите знать, может ли данная логическая формула стать истинной с помощью некоторого присвоения переменных. Это эквивалентно TQBF с использованием только экзистенциальных квантификаторов: ${\ displaystyle \ phi}$ ${\ Displaystyle \ существует x_ {1} \ cdots \ exists x_ {n} \ phi (x_ {1}, \ ldots, x_ {n})}$ Это также пример большего результата NP ⊆ PSPACE, который непосредственно следует из наблюдения, что верификатор с полиномиальным временем для доказательства языка, принятого NTM ( недетерминированная машина Тьюринга ), требует полиномиального пространства для хранения доказательства.
Для любого класса в полиномиальной иерархии ( PH ) TQBF представляет собой сложную проблему. Другими словами, для класса, включающего все языки L, для которых существует поли-временный TM V, верификатор, такой, что для всех входных x и некоторой константы i, ${\ 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}$ который имеет конкретную формулировку QBF, которая задается как ${\ Displaystyle \ существует \ phi}$ такой, что где - векторы логических переменных. ${\ 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}$ ${\ displaystyle {\ vec {x_ {i}}}}$
Важно отметить, что хотя язык TQBF определен как набор истинных количественных логических формул, аббревиатура TQBF часто используется (даже в этой статье) для обозначения полностью количественно выраженной логической формулы, часто называемой просто QBF (количественно выраженная логическая формула). формула, понимаемая как «полностью» или «полностью» количественно определенная). Важно различать контекстуально два использования аббревиатуры TQBF при чтении литературы.
TQBF можно рассматривать как игру между двумя игроками с чередованием ходов. Переменные, определяемые количественно, эквивалентны представлению о том, что игрок может сделать ход в свой ход. Универсальные количественные переменные означают, что исход игры не зависит от того, какой ход игрок делает в этот ход. Кроме того, TQBF, первый квантор которого является экзистенциальным, соответствует игре по формуле, в которой первый игрок имеет выигрышную стратегию.
TQBF, для которого количественная формула находится в 2-CNF, может быть решена за линейное время с помощью алгоритма, включающего строгий анализ связности его графа импликации . Проблема 2-выполнимости - это частный случай TQBF для этих формул, в котором каждый квантор экзистенциальный.
Существует систематическая обработка ограниченных версий количественных булевых формул (дающих классификации типа Шефера), представленная в пояснительной статье Хуби Чена.
Планарный TQBF, обобщающий Planar SAT , был доказан Д. Лихтенштейном как PSPACE-полный.

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

^ М. Garey и Д. Джонсон (1979). Компьютеры и непоколебимость: руководство по теории NP-полноты . WH Freeman, Сан-Франциско, Калифорния. ISBN 0-7167-1045-5.
^ A. Chandra, Д. Кодзэн и Л. Stockmeyer (1981). «Чередование» . Журнал ACM . 28 (1): 114–133. DOI : 10.1145 / 322234.322243 .CS1 maint: несколько имен: список авторов ( ссылка )
↑ Ади Шамир (1992). «Ip = Pspace» . Журнал ACM . 39 (4): 869–877. DOI : 10.1145 / 146585.146609 . S2CID 315182 .
^ Арора, Санджив; Barak, Боаз (2009), "сложность Space" , вычислительная сложность , Кембридж. Cambridge University Press, стр 78-94, DOI : 10,1017 / cbo9780511804090.007 , ISBN 978-0-511-80409-0, получено 2021-05-26
^ ^a ^b ^c "Домашняя страница QBFEVAL" . www.qbflib.org . Проверено 13 февраля 2021 .
^ ^a ^b ^c "Решатели QBF | Помимо NP" . Beyondnp.org . Проверено 13 февраля 2021 .
^ ^a ^b Балабанов Валерий; Роланд Цзян, Цзе-Хун; Шолль, Кристоф; Мищенко, Алан; К. Брайтон, Роберт (2016). «2QBF: проблемы и решения» (PDF) . Международная конференция по теории и приложениям проверки выполнимости: 453–459. Архивировано (PDF) из оригинала 13 февраля 2021 года - через SpringerLink.
^ ^а ^б "QBFEVAL'20" . www.qbflib.org . Проверено 29 мая 2021 .
^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ Лонсинг, Флориан (декабрь 2017 г.). «Введение в решение QBF» (PDF) . www.florianlonsing.com . Проверено 29 мая 2021 года .
^ Раба, Маркус Н. (2021-04-15), MarkusRabe / курсант , извлекается 2021-05-06
^ Tentrup, Leander (06.05.2021), ltentrup / caqe , получено 06.05.2021
^ "DepQBF Solver" . lonsing.github.io . Проверено 6 мая 2021 .
^ "sKizzo - решатель QBF" . www.skizzo.site . Проверено 6 мая 2021 .
^ ^a ^b ^c ^d Шукла, Анкит; Бир, Армин; Зайдл, Мартина; Пулина, Лука (2019). Обзор приложений квантифицированных булевых формул (PDF) . 31-я Международная конференция IEEE 2019 по инструментам для искусственного интеллекта. С. 78–84. DOI : 10.1109 / ICTAI.2019.00020 . Проверено 29 мая 2021 года .
^ Шэнь, Чжихэ. Использование решателей QBF для решения игр и головоломок (PDF) (Диссертация). Бостонский колледж.
^ ^a ^b Янота, Миколаш; Маркес-Силва, Жоао (2011). О принятии решения о членстве MUS в QBF . Принципы и практика программирования в ограничениях - CP 2011. 6876 . С. 414–428. DOI : 10.1007 / 978-3-642-23786-7_32 . ISBN 978-3-642-23786-7.
^ Кром, Мелвен Р. (1967). «Проблема решения для класса формул первого порядка, в котором все дизъюнкции двоичны». Zeitschrift für Mathematische Logik und Grundlagen der Mathematik . 13 (1-2): 15-20. DOI : 10.1002 / malq.19670130104 ..
^ Аспвалл, Бенгт; Plass, Майкл Ф .; Тарьян, Роберт Э. (1979). «Алгоритм линейного времени для проверки истинности определенных количественных логических формул» (PDF) . Письма об обработке информации . 8 (3): 121–123. DOI : 10.1016 / 0020-0190 (79) 90002-4 ..
↑ Чен, Хьюби (декабрь 2009 г.). «Встреча логики, сложности и алгебры». ACM Computing Surveys . ACM. 42 (1): 1–32. arXiv : cs / 0611018 . DOI : 10.1145 / 1592451.1592453 . S2CID 11975818 .
^ Лихтенштейн, Дэвид (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). Введение в теорию вычислений. Бостон: Технологии курса Томсона.
Чжан, Линтао. (2003). В поисках истины: методы выполнимости булевых формул . Проверено 10 октября 2005 года.

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

Теорема Кук-Левин , заявив , что СБ является NP-полной
Обобщенная география

внешние ссылки

Библиотека количественных булевых формул (QBFLIB)
Международный семинар по количественным булевым формулам

[1] М. Garey и Д. Джонсон (1979). Компьютеры и непоколебимость: руководство по теории NP-полноты . WH Freeman, Сан-Франциско, Калифорния. ISBN 0-7167-1045-5.

[2] A. Chandra, Д. Кодзэн и Л. Stockmeyer (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 . S2CID 315182 .

[4] Арора, Санджив; Barak, Боаз (2009), "сложность Space" , вычислительная сложность , Кембридж. Cambridge University Press, стр 78-94, DOI : 10,1017 / cbo9780511804090.007 , ISBN 978-0-511-80409-0, получено 2021-05-26

[:0-5] "Домашняя страница QBFEVAL" . www.qbflib.org . Проверено 13 февраля 2021 .

[:1-6] "Решатели QBF | Помимо NP" . Beyondnp.org . Проверено 13 февраля 2021 .

[:2-7] Балабанов Валерий; Роланд Цзян, Цзе-Хун; Шолль, Кристоф; Мищенко, Алан; К. Брайтон, Роберт (2016). «2QBF: проблемы и решения» (PDF) . Международная конференция по теории и приложениям проверки выполнимости: 453–459. Архивировано (PDF) из оригинала 13 февраля 2021 года - через SpringerLink.

[:3-8] а ^б "QBFEVAL'20" . www.qbflib.org . Проверено 29 мая 2021 .

[:4-9] ^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ Лонсинг, Флориан (декабрь 2017 г.). «Введение в решение QBF» (PDF) . www.florianlonsing.com . Проверено 29 мая 2021 года .

[10] Раба, Маркус Н. (2021-04-15), MarkusRabe / курсант , извлекается 2021-05-06

[11] Tentrup, Leander (06.05.2021), ltentrup / caqe , получено 06.05.2021

[12] "DepQBF Solver" . lonsing.github.io . Проверено 6 мая 2021 .

[13] "sKizzo - решатель QBF" . www.skizzo.site . Проверено 6 мая 2021 .

[:5-14] Шукла, Анкит; Бир, Армин; Зайдл, Мартина; Пулина, Лука (2019). Обзор приложений квантифицированных булевых формул (PDF) . 31-я Международная конференция IEEE 2019 по инструментам для искусственного интеллекта. С. 78–84. DOI : 10.1109 / ICTAI.2019.00020 . Проверено 29 мая 2021 года .

[15] Шэнь, Чжихэ. Использование решателей QBF для решения игр и головоломок (PDF) (Диссертация). Бостонский колледж.

[:6-16] Янота, Миколаш; Маркес-Силва, Жоао (2011). О принятии решения о членстве MUS в QBF . Принципы и практика программирования в ограничениях - CP 2011. 6876 . С. 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. DOI : 10.1002 / malq.19670130104 ..

[18] Аспвалл, Бенгт; Plass, Майкл Ф .; Тарьян, Роберт Э. (1979). «Алгоритм линейного времени для проверки истинности определенных количественных логических формул» (PDF) . Письма об обработке информации . 8 (3): 121–123. DOI : 10.1016 / 0020-0190 (79) 90002-4 ..

[19] Чен, Хьюби (декабрь 2009 г.). «Встреча логики, сложности и алгебры». ACM Computing Surveys . ACM. 42 (1): 1–32. arXiv : cs / 0611018 . DOI : 10.1145 / 1592451.1592453 . S2CID 11975818 .

[20] Лихтенштейн, Дэвид (1982-05-01). «Планарные формулы и их использование» . SIAM Journal on Computing . 11 (2): 329–343. DOI : 10.1137 / 0211025 . ISSN 0097-5397 .

Languages

In other projects