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

«QBF» перенаправляется сюда. Чтобы узнать о руководящем органе баскетбола в Катаре, см. Катарскую федерацию баскетбола .

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

Обзор

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

$\forall x\ \exists y\ \exists z\ ((x\lor z)\land y)$

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

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

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

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

Пренекс нормальная форма

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

$\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})$

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

$\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

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

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

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

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

Если $Q_{1}=\exists$, затем вернитесь $A\lor B$. Если $Q_{1}=\forall$, затем вернитесь $A\land B$.

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

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

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

Несмотря на PSPACE-полноту QBF, для решения этих случаев было разработано множество решателей. (Это аналогично ситуации с SAT , единственной версией квантора существования; даже несмотря на то, что она NP-полная , все же возможно эвристически решить многие экземпляры SAT.) Особое внимание привлек случай, когда имеется только два квантора, известный как 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-полной задачей. Быть PSPACE-полным означает, что язык находится в PSPACE и что он также является PSPACE-сложным . Приведенный выше алгоритм показывает, что TQBF находится в PSPACE.Чтобы показать, что TQBF является PSPACE-сложным, необходимо показать, что любой язык класса сложности PSPACE можно свести к TQBF за полиномиальное время. Т.е.,

$\forall L\in {\mathsf {PSPACE}},L\leq _{p}\mathrm {TQBF} .$

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

$x\in L\iff f(x)\in \mathrm {TQBF} .$

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

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

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

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

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

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

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

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

$\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})$ сделано, $\phi _{c_{1},c_{2},t}\iff \phi _{c_{3},c_{4},\lceil t/2\rceil }$.

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

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

Разное

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

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

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

См. также

• Теорема Кука – Левина , утверждающая, что SAT NP -полна.
• Обобщенная география

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

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