• Thèse soutenue le :
  • 5 déc. 2008 • Amphi SRC (IUT)

Résumé

Cette thèse traite de deux problèmes combinatoires difficiles : la satisfiabilité propositionnelle - SAT (NP-Complet) et la résolution de formules booléennes quantifiées - QBF (PSPACE Complet). Dans le cas SAT, nous présentons tout d’abord deux extensions efficaces du schéma classique d’analyse des conflits, communément appelé CDCL “Conflict Driven Clause Learning”. En intégrant de nouveaux arcs (ou implications) au graphe d’implication classique, cette première extension permet d’améliorer la hauteur des sauts lors du retour arrière. La seconde extension permet de déduire de nouvelles raisons pour les littéraux impliqués et permettre ainsi un réarrangement de l’interprétation partielle courante. Ensuite un nouveau solveur parallèle ManySAT est décrit. ManySAT utilise un portfolio complémentaire d’algorithmes séquentiels conçus grâce à une minutieuse variation dans les principales stratégies de résolution. Ces stratégies sont combinées au partage de clauses dans le but d’améliorer les performances globales. Enfin, une nouvelle représentation sous forme de graphe d’une formule CNF est présentée. Elle étend le graphe d’implication utilisé dans le cas du fragment polynomial 2-SAT en associant des valuations (ensembles de littéraux, appelés conditions) aux arcs. La résolution classique est reformulée en utilisant la fermeture transitive du graphe. Trois utilisations concrètes de cette nouvelle représentation sont présentées. La première concerne le calcul d’ensembles 2-SAT strong backdoor. Dans la seconde, nous exploitons cette représentation pour la génération d’instances SAT difficiles. Alors que dans la troisième, nous dérivons une nouvelle technique de prétraitement des formules CNF. Dans le cas QBF, nous présentons deux approches duales pour supprimer les symétries. La première consiste à reformuler les interprétations symétriques en pré-modèles qu’on peut ajouter préalablement à la QBF en plus du SBP (Symetry Breaking Predicates) restreint aux cycles existentiels permettant d’obtenir une formule mixte CNF/DNF. La deuxième approche est une extension du SBP classique de SAT vers QBF. Elle est réalisée grâce à une transformation du préfixe de la formule et à l’ajout (en plus du SBP classique) de nouvelles contraintes appelés QSBP (Quantified Symetry Breaking Predicates).

Mots clés : Satisfiabilité (SAT), Formules Boolénnes Quantifiées (QBF), Symétries, Résolution Parallèle.