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.

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:

• SAT
• Pseudo-Boolean
• MAXSAT