SAT4J est une bibliothèque de raisonnement booléen (SAT,MAXSAT, Pseudo-Booléen) en Java. Elle est conçue pour être facile à utiliser et performante sur les instances SAT issues de problèmes réels. La bibliothèque offre aussi la gestion des contraintes pseudo booléennes, et décline un grand nombre de problèmes de décision ou d’optimisation en terme de problème SAT ou Pseudo-Booléen (MAXSAT, CSP).

SAT4J est utilisée dans divers projets académiques :

Les personnes intéressées par le sudoku peuvent visiter la page de Ivor Spence sur Sudoku as Satisfiability qui utilise SAT4J.

Depuis juin 2008, SAT4J est utilisé dans la plate-forme Eclipse pour gérer les dépendances entre plugins.

L’une des conséquences de l’adoption de SAT4J par Eclipse est que SAT4J est maintenant disponible dans la plupart des nouvelles distributions Linux (la première à l’intégrer est la Mandriva 2009, sortie le 9 octobre).

Enfin, SAT4J est aussi utilisé dans deux outils de bioinformatique : GNA.sim de la société Genostar, et SATlotyper du Max Planck Institute.

SAT4J a été mis à l’honneur en 2018 par une médaille de l’innovation du CNRS.

Sat4j est développé de manière ouverte comme projet OW2.



EPL    LGPL    Toute catégorie    Logiciels pérennes    Prouveurs CSP & SAT   


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