Problem solving around SAT
- Author:
- Gilles Audemard
- HDR Defended on :
- Nov 29, 2010 • IUT de Lens, amphi SRC
Abstract
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
Supervisor
- Christophe Lecoutre, Professor, University of Artois
Rapporteurs
- Arnaud Lallouet, Professor, University of Caen
- Frédéric Saubion, Professor, University of Angers
- Thomas Schiex, Research Director, INRA
Reviewers
- Chu Min Li, Professor, University of Picardy
- Lakhdar Saïs, Professor, University of Artois