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.



EPL    LGPL    Any category    Perennial software    CSP & SAT Provers   


  • 2022 Xhevahire Tërnava, Johann Mortara, Philippe Collet, Daniel Le Berre, Identification and visualization of variability implementations in object-oriented variability-rich systems: a symmetry-based approach in Automated Software Engineering, pp. 1-52, 2022.
    2018 Daniel Le Berre, Pascal Rapicault, Boolean-Based Dependency Management for the Eclipse Ecosystem in International Journal on Artificial Intelligence Tools, vol. 27, n° 01, pp. 1840003, 2018.
    2014 Daniel Le Berre, Stéphanie Roussel, Sat4j 2.3.2: on the fly solver configuration, System Description in Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 8, pp. 197-202, 2014.
    2010 Daniel Le Berre, Anne Parrain, The SAT4J library, Release 2.2, System Description in Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, pp. 59-64, 2010.
    2022 Thibault Falque, Romain Wallon, On PB Encodings for Constraint Problems in Doctoral Program of the 28th International Conference on Principles and Practice of Constraint Programming (DPCP'22), 2022.
    2021 Daniel Le Berre, Romain Wallon, On Dedicated CDCL Strategies for PB Solvers in 24th International Conference on Theory and Applications of Satisfiability Testing (SAT'21), pp. 315-331, 2021.
    2020 Daniel Le Berre, Pierre Marquis, Romain Wallon, On Weakening Strategies for PB Solvers in 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT'20), pp. 322-331, 2020.
    2014 Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey, Detecting Cardinality Constraints in CNF in 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), Springer, pp. 285-301, 2014.
    2014 Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara, Naoyuki Tamura, Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem in 14th European Conference on Logics in Artificial Intelligence (JELIA'14), Springer, pp. 684-693, 2014.
    2013 David Deharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure, Computing prime implicants in 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD'13), IEEE Press, pp. 46-52, 2013.
    2013 Daniel Le Berre, Pierre Marquis, Stéphanie Roussel, Planning Personalised Museum Visits in 23rd International Conference on Automated Planning and Scheduling (ICAPS'13), AAAI Press, pp. 380-388, 2013.
    2010 Daniel Le Berre, Pascal Rapicault, Dependency Management for the Eclipse Ecosystem: An Update in 3rd International Workshop on Logic and Search {LaSh'10), 2010.
    2009 Daniel Le Berre, Pierre Marquis, Meltem Öztürk, Aggregating Interval Orders by Propositional Optimization in 1st International Conference on Algorithmic Decision Theory (ADT'09), Springer, vol. 5783, pp. 249-260, 2009.
    2009 Daniel Le Berre, Pascal Rapicault, Dependency management for the Eclipse ecosystem in Open Component Ecosystems International Workshop (IWOCE'09), 2009.
    2022 Thibault Falque, Romain Wallon, Des encodages PB pour la résolution de problèmes CSP in 17es Journées Francophones de Programmation par Contraintes (JFPC’22), 2022.
    2019 Daniel Le Berre, Pierre Marquis, Stefan Mengel, Romain Wallon, De la pertinence des littéraux dans les contraintes pseudo-booléennes apprises in 15es Journées Francophones de Programmation par Contraintes (JFPC’19), pp. 43-52, 2019.
    2014 Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey, Détection de contraintes de cardinalité dans les CNF in 10èmes Journées Francophones de Programmation par Contraintes (JFPC'14), pp. 253-262, 2014.
    2013 Daniel Le Berre, Emmanuel Lonca, Réutiliser ou adapter les prouveurs SAT pour l'optimisation booléenne in 9ièmes Journées Francophones de Programmation par Contraintes (JFPC'13), pp. 185-194, 2013.