Abstract

This document presents a synthesis of the research work accomplished since my thesis, almost 10 years ago. My research activities are aimed at the practical solution of the NP-complete problem, namely SAT, and problems related to it. The first chapter presents the context of my work, describes the problems problems addressed and defines the terms and notations most commonly used in this thesis. The two following chapters deal mainly with my contributions: the first one develops my work on SAT and the second one on problems related to SAT. On SAT, after a brief state of the art, I describe my work around three themes: the hybridization of solvers, the exploitation of structural properties and simplification techniques. The chapter entitled “Beyond SAT” gathers my contributions on problems such as the search for incoherent kernels in the propositional framework and in the more general framework of constraint networks, solving problems expressed with non-monotonic and and first-order logics, the compilation of knowledge bases, the resolution of quantified boolean formulas. In the last chapter, I state some research perspectives.

Keywords: SAT, Hybridization, Inconsistent kernels, CSP, QBF

Jury

Rapporteurs

  • Christian Bessière (Director of Research at CNRS, LIRMM, UMR 5506)
  • Felip Manyà (Director of Research at IIIA-CSIC, Barcelona)
  • Frédéric Saubion (Professor at the University of Angers)

Reviewers

  • Eric Grégoire (Professor at the University of Artois)
  • Chu Min Li (Professor at the University of Picardy)
  • Pierre Marquis (Professor at the University of Artois)

Supervisor

  • Lakhdar Saïs (Professor at the University of Artois)