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.


Authors :
Daniel Le Berre
Anne Parrain
Stéphanie Roussel
Emmanuel Lonca
Romain Wallon

EPL    LGPL    Any category    Perennial software    CSP & SAT Provers   

    • Go to the software webpage

    Source code

    International journals

    2022 Constraints 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 Constraints 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.

    International conferences

    2023 Constraints Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura, SAF: SAT-based Attractor Finder in Asynchronous Automata Networks in 21st International Conference on Computational Methods in Systems Biology (CMSB 2023), 2023.
    2021 Constraints 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 Constraints Daniel Le Berre, Pierre Marquis, Stefan Mengel, Romain Wallon, On Irrelevant Literals in Pseudo-Boolean Constraint Learning in 29th International Joint Conference on Artificial Intelligence (IJCAI'20), International Joint Conferences on Artificial Intelligence Organization, pp. 1148-1154, 2020.
    2020 Constraints 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 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.
    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.
    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, Pascal Rapicault, Dependency management for the Eclipse ecosystem in Open Component Ecosystems International Workshop (IWOCE'09), 2009.
    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.

    National conferences

    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.
    2021 Daniel Le Berre, Romain Wallon, Adaptation des stratégies des solveurs SAT CDCL aux solveurs PB natifs in 16es Journées Francophones de Programmation par Contraintes (JFPC'21), 2021.
    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.

    International workshops

    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.
    2020 Romain Wallon, On Adapting CDCL Strategies for PB Solvers in 11th International Workshop on Pragmatics of SAT (POS'20), 2020.
    2019 Daniel Le Berre, Pierre Marquis, Stefan Mengel, Romain Wallon, On Irrelevant Literals in Pseudo-Boolean Constraint Learning in 10th International Workshop on Pragmatics of SAT (POS'19), 2019.