• PhD Student:
  • Olivier Fourdrinoy
  • PhD defended on :
  • Nov 27, 2007 • 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