SAT4J: Bringing the power of SAT technology to the Java platform
The following projects are powered by SAT4J. Send an email to contact at sat4j dot org to see your own project here.
If you are a newcomer to the SATisfiability problem, you might want to take a look at wikipedia's page on the boolean satisfiability problem first. You might also find those surveys of interest. For a deeper insight of the current interest on SAT solvers for software and hardware verification, Armin Biere's course on formal systems is a good start. Eugene Goldberg has also a nice and somehow non standard way of introducing modern SAT solvers in his three part course on SAT.
A new release of SAT4J is now available. It will ship with Eclipse 3.5 (Galileo). The 2.1 release facilitates the integration of SAT technology in Java software, and improves the optimization engines (PB, MAXSAT).
March 24, 2009: Millions of SAT4J users worldwide?SAT4J ships in Eclipse 3.4. Here are some public numbers regarding the number of downloads of Eclipse distributions on Eclipse.org web site since June 2008. Note that those numbers do not include third party products such as IBM or Genuitec ones based on Eclipse.
Eclipse 3.5 M6 ships with SAT4J 2.1 RC2, containing an explanation engine for inconsistency based on QuickXplain.
June 25, 2008: Eclipse 3.4/Ganymede available! ships with SAT4JEclipse 3.4 is finally available. It ships with release 2.0.0 of SAT4J core and SAT4J pb. Those packages are available from ow2 forge download area.
SAT4J 2.0 drives Eclipse new update manager (Equinox P2)Pascal Rapicault from IBM just announced that SAT4J started shipping in Eclipse SDK builds on March 10, 2008.
March 2008: license changesStarting from SAT4J 2.0 RC5, the source code of SAT4J is now being distributed under both the EPL and the GNU LGPL licenses.
August 30, 2007: SAT4J 1.7 released! We are proud to announce the availability of SAT4J 1.7. The default SAT solver now uses Rapid Restart strategy as in Picosat, lightweight caching scheme as in RSAT, two SAT competition 2007 award winning solvers. More details are available on: What's new in release 1.7.
December 2006: Presentation of SAT4J to the Constraints and proofs group at Polytech'Nice-Sophia.
October 2006: French Science Fest 2006 Sudoku as Satisfiability demo information (in French).
The aim of the SAT4J library is to provide an efficient library of SAT solvers in Java. Compared to the OpenSAT project, the SAT4J library targets first users of SAT "black boxes", willing to embed SAT technologies into their application without worrying about the details. Since we use the library for our own research, it is also possible for SAT researchers to use it as a basis for their work.
SAT4J includes our implementation in Java of Niklas Een and Niklas Sorenson's MiniSAT specification: An extensible SAT solver. Niklas Eén and Niklas Sörensson. Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing, LNCS 2919, pp 502-518, 2003
The original C++ implementation is available here.
Whereas the overall algorithmic of the solver is respected, the design has been adapted to Java practices. Furthermore, the initial design has been extended to allow testing several heuristics and learning schemes.
Some data structures included in SAT4J were proposed by Lawrence Ryan: Efficient Algorithms for Clause Learning SAT Solvers, Lawrence Ryan, Master Thesis, SFU, Feb 2004.
