SAT4J as a standalone solver

SAT4J can be used as as standalone tool for solving SAT, CSP and pseudo-boolean problems. MAX-SAT problems can be treated as well.

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

If you want to improve the efficiency of the library, the best thing to do is to increase the amount of memory available to the JVM.

java -XmsMAXRAM -XmxMAXRAM -jar org.sat4j.core.jar cnffile

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, which can be found at http://www.cril.univ-artois.fr/PB16/.

To use SAT4J with a pseudo-boolean solver, use

java java -jar sat4j-pb.jar pbfile.opb

SAT4J as a standalone MAXSAT solver

MaxSAT capability is available since release 1.6 of the library. For these problems, use

java java -jar sat4j-maxsat.jar file.cnf

Weighted Partial MAX SAT problems are supported since release 1.7 of the library. For these problems, use the MAXSAT’06 evaluation format available at http://www.maxsat07.udl.es/ and use the following syntax:

java java -jar sat4j-maxsat.jar file.wcnf

SAT4J as a standalone CSP solver

CSP capabilities are available since release 1.5 of the library. Note that the input format was textual for release 2.1 and 3.0.

Note that SAT4J does not contain a real CSP solver: it translates CSP problems given in extension into SAT problems to solve them.

To solve a CSP problem in textual format using the default encoding, use

java -jar sat4j-csp.jar cspfile.txt

To solve a CSP problem in textual format using the direct encoding, use

java -jar sat4j-csp.jar CSP:cspfile.txt

To solve a CSP problem in textual format using the binary support encoding and direct encoding for n-ary clauses, use

java -jar sat4j-csp.jar CSP2:cspfile.txt

To solve a CSP problem in textual format using the generalized support encoding, use

java -jar sat4j-csp.jar CSP3:cspfile.txt

To solve a CSP problem in XML format using the binary support encoding and direct encoding for n-ary clauses, use

java -jar sat4j-csp.jar cspfile.xml