SAT4J is a library of boolean reasoners for the Java platform. The library has been designed to be easy to use and targets SAT instances coming from real problems translated into SAT. The library supports also pseudo boolean constraints, and provides solutions for various decision and optimization problems by translation into SAT of Pseudo-Boolean problems (MAXSAT, CSP).

SAT4J is already used in several projects:

Sudoku lovers can check Ivor Spence’s web page on Sudoku as Satisfiability which is based on SAT4J.

Since June 2008, SAT4J is managing plugin dependencies of Eclipse based applications.

As a consequence, SAT4J is now being distributed with Linux distributions (it started in October 2009 with Mandriva 2009).

Finally, SAT4J is also used in two software in bioinformatics: GNA.sim by Genostar, and SATlotyper by the Max Planck Institute.

Sat4j has been highlighted by CNRS in 2018 by being the subject of an innovation medal.

Sat4j is developed openly as OW2’s project.