SAT4J: Bringing the power of SAT technology to the Java platform
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/trunkor 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 installto build the library.
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... 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.
java java -jar org.sat4j.pb.jar pbfile.opb
java -jar sat4j-maxsat.jar file.cnf
java -jar sat4j-maxsat.jar file.wcnf
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);
// 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!");
}
}
}
final int MAXVAR = 1000000;
final int NBCLAUSES = 500000;
ISolver solver = SolverFactory.newDefault();
// prepare the solver to accept MAXVAR variables. MANDATORY
solver.newVar(MAXVAR);
// not mandatory for SAT solving. MANDATORY for MAXSAT solving
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!");
}
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.
