Посоветуйте SAT решатель

[Jaxel]

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

[Aritaborian]

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

[Sender]

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