2010-01-29 • Salle des Thèses UFR des Sciences Lens

Résumé

Ce mémoire présente une synthèse des travaux de recherche que j’ai accomplis depuis ma thèse, il y a maintenant près de 10 ans.Mes activités de recherche ont pour objet la résolution pratique du problème NP-complet de référence, à savoir SAT, et de problèmes liés à celui-ci. Le premier chapitre présente le contexte de mes travaux, décrit les problèmes abordés et définit les termes et les notations les plus utilisés dans ce mémoire. Les deux chapitres suivants traitent principalement de mes contributions : le premier développe mes travaux sur SAT et le second mes travaux sur des problèmes connexes à SAT. Sur SAT, après un bref état de l’art, je décris mes travaux autour de trois thèmes : l’hybridation de solveurs, l’exploitation de propriétés structurelles et les techniques de simplification. Le chapitre intitulé « Au-delà de SAT » regroupe mes contributions sur des problèmes tels que la recherche de noyaux incohérents dans le cadre propositionnel et dans le cadre plus général de réseaux de contraintes, la résolution de problèmes exprimés à l’aide de logiques non monotones et du premier ordre, la compilation de bases de connaissances, la résolution des formules booléennes quantifiées. Dans le dernier chapitre, j’énonce quelques perspectives de recherche.

Mots-clés: SAT, Hybridation, Noyaux incohérents, CSP, QBF

Composition du jury

Rapporteurs

  • Christian Bessière (Directeur de Recherche au CNRS, LIRMM, UMR 5506)
  • Felip Manyà (Directeur de Recherche au IIIA-CSIC, Barcelone)
  • Frédéric Saubion (Professeur à l’Université d’Angers)

Examinateurs

  • Eric Grégoire (Professeur à l’Université d’Artois)
  • Chu Min Li (Professeur à l’Université de Picardie)
  • Pierre Marquis (Professeur à l’Université d’Artois)

Directeur

  • Lakhdar Saïs (Professeur à l’Université d’Artois)