Utilisation de techniques polynomiales pour la résolution pratique
- PhD Student:
- Olivier Fourdrinoy
- Co-Advisors :
- Éric Grégoire
- Lakhdar Saïs
- Co-Supervisor :
- Bertrand Mazure
- 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