Предложение эффективного решателя SAT с хорошим интерфейсом C ++ (или: Z3 мне подходит)?

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

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

  2. Проект должен по-прежнему активно поддерживаться и быть достаточно качественным, а не отказываться от какого-то выигравшего конкурс исследовательского проекта после публикации (см. picosat).

  3. Более того, поскольку я использую C ++, решающая программа должна обеспечивать эффективный и (возможно) хорошо написанный интерфейс C ++.

Первым кандидатом, который я рассмотрел, был Z3, но я смущен документацией и не могу понять, поддерживается ли пункт 1. выше, и может ли это быть излишним, учитывая, что мне нужен только SAT, а не SMT. Интерфейс C ++ также кажется очень простым в использовании, но я не могу вынести того факта, что мне приходится называть переменные простыми строками (это очень плохо сочетается с моим окружающим алгоритмом. Разве этого нельзя избежать?).

Не могли бы вы дать мне какое-нибудь предложение по поводу того, какой решатель SAT использовать, или пролить свет на сомнения относительно Z3?


c++ sat z3
person gigabytes    schedule 09.12.2016    source источник
comment
Никогда не использовал, но слышал об этом: minisat.se   -  person Fefux    schedule 09.12.2016
comment
(1a) Вы можете извлечь модели из Z3: см. rise4fun.com/Z3/tutorial/guide и выполните поиск get-model (1b) Извлечение различных моделей возможно, но требует написанного вручную цикла решения, ср. stackoverflow.com/questions/13395391   -  person Malte Schwerhoff    schedule 09.12.2016
comment
@Fefux спасибо. В то время как minisat хорош для экспериментов, я говорил именно о таком некомандированном исследовательском проекте. Он тоже довольно старый.   -  person gigabytes    schedule 09.12.2016
comment
@MalteSchwerhoff, спасибо. Знаете ли вы, можно ли избежать использования строк для именования переменных? Я бы предпочел целочисленные идентификаторы.   -  person gigabytes    schedule 09.12.2016
comment
z3 - это больше, чем решатель SAT, это решатель SMT, например, Yices, cvc4 и mathsat5. См. Sat Competition и соревнование smt для большего количества решателей. Некоторые решатели предоставляют интерфейс all-sat, возвращающий все возможные решения. Однако вы можете сделать это с помощью любого решателя, просто постепенно вызывая resolve () после добавления в формулу отрицания предыдущей модели.   -  person Patrick Trentin    schedule 09.12.2016
comment
@PatrickTrentin: да, но решатель должен иметь состояние, чтобы второй вызов не начинал повторять всю работу, но мог постепенно продолжить поиск. В любом случае, я посмотрю на конкурентов, но мне нужен был совет, потому что список довольно длинный, и нет никаких указаний на то, является ли решатель всего лишь исследовательским прототипом или продуктом производственного качества.   -  person gigabytes    schedule 09.12.2016
comment
Существует множество инкрементальных решателей SAT и SMT, я думаю, что все, что я назвал, таковыми являются, что означает, что они сохраняют изученные предложения при последующих поисках. Изучив отрицание предыдущей модели, вы в любом случае вызываете перезапуск поиска с уровня 0, поэтому AFAIK делает мало разница, реализуете ли вы эту схему извне или используете ту, которая имеет прямую поддержку для этого. Поскольку у меня конфликт интересов, я должен воздержаться от предложений по конкретному инструменту. Вы можете рассматривать уровень z3 production-quality, как и многие другие.   -  person Patrick Trentin    schedule 09.12.2016
comment
Как вы говорите, Z3 может оказаться излишним. Однако он поддерживает переменные с целыми числами; Z3_mk_const принимает символ (не строку), и вы можете создавать символы с целыми числами через Z3_mk_int_symbol.   -  person Christoph Wintersteiger    schedule 09.12.2016
comment
@ChristophWintersteiger, о, понятно ... Значит, C ++ API просто не поддерживает эту функцию?   -  person gigabytes    schedule 09.12.2016
comment
C ++ API предоставляет только некоторые удобные функции, такие как классы expr, которые заботятся о подсчете ссылок. Он предназначен для использования в сочетании с C API. Однако в этом конкретном случае он предоставляет context :: int_symbol (int n).   -  person Christoph Wintersteiger    schedule 10.12.2016
comment
Ах я вижу. Спасибо. Кстати, о том, что Z3 перебор: вот в чём тема. Есть какие-нибудь подсказки по поводу быстрого производственного решателя SAT?   -  person gigabytes    schedule 10.12.2016
comment
@gigabytes Было бы здорово, если бы вы могли сообщить о своих выводах, например если у вас хватило времени сравнить решатели, которые участвовали в соревнованиях SAT и SMT (как было предложено Патриком)   -  person Malte Schwerhoff    schedule 13.12.2016
comment
Да, напишу ответ, когда удастся сделать сравнение :)   -  person gigabytes    schedule 13.12.2016
comment
@gigabytes Вы пробовали посмотреть Программирование набора ответов и решатели #SAT? Они перечисляют все возможные решения данной формулы. Я бы порекомендовал решить Potassco в качестве отправной точки, однако я не уверен, насколько хорош этот API. Я использовал sharpCDCL для решения некоторых реальных проблем. Он идеально соответствовал моим требованиям, но с точки зрения API это в основном минисат.   -  person CaptainTrunky    schedule 08.03.2017
comment
@gigabytes И, кстати, попробуйте поискать решатель глюкозы. Он основан на MiniSat и содержится в хорошем состоянии. Он показал лучшую производительность в моих собственных проектах (за исключением собственного коммерческого решателя).   -  person CaptainTrunky    schedule 09.03.2017
comment
@CaptainTrunky, это интересно, спасибо!   -  person gigabytes    schedule 09.03.2017

Ответы (1)


arrow_upward
1
arrow_downward

Если вы хотите поработать над исправлением сборки для разных платформ (или вам они не нужны), MiniSat's интерфейс довольно приятный. Обратите внимание, что он больше не поддерживается.

Также существует Gluosis, который использует интерфейс MiniSat и относительно активно поддерживается. Он также намного лучше показывает себя в соревнованиях SAT, чем MiniSat.

Прежде чем выбрать один или другой, вы должны понять, что, хотя глюкоза обычно побеждает MiniSat в соревнованиях SAT, ваш вариант использования может не решать соревнования SAT. Например, наш проект обычно генерирует удовлетворительные формулы, где задача состоит в том, чтобы найти одно из (обычно) множества заданий SAT, и MiniSat обычно там превосходит Gluosis. OTOH, если ваш проект в основном генерирует неудовлетворительные формулы или формулы с единственным решением, которое нужно найти, Gluosis, вероятно, будет лучше, поскольку он оптимизирован для быстрого поиска доказательств UNSAT, а не для поиска заданий SAT.

Еще один решатель, с которым у меня был опыт встраивания, - это CryptoMiniSat. Он имеет разумный интерфейс C ++ и очень активно поддерживается. Когда у меня возникала проблема или ошибка, обычно ее исправляли в течение недели. Однако он редко предоставляет стабильные выпуски, поэтому, если вы его используете, вы, скорее всего, в конечном итоге будете жить за счет определенного хэша, а не правильного выпуска.

Еще одно замечание: Gluosis предоставляет параллельный решатель, но с довольно интересной лицензией. CMSat предоставляет параллельный решатель по лицензии MIT. MiniSat имеет очень либеральную лицензию, но не имеет параллельного варианта.

person Xarn    schedule 13.10.2017