Описание тега sat4j
Проект Sat4j стартовал в 2004 году как реализация на Java спецификации MiniSAT Никласа Эна и Никласа Соренсона: расширяемый решатель SAT, Никлас Эен и Никлас Соренсон. Труды Шестой Международной конференции по теории и приложениям проверки выполнимости, LNCS 2919, стр 502-518, 2003.
Оригинальная реализация C++ доступна здесь.
Несмотря на то, что общая алгоритмика решателя была соблюдена, дизайн был адаптирован к практике Java, а первоначальный дизайн был расширен, чтобы позволить тестировать несколько эвристик и схем обучения.
С годами была добавлена поддержка псевдобулевой оптимизации (2005 г.), преобразования CSP в SAT (2005 г.), MaxSat (2006 г.) и MUS (2011 г.).
С июня 2008 года платформа Eclipse полагается на Sat4j для решения своих программных зависимостей. Таким образом, Sat4j, вероятно, является наиболее широко развернутой и используемой библиотекой на основе Sat в мире.
Если вы новичок в проблеме удовлетворенности, вы можете сначала взглянуть на страницу википедии, посвященную задаче логической выполнимости.
Эти опросы также могут вас заинтересовать. Курс Армина Биэра по формальным системам является хорошим началом для более глубокого понимания нынешнего интереса к решателям SAT для проверки программного и аппаратного обеспечения.
У Юджина Голдберга также есть хороший и в чем-то нестандартный способ представить современные решатели SAT в своем трехчастном курсе по SAT.
Мы также прочитали лекцию по SAT для летней школы по технологиям, системам и приложениям верификации в октябре 2009 года.
Есть много международных соревнований, организованных вокруг этих задач, где вы можете увидеть sat4j в действии:
Вот список программного обеспечения, использующего SAT4J:
https://stackru.com/images/d30cafa7183de4081d18cf59b673c120d23ee09b.png
Вот документация по использованию SAT4J: http://www.sat4j.org/doc.php.