Проверьте комбинаторные кодеры CNF SAT?

Question

Я пытаюсь решить комбинаторную проблему, используя SAT Solver.

Это включает в себя следующие этапы:

1. Encode проблему как набор логических выражений.
2. Перевести конъюнкцию выражений в CNF/DIMACS
   (с использованием домашнего выращены инструменты, bc2cnf, bool2cnf или Limboole)
3. Решить CNF
   (используя решателей SAT как Cryptominisat, Plingeling, Clasp или Z3)
4. Перевести решение (предполагая результат «SAT») обратно в проблемную область

Это работает в моем случае для небольших образцов. Но для более сложных задач решение SAT занимает несколько часов или даже дней, не придя к выводу SAT/UNSAT. Я пытаюсь настроить кодировку, чтобы найти решение. Но чем больше усилий я вкладываю в свою кодировку, тем менее я уверен, что моя кодировка действительно правильная (т. Е. Эквивалент «выполнимости»).

Шаг от булевого выражения до CNF довольно запутан, чтобы быть эффективным с точки зрения управляемого количества предложений и переменных. Это больно ждать возраста для решателя SAT и не быть уверенным, что время тратится на правильный путь.

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

Мой вопрос:

Как я мог убедиться, что данное кодирование является действительным представлением исходного логического выражения?

Из литературы я знаю решения некоторых проблем, которые я мог бы перевести на переменные назначения, чтобы получить доверие к процессу кодирования. Но из-за Tseitin encoding большинство переменных в моем CNF являются вспомогательными (переключающими) переменными. Без Tseitin encoding мой CNF был бы слишком велик, чтобы быть разрешимым. Поэтому я не могу просто проверить, выполнено ли каждое предложение CNF известным решением.

Я попытался перевести CNF обратно в булевы выражения, используя cnf2aig, но инструмент все еще находится в зачаточном состоянии. Без переключения переменных просто проверить привязку к булевым выражениям первичных переменных задачи.

Существует несколько публикаций о подходах «CNF to circuit», но ни один из них не предоставляет полезный инструмент.

Есть ли какая-либо передовая практика для проведения такой проверки?

Answer 1

Так что вы просите это:

Учитывая логическое выражение B и C CNF, есть способ узнать, есть ли они equisatisfiable?

Или другими словами:

Существует модель, которая удовлетворяет B, но не C, или что удовлетворяет С, но не Б? Если такой модели не существует, то оба они являются равными.

Мое решение этой проблемы было бы следующее:

1. Я хотел бы использовать заведомо исправный программное обеспечение (например, ваш неоптимизированная код или инструмент третьей стороной), чтобы сформировать заведомо исправный CNF D из булево выражение.

2. Использование Цейтина для генерации CNF для! B от C и D. I.e. интерпретировать CNF для C как произведение сумм (объединение дизъюнкции) и инвертировать все выражение. Давайте назовите полученные CNF C 'для обратного C и D' для обратного D.

   Таким образом, модель, которая удовлетворяет C, не будет удовлетворять C 'и наоборот. Аналогично для D и D '.

3. Используйте SAT-решатель, чтобы найти модель, которая удовлетворяет требованиям C и D '. Такая модель должна удовлетворять C, но не B.

4. Используйте решатель SAT, чтобы найти модель, которая удовлетворяет C»и D. Такая модель будет удовлетворять B, но не C.

5. Если шаги 3. и 4. оба не дают модель (unsat), тогда вы доказали, что B и C являются достаточно уместными.

Этапы 3. и 4. легки. Просто создайте одну большую CNF, содержащую все предложения из двух CNF. Все переменные из B должны быть закодированы с одним и тем же литералом в обоих CNF, а вспомогательные переменные должны быть выделены из отдельных пулов.

В зависимости от вашей проблемы решающие шаги 3. и 4. могут быть довольно дорогостоящими. Таким образом, такой подход может быть осуществим только в том случае, если вы можете разделить проблему на более мелкие куски, которые могут быть проверены независимо друг от друга.

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

https://github.com/cliffordwolf/yosys/tree/master/libs/ezsat

У порожден этой библиотекой не очень эффективно! Но это хорошо протестировано.