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.

Please report problems and feature request using OW2 Gitlab Trackers If you need help, you can contact us preferably 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:

• SAT04 (desc, results), SAT05 (desc, results), SAT Race 06 (desc, results), SAT07 (results), SAT Race 08 (desc, results), SAT09 (results), SAT Race 2010 (results), SAT11(results)
• PB05 (desc, results), PB06 (desc, results), PB07 (results)
• MAXSAT 06 (results), MAXSAT 07 (results), MAXSAT 08 (results)
• CSP 05 (desc, results), CSP 06 (desc,results)

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

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

• Current release! Release 2.3.4
• Release 2.3.3
• Release 2.3.2
• Release 2.3.1
• Release 2.2
• Release 2.1
• Release 2.0

Browse the API documentation.

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

• Unit and regression test (Junit) report
• Design analysis (Jdepend) report
• Design analysis (Classycle) report
• Code convention analysis (Checkstyle) report
• Similarity analysis (Simian) report
• Another static code analysis (Pmd) report

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:

• Unit and regression test (Junit) report
• Code coverage (Clover) report
• Design analysis (Jdepend) report
• Design analysis (Classycle) report
• Code convention analysis (Checkstyle) report
• Similarity analysis (Simian) report
• Bug reports (FindBugs) report

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

To obtain the list of available solvers:

java -jar sat4j-1.5.jar

Browse the javadoc

Browse the various reports about the release:

• Unit and regression test (Junit) report
• Code coverage (Clover) report
• Design analysis (Jdepend) report
• Design analysis (Classycle) report
• Code convention analysis (Checkstyle) report
• Similarity analysis (Simian) report
• Bug reports (FindBugs) report