Satisfiabilité propositionnelle et raisonnement par contraintes : modèles et algorithmes
- Doctorant:
- Jean-Marie Lagniez
- Directeur de thèse :
- Lakhdar Saïs
- Co-encadrants de thèse :
- Gilles Audemard
- Bertrand Mazure
- Financement : Artois
- Thèse soutenue le :
- 7 déc. 2011 • salle des thèses
Résumé
La thèse porte sur la résolution des problèmes de satisfiabilité propositionnelle (SAT) et des problèmes de satisfaction de contraintes (CSP). Ces deux modèles déclaratifs sont largement utilisés pour résoudre des problèmes combinatoires de première importance comme la vérification formelle de matériels et de logiciels, la bioinformatique, la cryptographie, la planification et l’ordonnancement de tâches. Plusieurs contributions sont apportées dans cette thèse. Elles vont de la proposition de schémas d’hybridation des méthodes complètes et incomplètes, répondant ainsi à un challenge ouvert depuis 1998, à la résolution parallèle sur architecture multi-coeurs, en passant par l’amélioration des stratégies de résolution. Cette dernière contribution a été primée à la dernière conférence internationale du domaine (prix du meilleur papier). Ce travail de thèse a donné lieu à plusieurs outils (open sources) de résolution des problèmes SAT et CSP, compétitifs au niveau international.
Mots-clés : SAT, CSP, hybridation, résolution parallèle