Sat4j
the boolean satisfaction and optimization library in Java
 
How to build SAT4J from source?

SAT4J source code can be found on OW2 SVN. We provide both an ant and a Maven build file that easily allow any user to build SAT4J from source.

First checkout the source code available on HEAD (development version!)

svn checkout svn://svn.forge.objectweb.org/svnroot/sat4j/maven/trunk
or take the source code of one of the official releases, here 2.0.5 (preferred solution)
svn checkout svn://svn.forge.objectweb.org/svnroot/sat4j/maven/tags/2_0_5

To build the library for Java 1.4 and newer, just type:

ant 

To build a CSP solver just type:

ant csp 

To get the list of available options, just type:

ant -p

Maven user will use the classical

mvn install
to build the library.

How to use SAT4J as a standalone SAT solver?

The SAT solver uses input files using the common CNF Dimacs format.

java -jar org.sat4j.core.jar cnffile
How to use SAT4J as a standalone CSP solver?

CSP capabilities is available since release 1.5 of the library. Note that the input format was textual for release 1.5 (using the First CSP competition table format) and is now XML because of the new XML CSP format 2.0 designed for the Second CSP competition. Note that SAT4J does not contain a real CSP solver: it translates CSP problems given in extension into SAT problems to solve them.

Use ...

java -jar sat4j-csp.jar cspfile.txt
... to solve a CSP problem in textual format using the default encoding.
java -jar sat4j-csp.jar CSP:cspfile
... to solve a CSP problem in textual format using the direct encoding.
java -jar sat4j-csp.jar CSP2:cspfile
... to solve a CSP problem in textual format using the binary support encoding and direct encoding for n-ary clauses.
java -jar sat4j-csp.jar CSP3:cspfile
... to solve a CSP problem in textual format using the generalized support encoding.
java -jar sat4j-csp.jar cspfile.xml
... to solve a CSP problem in XML format using the binary support encoding and direct encoding for n-ary clauses.

How to use SAT4J as a standalone Pseudo Boolean solver?

Pseudo Poolean capabilities is available since release 1.5 of the library. Note that the library is keeping up-to-date its input format with the one of the latest PB Evaluation.

java java -jar sat4j-pb.jar pbfile.opb
How to use SAT4J as a standalone [Partial][Weighted] MAX SAT solver?

MaxSAT capability is available since release 1.6 of the library. Weighted Partial MAX SAT problems are supported since release 1.7 of the library.

MAX SAT problems

java -jar sat4j-maxsat.jar file.cnf

[Partial] Weighted MAX SAT problems (MAX SAT 06 Evaluation format)

java -jar sat4j-maxsat.jar file.wcnf
How to setup the JVM for improved SAT solving?

The best thing to do to improve the efficiency of the library is to increase the amount of memory available to the JVM and to use java hotspot server compiler.

java -server -XmsMAXRAM -XmxMAXRAM -jar org.sat4j.core.jar cnffile
How to embed a SAT solver in my Java software?
public class Example {

    public static void main(String[] args) {
        ISolver solver = SolverFactory.newDefault();
        solver.setTimeout(3600); // 1 hour timeout
        Reader reader = new DimacsReader(solver);
        // CNF filename is given on the command line 
        try {
            IProblem problem = reader.parseInstance(args[0]);
            if (problem.isSatisfiable()) {
                System.out.println("Satisfiable !");
                System.out.println(reader.decode(problem.model()));
            } 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!");      
        }
    }
}
How to feed a SAT solver without using a Reader?
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 {
 ...
}
How to iterate over all 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!");
        }
Which solver is right for me?

To make things easier for the end user, SAT4J provides in org.sat4j.minisat.SolverFactory two convenience methods that provide you a SAT solver depending of your needs:

defaultSolver()
This SAT solver is well suited for huge and difficult SAT benchmarks. It is basically the best solver available in the library.
lightSolver()
This SAT solver is useful for people using a SAT solver for hundreds or thousands small/easy SAT problems within their application.

However, if the above solvers do not meet your expectations, please check the other solvers from the library. None of the solver is better of worse than all the others on all benchmarks.