• HDR Defended on :
  • Nov 29, 2010 • IUT de Lens, amphi SRC


This document presents the whole of the research work carried out since the end of my thesis. They have a common base: satisfiability of SAT problems. I started to work on this problem, and essentially on the associated algorithmic during my thesis. The dichotomy between the simplicity to formulate a SAT problem and the difficulty to solve it has always fascinated me. I have also worked on some extensions of this problem, allowing a more important expressiveness like the QBF (Quantified Boolean Formulas) problem or the SMT problem (SAT Modulo Theories).

This document is composed of three parts. The first one is a synthesis of the research work. I have separated it in 3 main chapters. The first one summarizes my work around SAT, the second one around QBF and finally the third one around SMT. The second part of this thesis is a resume presenting my various research and teaching activities, but also the list of my publications. Finally, the third part is a selection of my publications covering the various fields discussed in the in the first part.

Jury composition


  • Christophe Lecoutre, Professor, University of Artois


  • Arnaud Lallouet, Professor, University of Caen
  • Frédéric Saubion, Professor, University of Angers
  • Thomas Schiex, Research Director, INRA


  • Chu Min Li, Professor, University of Picardy
  • Lakhdar Saïs, Professor, University of Artois