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:

• 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.

Browse the Maven generated site.

Browse the Maven generated site.

Browse the Maven generated site.

Browse the Maven generated site.

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

• java -jar sat4j-1.6.jar cnffile

  solves cnffile using the default solver.

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

  solves cnffile using MiniLearning SAT solver.

  java -jar sat4j-1.6.jar

  for usage.
• 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

• java -jar sat4j-1.5.jar cnffile

  solves cnffile using the default solver.

  java -jar sat4j-1.5.jar MiniLearning cnffile

  solves cnffile using MiniLearning SAT solver.

  java -jar sat4j-1.5.jar

  provides the list of available solvers.
• 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