• 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