Преобразование (математических) задач в экземпляры SAT

22

То, что я хочу сделать, это превратить мою математическую задачу в булеву проблему удовлетворенности (SAT), а затем решить ее с помощью SAT Solver. Интересно, знает ли кто-нибудь руководство, руководство или что-нибудь, что поможет мне преобразовать мою проблему в экземпляр SAT.

Кроме того, я хочу решить эту проблему лучше, чем экспоненциально. Я надеюсь, что SAT Solver поможет мне.

Dchris
источник
1
У SAT нет эффективных методов ... но взгляните на эти слайды
Файез Абдлразак, Deab,
пожалуйста, посмотрите также здесь: cs.stackexchange.com/questions/12135/convert-problem-to-cnf
Дхрис
Просто быстрое и грязное решение, прежде чем вы попробуете что-то еще, на случай, если вы просто захотите что-то протестировать: cryptlogver . Инструмент говорит, что он предназначен для криптографии, но сработает. Более того, синтаксис языка, который вы будете использовать, очень похож, поэтому у вас не будет много проблем. Установка не сложная, но квартус большой, так что возьмите чашку кофе.
absinthe_minded
1
См. Также связанный вопрос cs.stackexchange.com/q/30790
Андраш Саламон

Ответы:

20

Глава 2 SAT Handbook (Стивен Прествич) рассказывает о том, как с некоторой глубиной превратить проблемы дискретного решения в CNF. (К сожалению, я не думаю , что есть проект версия онлайн - вероятно , лучше всего обратиться в местную библиотеку.) Некоторые из других цитированных ссылок в причудливых обзорных Magnus Бьорк Успешных методов СБ кодирования также полезны.

Если ваши проблемы непрерывны или вас особенно интересуют системы неравенств, то другие виды решателей с большей вероятностью будут полезны. Как указывает Кайл, SMT-решатели (такие как Z3 , Yices или OpenSMT ) могут быть полезны, хотя традиционно теории SMT обычно ориентированы на проверку компьютерного программного обеспечения, поэтому решатели SMT обычно имеют большую поддержку для таких вещей, как выражения с интервалами целых чисел. , но может плохо работать на ограничениях приемистости. Для проблем, которые естественным образом выражаются в виде систем неравенств, CPLEX - это тот, который побеждает (раньше он был доступен для академического использования бесплатно, и он все еще может быть). Для некоторых комбинаторных задач решения (например, поискупаковки прямоугольников в квадрат ), решатели ограничений, такие как Minion, превосходят решатели SAT и часто проще в использовании.

Андраш Саламон
источник
13

Если вы не переводите математические задачи в экземпляры SAT в качестве учебного упражнения, ваше время будет гораздо более плодотворно потрачено на изучение теорий выполнимости по модулю . SMT позволит вам выражать уравнения и другие ограничения гораздо более естественно, чем в виде логических SAT. Некоторые решатели SMT поддерживают экзистенциальные и универсальные квантификаторы, что позволяет вам выйти за пределы NP и выражать проблемы PSPACE.

Помимо того, что SMT решают более быстро, они работают быстрее. Не P = NP быстрее, но более эффективен в том смысле, что хороший решатель SMT не отбрасывает специфическую для теории структурную информацию, которая помогает направлять решатель через пространство поиска. Выполнение редукции Karp непосредственно для экземпляра SAT заставляет решатель SAT заново изучать всю эту структуру, часто по экспоненциальной стоимости. Например, тот факт, что сложение является коммутативным, теряется в решателях SAT как на основе DPLL, так и на основе локального поиска; решатель не знает, что он имеет дело с числами вообще! Чтобы избежать попытки перестановок x + y + z = 10, для SAT-решателя необходим код с нарушением симметрии, который требует обнаружения автоморфизма графа. Наилучшие современные алгоритмы распознавания автоморфизмов графа требуют экспоненциального по времени числа вершин в худшем случае,

Кайл Джонс
источник
2
вы предлагаете какой-либо конкретный smt решатель?
Дхрис
5

Два инструмента, которые конвертируют языки высокого уровня в SMT или CNF.

CVC Синтаксис близок к CAS.

CBMC Конвертирует C-программу в CNF, что позволяет делать утверждения. Утверждения либо всегда верны, либо, если ложно, найден ввод контрпримеров. CBMC развертывает циклы, поэтому некоторые программы на C имеют экспоненциально большой CNF / SMT.

elluser
источник
Похоже, CBMC не конвертирует произвольную C-программу в CNF; он создает файл CNF на основе C-программы, которая выполняет статический анализ целочисленных переполнений, переполнений буфера и тому подобного.
vy32