Sat4j, un moteur libre de raisonnement en logique propositionnelle
- Auteur:
- Daniel Le Berre
- HDR soutenu le :
- 3 déc. 2010 • Salle des thèses, Faculté des Sciences Jean Perrin, Lens.
Résumé
Nos travaux de recherche se situent dans le cadre de la logique propositionnelle. Nous nous intéressons à la modélisation de problèmes dans ce formalisme et à leur résolution pratique. Nous présentons comme fil conducteur du document le problème de la gestion des dépendances entre logiciels. Nous montrons comment divers aspects de ce problème peuvent être modélisés comme des problèmes d’optimisation pseudo-booléens ou de type MaxSat, et indiquons aussi comment la logique du choix qualitatif peut être utilisée comme cadre de représentation de préférences complexes à prendre en compte pour gérer les dépendances. Nous présentons ensuite en détail les fonctionnalités de la bibliothèque libre Sat4j, permettant de résoudre divers problèmes de décision et d’optimisation en logique propositionnelle. Ses performances sont évaluées contre l’état de l’art dans chaque domaine (SAT, pseudo-booléen, MaxSat). Nous présentons enfin les motivations et le fonctionnement des diverses éditions de la compétition internationale de prouveurs SAT que nous avons organisées.
Composition du jury
Rapporteurs
- Armin Biere, Professeur à l’Université Johannes Kepler
- Roberto Di Cosmo, Professeur à l’Université Paris Diderot
- Enrico Giunchiglia, Professeur à l’Université de Gênes
Examinateurs
- Éric Grégoire, Professeur à l’Université d’Artois
- Christophe Lecoutre, Professeur à l’Université d’Artois
- Joao Marques-Silva, Professeur à l’Université de Dublin
- Lakhdar Saïs, Professeur à l’Université d’Artois
Directeur
- Pierre Marquis, Professeur à l’Université d’Artois