Sat4j: the boolean satisfaction and optimization library for Java
 
Newcomer in satisfiability testing?

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. We also gave a lecture on SAT for the Verification Technology, Systems and Applications summer school in october 2009.

There are many international competitions organized around those problems, where you can see sat4j in action:

How to cite/refer to Sat4j?

The easiest way to proceed is to add a link to this web site in a credits page if you use Sat4j in your software.

If you are an academic, please use the following reference instead of sat4j web site if you need to cite Sat4j in a paper: 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.

Sat4j on social or software networks
About Sat4j

The Sat4j project started in 2004 as an implementation in Java of Niklas Een and Niklas Sorenson's MiniSAT specification: An extensible SAT solver. Niklas Eén and NiklasSö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 was respected, the design has been adapted to Java practices and the initial design has been extended to allow testing several heuristics and learning schemes.

Over the years, the support for pseudo-boolean optimization (2005), CSP to SAT translation (2005), MaxSat (2006), and MUS (2011) has been added.

Since June 2008, the Eclipse platform relies on Sat4j to solve its software dependencies. As such, Sat4j is probably the most widely deployed and used Sat-based library in the world.

Sat4j is a java library for solving boolean satisfaction and optimization problems. It can solve SAT, MAXSAT, Pseudo-Boolean, Minimally Unsatisfiable Subset (MUS) problems. Being in Java, the promise is not to be the fastest one to solve those problems (a SAT solver in Java is about 3.25 times slower than its counterpart in C++), but to be full featured, robust, user friendly, and to follow Java design guidelines and code conventions (checked using static analysis of the source code). The library is designed for flexibility, by using heavily the decorator and strategy design patterns. Furthermore, Sat4j is open source, under the dual business friendly Eclipse Public License and academic friendly GNU LGPL license.

To get an idea of what can be done using Sat4j, you might want to take a look at Sat4j case studies (draft).

Over the years, Sat4j has been used by numerous research groups, especially in software engineering, and has been included in the curriculum of many constraint programming, AI or software verification classes (see all papers citing Sat4j's system description/see all papers mentioning Sat4j/see all web pages mentioning Sat4j).

October 2011: Sat4j 2.3.1 released

After receiving much feedback from both external and internal users, we are proud to announce the availability of that new release, that fixes several issues, improves the API and provides the possibility to optimize by lower bounding. See the changelog for details.

March 2011: Sat4j 2.3.0 released

The new release mainly cleans up the code of release 2.2 and provides the new Minimally Unsatisfiable Subset solver submitted to the SAT 2011 competition and the possibility for the MAXSAT solver to be used as an incomplete solver for the MAXSAT Evaluation 2011.

October 2010: SAT4J 2.2.2 released

A new release of SAT4J is now available. Release 2.2 corresponds to the version that ships with Eclipse 3.6. Release 2.2.1 contains a fix for solving WBO problems while release 2.2.2 contains a bugfix for solving some MaxSat problems declaring much more variables than the ones really used. It contains the most efficient MaxSat solver we ever shipped in Sat4j.

May 2009: SAT4J 2.1 released

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.

March 13, 2009: Eclipse 3.5 M6 ships with improved explanation support!

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 SAT4J

Eclipse 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 changes

Starting 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).

CRIL OW2 Consortium
Valid XHTML 1.1 Valid CSS!
This is free software under both the Eclipse Public License and the GNU LGPL licence developed at CRIL. The SAT4J project is kindly hosted on the OW2 forge.YourKit is kindly supporting open source projects with its full-featured Java Profiler. YourKit, LLC is the creator of innovative and intelligent tools for profiling Java and .NET applications. Take a look at YourKit's leading software products: YourKit Java Profiler and YourKit ASP.NET Profiler.