Sat4j
the boolean satisfaction and optimization library in Java
 
Sat4j on social or software networks
Developer's corner

Sat4j is an open source projet. As such, we welcome your feedback:

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 is a full featured boolean reasoning library designed to bring state-of-the-art SAT technologies to the Java Virtual Machine.

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

April 2013: Sat4j 2.3.4 released

Sat4j 2.3.4 fixes an important issue in the OptToPBSATAdapter class. All users of the optimization part of the library are strongly encouraged to update to that new release.

The users of the core SAT engine can now produce UNSAT proofs using the RUP format used in the SAT competition 2013

Sat4j 2.3.4 will ship with the upcoming release of Eclipse, 4.3 Kepler.

February 2013: Sat4j 2.3.3 released

Sat4j 2.3.3 fixes several issues with the previous release. The default SAT solver now uses Glucose 2.1 like dynamic restart policy and agressive learned clauses deletion management. It provides the ability to read problems using JSON. See the full changelog for details.

Note that the artifacts are now provided by the nexus instance managed by ow2. As such, the maven group and artifact ids of sat4j start now by org.ow2.sat4j instead of simply org.sat4j.

July 2012: Sat4j 2.3.2 released. visualize and control your search!

Sat4j 2.3.2 includes a new feature quite useful for people willing to understand what's going on inside the solvers: a dashboard that let you visualize various metrics live, and to change various parameters during the search. See our PoS'12 presentation for details.

November 2011: Sat4j is now an official Artois University/CNRS software

Artois University CNRS

After seven years of incubation in our lab, Sat4j is now an official Artois University and CNRS software. The software has been registered to the APP. This website, the documentation and the source code are progressively being updated to refer to those copyright owners. Sat4j will continue to be distributed under the same dual license (EPL and GNU LGPL). However, it is now possible to provide Sat4j under a specific license on demand. Contact us for details.

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.

Older news

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