Предложение эффективного решателя SAT с хорошим интерфейсом C ++ (или: Z3 хорош для меня)?
Для проекта, который я начинаю, мне нужно будет использовать SAT-решатель. Я использовал некоторые из них раньше, но в основном для экспериментов, в то время как здесь основным ограничением для проекта является хорошая производительность. Я пытаюсь найти альтернативы и пытаюсь понять, как каждая альтернатива позиционируется в соответствии с моими конкретными требованиями. Особенно:
-
Мне нужно будет извлекать удовлетворяющие задания, а не только проверять их на удовлетворенность, а решатель должен позволять мне многократно решать одну и ту же формулу в поисках различных возможных удовлетворяющих заданий, в конечном итоге итерируя по всем из них, эффективным способом (например, без меня). необходимость добавить пункт и начать все сначала).
-
Проект должен по-прежнему активно поддерживаться и иметь достаточно производственное качество, а не какой-либо победивший в конкурсе исследовательский проект, оставленный после публикации (см.
picosat). -
Более того, поскольку я использую C ++, решатель должен обеспечить эффективный и (возможно) хороший письменный интерфейс C ++.
Первым кандидатом, которого я рассмотрел, был Z3, но я смущен документами и не могу понять, поддерживается ли пункт 1. выше, и может ли это быть излишним, учитывая, что мне нужен только SAT, а не SMT. Интерфейс C ++ также кажется очень простым в использовании, но я не могу смириться с тем фактом, что мне приходится называть переменные простыми строками (это очень плохо сочетается с моим окружающим алгоритмом. Разве этого не избежать?).
Итак, можете ли вы дать мне несколько советов о том, какой SAT решатель использовать, или пролить свет на сомнения относительно Z3?
Решение
Если вы хотите поработать над исправлением сборки для разных платформ (или вообще не нужны), Интерфейс MiniSat довольно приятный. Обратите внимание, что на самом деле это больше не поддерживается.
Существует также глюкоза, который разделяет интерфейс MiniSat и относительно активно поддерживается. Кроме того, он намного лучше выступает на соревнованиях SAT, чем MiniSat.
Прежде чем выбрать один или другой, вам необходимо понять, что, хотя Глюкоза обычно побеждает MiniSat в соревнованиях SAT, ваш вариант использования может не решать соревнования SAT. Например, наш проект обычно генерирует удовлетворительные формулы, где задача состоит в том, чтобы найти одно из (обычно) многих заданий SAT, а MiniSat обычно превосходит Глюкозу там. OTOH, если ваш проект в основном генерирует неудовлетворительные формулы или формулы с единственным решением, которое будет найдено, Глюкоза, вероятно, будет лучше, так как она оптимизирована для быстрого поиска доказательств UNSAT, а не для определения назначений SAT.
Еще один решатель, который у меня был опыт встраивания, CryptoMiniSat. Он имеет разумный интерфейс C ++ и поддерживается очень активно. Когда у меня была проблема или ошибка, она обычно исправлялась в течение недели. Однако он редко предоставляет стабильные выпуски, поэтому, если вы используете его, вы, скорее всего, будете жить за счет определенного хеша, а не правильного выпуска.
Еще одна вещь, на которую следует обратить внимание: Glucose предоставляет параллельный решатель, но с довольно интересной лицензией. CMSat предоставляет параллельный решатель по лицензии MIT. У MiniSat очень либеральная лицензия, но нет параллельного варианта вообще.
Другие решения
Других решений пока нет …