Проверка формул с двумя квантификаторами ( ) - 2QBF

SAT решатели дают мощный способ проверить правильность логической формулы с одним квантификатором.

Например, чтобы проверить правильность , мы можем использовать SAT-решатель, чтобы определить, выполнимо ли . Чтобы проверить правильность , мы можем использовать SAT-решатель, чтобы определить, выполнимо ли . (Здесь - -вектор булевых переменных, а - булева формула.) $\exists x . \varphi(x)$ $\varphi(x)$ $\forall x . \varphi(x)$ $\neg \varphi(x)$ $x=(x_1,\dots,x_n)$ $n$ $\varphi$

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

Что если у нас есть формула с двумя квантификаторами? Являются ли они эффективными алгоритмами проверки достоверности: лучше, чем обычные алгоритмы для QBF? Чтобы быть более конкретным, у меня есть формула вида (или ), и хотите проверить его правильность. Есть ли хорошие алгоритмы для этого? Редактировать 4/8: я узнал, что этот класс формул иногда называют 2QBF, поэтому я ищу хорошие алгоритмы для 2QBF. $\forall x . \exists y . \psi(x,y)$ $\exists x . \forall y . \psi(x,y)$

Специализируясь далее: в моем конкретном случае у меня есть формула вида , правильность которого я хочу проверить, где - функции, которые производят битный вывод. Существуют ли алгоритмы проверки правильности этой конкретной формулы, более эффективные, чем универсальные алгоритмы для QBF? $\forall x . \exists y . f(x)=g(y)$ $f,g$ $k$

PS Я не спрашиваю о жесткости в худшем случае, в теории сложности. Я спрашиваю о практически полезных алгоритмах (так же, как современные решатели SAT практически полезны для многих задач, даже если SAT является NP-полной).

\forall x \exists y ψ (x, y)

$\forall x \exists y \ \psi(x,y)$ существу не эквивалентно .

\exists x \forall y ψ (x, y)

$\exists x \forall y \ \psi(x,y)$

Гек Беннетт

Я думаю, что OP подразумевает это неформально, потому что они оба трудны для решателей SAT и что решение любого из них было бы интересно

Suresh Venkat

@HuckBennett, я думаю, что оба имеют одинаковую твердость. (Доказательство: допустимо тогда и только тогда, когда есть. Поэтому, если у нас есть способ проверить правильность формул вида , мы также можем проверить правильность формул , указав и проверяем правильность .) Но в любом случае меня бы заинтересовали алгоритмы в любом случае ,

\exists x . \forall y . ψ (x, y)

$\exists x . \forall y . \psi(x,y)$

\neg \forall x . \exists y . \neg ψ (x, y)

$\neg \forall x . \exists y . \neg \psi(x,y)$

\forall x . \exists y . ψ (x, y)

$\forall x . \exists y . \psi(x,y)$

\exists x . \forall y . ψ (x, y)

$\exists x . \forall y . \psi(x,y)$

ψ^{'} (x, y) = \neg ψ (x, y)

$\psi'(x,y) = \neg \psi(x,y)$

\forall x . \exists y . ψ^{'} (x, y)

$\forall x . \exists y . \psi'(x,y)$

@DW, не обязательно, например, SAT и TAUT, как полагают, не имеют одинаковую сложность.

Каве

@chazisop: Я думаю, что OP просит алгоритмы / решатели

-SAT, а не общие решатели QBF. Однако существует множество решателей QBF. Смотрите вкладку «решатели» на qbflib.org

Π_{2} / Σ_{2}

$\Pi_2/\Sigma_2$

Гек Беннетт

Ответы:

Если я могу, довольно откровенно, рекламировать себя, мы написали статью об этом прошлом алгоритме на основе абстракций для 2QBF . У меня есть реализация для qdimacs, которую я могу предоставить, если хотите, но из моего опыта можно извлечь большую пользу из специализации алгоритма для конкретной проблемы. Существует также более старая статья «Сравнительное исследование алгоритмов 2QBF» , в которой также представлены довольно легко реализуемые алгоритмы.

Миколас
источник

Потрясающие! Спасибо, Миколас, это именно то, на что я надеялся.

Привет @DW рад, что мог помочь. Надеюсь, вы найдете это полезным. QBF - это совсем другой зверь, чем SAT, поэтому нужно быть немного осторожнее, потому что все может взорваться очень легко :-). Не стесняйтесь написать мне по электронной почте, если у вас есть более подробные вопросы о нашей работе.

Миколас

Я прочитал две статьи, связанные с этим, одна специально связана с 2QBF. Документы следующие:

Инкрементная детерминация , Маркус Н. Рабе и Санджит Сешиа, Теория и приложения тестирования удовлетворенности (SAT 2016).

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

Второй - это пошаговое решение QBF , Флориан Лонсинг и Уве Эгли.

Реализовано в инструменте с именем DepQBF . Он не накладывает никаких ограничений на количество чередования кванторов. Он начинается с предположения, что мы имеем тесно связанные формулы qbf. Он основан на пошаговом решении и не выбрасывает пункты, изученные во время последнего решения. Он добавляет предложения и кубы в текущую формулу и останавливается, если предложения или кубы пусты, представляя unsat или sat.

Изменить : просто для того, чтобы посмотреть, насколько хорошо эти подходы работают для 2QBF-тестов. Пожалуйста, посмотрите на результаты QBFEVal-2018 для результатов ежегодного конкурса QBF QBFEVAL . В 2019 году не было трека 2QBF.

В 2QBF Трек QBFEVAL-2018 DepQBF был победителем , КУРСАНТ был вторым в гонке.

Таким образом, эти два подхода на самом деле очень хорошо работают на практике (по крайней мере, в тестах QBFEVAL).

Pushpa
источник

Чтобы показать удовлетворенность , мы можем сыграть в игру с двумя игроками A и B, каждый из которых имеет доступ к решателю SAT. Если мы работаем в области , то на каждой итерации (включая первую) A выбирает элемент, который удовлетворяет установленному на нем ограничению (начинается с нуля), , в качестве нашего кандидата для выполнения формулы. Затем, B пытается удовлетворить с некоторым . Если B не может сделать это, это означает , что работа и мы сделали, в противном случае мы возвращаемся к A , и мы добавим его ограничение множество $\exists x \forall y \phi$ $D$ $a \in D$ $\neg \phi[a/x]$ $b \in B$ $a$ , который гарантирует, что такого рода ошибки больше не будут повторяться. У меня есть ощущение, что можно подумать о форме и сделать такую процедуру более стратегическим способом, полагаясь на некоторые достаточные подмножества, чтобы исключить любого данного кандидата, или некоторые известные симметрии, чтобы на ранних этапах исключить части этого поиска. Возможно, можно даже добавить свои собственные ограничения к начальному набору ограничений A. $\phi [b/y]$ $\phi$

Сэмюэль Шлезингер
источник

Это алгоритм, описанный в статье, которую цитирует Миколас ; см. алгоритм 1 этой статьи. Если в качестве отрицания формулы CNF указано

, то они показывают некоторые способы дальнейшего улучшения алгоритма, принимая во внимание форму

(как можно предположить из вашего ответа); см. раздел 5 этого документа. Хорошее объяснение элегантного и мощного подхода!

ϕ

$\phi$

ϕ

$\phi$

Это довольно хорошо, есть аналогия с противоборствующим машинным обучением, если вы щурились, и это действительно работает для любой дополненной решетки, где у вас есть своего рода решатель

Сэмюэль Шлезингер