Search code examples
javasatisfiabilitysatsat-solverssat4j

How to assign integer values to boolean formula's variables using sat4j in java?

I am totally new for sat4j solver and researching boolean satisfiable problems; and i am stuck.I want to make a program which solves integer variables which are in boolean formula like;

x1 < x2 + x3 the user enter that formula and my program satisfies this formula (return true) like x1 = 5 , x2 = 3, x3 = 4. So the formula returns true and user gets this integer values which satisfies the formula.Is it possible to make it in sat4j because i work in eclipse with java.

Solution

  • Not sure if SAT4J does SMT solving... You should look for SMT solvers that support linear arithmetic (your case seems only difference logic would also do). You can check : Z3 (SMT solver from Microsoft), CVC4 and Yices. More extensive list is here : https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

    Hope this helps...