2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




 
 Посоветуйте SAT решатель
Сообщение22.02.2021, 07:45 
Добрый день.
Нужен SAT solver, чтобы решить уравнение/систему уравнений алгебры логики. Например, я даю решателю формулу $x \bigwedge y$ и должен получить все возможные означивания, которые делают формулу истинной, в данном случае ответ: $[x=1,y=1]$. Подскажите такие решатели. Будет плюсом, если они написаны на джаве или си++.

 
 
 
 Re: Посоветуйте SAT решатель
Сообщение22.02.2021, 11:16 
Аватара пользователя
Вам нужно что-то открытое? Если необязательно, то Mathematica такое умеет. Ваш примерчик будет выглядеть так: SatisfiabilityInstances[x && y, {x, y}]

 
 
 
 Re: Посоветуйте SAT решатель
Сообщение22.02.2021, 13:44 
Можете посмотреть cryptominisat, например. Или вот у Армина Бире есть несколько отличных решателей: https://github.com/arminbiere. Вообще, есть сайты, где выкладываются результаты ежегодных соревнований решателей, например, http://www.satcompetition.org/. Дальше по ссылкам можно найти исходные коды многих из них.
Ответом, как правило, служит первое найденное решение. Если вам нужны все, можно по мере нахождения решений добавлять в формулу соответствующие дизъюнкции, запрещающие их (ах, да, общепринятый формат задач, принимаемый в качестве входа - DIMACS).

 
 
 [ Сообщений: 3 ] 


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group