Как назначить целочисленные значения для переменных булевой формулы, используя sat4j в Java?

Question

Я совершенно новичок в решении sat4j и изучаю булевы выполнимые проблемы; и я застрял. Я хочу сделать программу, которая решает целочисленные переменные, которые в виде логической формулы, как;

x1

Answer 1

Не уверен, что SAT4J выполняет SMT-решение... Вам следует искать SMT-решатели, которые поддерживают линейную арифметику (в вашем случае кажется, что только логика различий тоже подойдет). Вы можете проверить: Z3 (SMT-решатель от Microsoft), CVC4 и Yices. Более обширный список здесь: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

Надеюсь это поможет...