Sat4j
the boolean satisfaction and optimization library in Java
 

The architecture of the solver has been recently published in a JSAT system description: Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, Volume 7 (2010), system description, pages 59-64.

A getting started guide is currently under development. Your feedback about it is welcome.

A Wiki-Style documentation is also available from SAT4J @ Objectweb. Please report problems and feature request using OW2 Jira Trackers If you need help, you can contact us preferably on our forums or by sending an email to help at sat4j dot org.

If you are looking for the detailed features available in the library, the description of the solvers submitted to the various competitions and evaluations is a good start:

A poster showing the various dependencies of the SAT4J project can also be of some help.

Latests releases

You can browse the Maven generated site for each of those releases:

Release 1.7

Browse the API documentation.

For those interesting in software engineering, some reports are also available:

A web site generated by Maven 2 is also available.
Release 1.6_01

To solve cnffile using the default solver:

java -jar sat4j-1.6.jar cnffile

To solve cnffile using the MiniLearning SAT solver:

java -jar sat4j-1.6.jar -s MiniLearning cnffile

For usage:

java -jar sat4j-1.6.jar

Browse the javadoc

Browse the various reports about the release:

Release 1.5.0_01

To solve cnffile using the default solver:

java -jar sat4j-1.5.jar cnffile

To solve cnffile using the MiniLearning SAT solver:

java -jar sat4j-1.5.jar MiniLearning cnffile
solves cnffile using MiniLearning SAT solver.

To obtain the list of available solvers:

java -jar sat4j-1.5.jar

Browse the javadoc

Browse the various reports about the release: