• HDR soutenu le :
  • 29 nov. 2010 • IUT de Lens, amphi SRC.

Résumé

Ce document présente l’ensemble des travaux de recherche réalisé depuis la fin de ma thèse. Ils ont un socle commun, le problème SAT (pour satisfaisabilité). J’ai commencé à travailler sur ce problème, et essentiellement sur l’algorithmique associée, lors de ma thèse. La dichotomie entre la simplicité à le formuler et la difficulté à le résoudre m’a toujours fasciné. J’ai également travaillé sur quelques extensions de ce problème, autorisant une expressivité plus importante comme le problème QBF (Formules Booléennes Quantifiées) ou le problème SMT (SAT Modulo Théories).

Ce document se compose de trois parties. La première d’entre elle est un synthèse des travaux de recherche. Je l’ai séparé en 3 principaux chapitres. Le premier résume mes travaux autour de SAT, le second autour de QBF et enfin le troisième autour de SMT. La seconde partie de ce mémoire est un curriculum vitae présentant mes diverses activités de recherche, d’enseignement, mais également la liste de mes publications. Enfin, la troisième partie est une sélection de mes publications couvrant les divers domaines abordés dans la première partie.

Composition du jury

Directeur

  • Christophe Lecoutre, Professeur, Université d’Artois

Rapporteurs

  • Arnaud Lallouet, Professeur, Université de Caen
  • Frédéric Saubion, Professeur, Université d’Angers
  • Thomas Schiex, Directeur de Recherche, INRA

Examinateurs

  • Chu Min Li, Professeur, Université de Picardie
  • Lakhdar Saïs, Professeur, Université d’Artois