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.
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...