Using Sat4j as a Java library

Embedding a SAT solver in Java code

public class Example {

    public static void main(String[] args) {
ISolver solver = SolverFactory.newDefault();
        solver.setTimeout(3600); // 1 hour timeout
        Reader reader = new DimacsReader(solver);
        PrintWriter out = new PrintWriter(System.out,true);
        // CNF filename is given on the command line 
        try {
            IProblem problem = reader.parseInstance(args[0]);
            if (problem.isSatisfiable()) {
                System.out.println("Satisfiable !");
                reader.decode(problem.model(),out);
            } else {
                System.out.println("Unsatisfiable !");
            }
        } catch (FileNotFoundException e) {
            // TODO Auto-generated catch block
        } catch (ParseFormatException e) {
            // TODO Auto-generated catch block
        } catch (IOException e) {
            // TODO Auto-generated catch block
        } catch (ContradictionException e) {
            System.out.println("Unsatisfiable (trivial)!");
        } catch (TimeoutException e) {
            System.out.println("Timeout, sorry!");      
        }
    }
}

Feeding a SAT solver without aReader

final int MAXVAR = 1000000;
final int NBCLAUSES = 500000;

ISolver solver = SolverFactory.newDefault();

// prepare the solver to accept MAXVAR variables. MANDATORY for MAXSAT solving
solver.newVar(MAXVAR);
solver.setExpectedNumberOfClauses(NBCLAUSES);
// Feed the solver using Dimacs format, using arrays of int
// (best option to avoid dependencies on SAT4J IVecInt)
for (int i=0;<NBCLAUSES;i++) {
  int [] clause = // get the clause from somewhere
  // the clause should not contain a 0, only integer (positive or negative)
  // with absolute values less or equal to MAXVAR
  // e.g. int [] clause = {1, -3, 7}; is fine
  // while int [] clause = {1, -3, 7, 0}; is not fine 
  solver.addClause(new VecInt(clause)); // adapt Array to IVecInt
}

// we are done. Working now on the IProblem interface
IProblem problem = solver;
if (problem.isSatisfiable()) {
   ....
} else {
 ...
}

Iterating over all the models

        ISolver solver = SolverFactory.newDefault();
        ModelIterator mi = new ModelIterator(solver);
        solver.setTimeout(3600); // 1 hour timeout
        Reader reader = new InstanceReader(mi);

        // filename is given on the command line
        try {
            boolean unsat = true;
            IProblem problem = reader.parseInstance(args[0]);
            while (problem.isSatisfiable()) {
               unsat = false;
               int [] model = problem.model();
                // do something with each model
            }
            if (unsat)
                // do something for unsat case
        } catch (FileNotFoundException e) {
            e.printStackTrace();
        } catch (ParseFormatException e) {
            e.printStackTrace();
        } catch (IOException e) {
            e.printStackTrace();
        } catch (ContradictionException e) {
            System.out.println("Unsatisfiable (trivial)!");
        } catch (TimeoutException e) {
            System.out.println("Timeout, sorry!");
        }