• PhD defended on :
  • 2007-11-27
  • Salle des thèses

mardi 27 novembre 2007 - 14h30 - Salle des thèses

Résumé

Dans cette thèse, nous abordons la résolution pratique d’instances du
problème de la SATisfiabilité d’une formule booléenne mise sous forme
normale conjonctive (SAT) via deux thèmes principaux :
- l’hybridation des méthodes de résolution pour SAT. La recherche locale
est ici utilisée pour guider des algorithmes de type DPLL afin de
résoudre des instance de SAT;
- l’utilisation de la déduction restreinte à la propagation unitaire
pour produire ou supprimer divers types de clauses dans une formule SAT
un ensemble de prétraitements est proposé et expérimenté. Nous proposons également un ensemble de classes polynomiales utilisant la propagation unitaire comme mécanisme de détection.

Composition du jury

  • Éric Grégoire
  • Lakhdar Saïs
  • Bertrand Mazure
  • Laure Devendeville
  • Frédéric Saubion
  • Belaïd Benhamou