SAT4J est une bibliothèque de prouveurs SAT 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. SAT4J va intégrer la prochaine version du framework Maven pour effectuer la même tâche.

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.

Aller sur la page web du logiciel