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

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

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

java -jar org.sat4j.core.jar cnffile

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

java -jar sat4j-csp.jar CSP:cspfile

java -jar sat4j-csp.jar CSP2:cspfile

java -jar sat4j-csp.jar CSP3:cspfile

java -jar sat4j-csp.jar cspfile.xml

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

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

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

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!");      
        }
    }
}

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

        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!");
        }

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.