SAT4J: Bringing the power of SAT technology to the Java platform
We provide an ant build file that easily allow any user to build the SAT4J library from CVS. There is no need to have an account on objectweb for that. It uses a simple anonymous (read-only) access to CVS. The build file can be downloaded from SAT4J objectweb forge.
To build the library for Java 5 and newer, just type:
ant -f build-1.5.xml(You need an internet access properly configured on your computer).
To build a CSP solver just type:
ant -f build-1.5.xml csp
To get the list of available options, just type:
ant -f build-1.5.xml -p
Note that you can also rename the file into build.xml. in that case, you can simple use
antto build the library.
java -jar sat4j-1.5.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-1.5.jar cspfile.txt... to solve a CSP problem in textual format using the default encoding.
java -jar sat4j-1.5.jar CSP:cspfile... to solve a CSP problem in textual format using the direct encoding.
java -jar sat4j-1.5.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-1.5.jar CSP3:cspfile... to solve a CSP problem in textual format using the generalized support encoding.
java -jar sat4j-1.6_01.jar cspfile.xml... to solve a CSP problem in XML format using the binary support encoding and direct encoding for n-ary clauses.
java -jar sat4j-1.5.jar MiniOPBMin pbfile.opb
java -jar sat4j-1.5.jar MiniOPBMin OPB:pbfile
java -cp sat4j-1.5.jar org.sat4j.LanceurPseudo2007 pbfile
java -cp sat4j-1.6.jar org.sat4j.MaxSatLauncher file.cnf
java -cp sat4j-1.6.jar org.sat4j.MaxSatLauncher file.wcnf
java -server -XmsMAXRAM -XmxMAXRAM -jar sat4j-1.5.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.
