1

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.

Aysim Toker
  • 23
  • 5

1 Answers1

2

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

fturkmen
  • 324
  • 3
  • 11
  • sat4j has a module that handles constraint satisfaction problems, which would cover this, but it does so by reducing the CSP to a SAT instance. Using an SMT solver is a better approach for anything but toy problems, because mashing a CSP down to SAT throws away too much structural information that a smart solver can use to guide the search. – Kyle Jones Nov 18 '15 at 18:59