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.

Aller sur la page web du logiciel