Ampithéatre CTL
25 juin 2009 - 14h00
Sur Quelques Problèmes de la Satisfiabilité (Phd Defense)
par Scott Cotton de Verimag
Résumé : Un nombre croissant d'applications, telles que la vérification et l'optimisation non-linéaire, fait usage des solveurs SAT et SMT. Malgré des progrès récents dans le développement de techniques de SAT et SMT, les problèmes pour lesquels les solveurs SAT and SMT sont utilisés sont souvent difficiles et intractables, et la performance de ces solveurs est difficile à estimer. En consequence, le développement de méthodes de SAT et de SMT efficaces est un domaine de recherche actif. Dans ce séminaire, nous présentons des techniques de calcul liées aux solveurs SAT et SMT. La présentation contient quatre parties.
Tout d'abord, nous donnons une introduction de la satisfiabilité propositionelle, y compris DPLL et DPLL(T).
Deuxièmement, nous introduisons le concept de résolution basée sur une composition d'étiquettes, une variante de DPLL(T). Dans cette partie, nous examinons la composition d'un solveur de la logique de différences (DL) avec un solveur SAT. Nous décrivons ensuite un solveur efficace DL sur la base d'une un algorithm de plus courts chemins. Nous présentons également des résultats expérimentaux montrant l'efficacité des solveurs composés, et en plus, l'utilisation de ce solveur de DL efficace a permis une amélioration par rapport aux résultats antérieurs.
Troisièmement, nous considérons le problème de DPLL plus profondément. Nous présentons une stratégie de redémarrage, qui cherche en utilisant de différents heuristiques des états plus proches de la terminaison.
Quatrièmement, nous présentons une méthode directe et générale pour résoudre des problèmes conjunctifs. Cette méthode est fondée sur la recherche en profondeur dans l'ensemble des valuations des variables. Cette méthode utilise une condition de cohérence locale que nous appelons conhérence unate. Nous examinons les similarités et les différences entre cette méthode et DPLL, avec un accent sur le cas de domaines de variables infinis. Nous concluons avec des expérimentations préliminaires avec une implantation de prototype en Java.
Jury composé de
Yassine Lakhnech Président (Proposé)
Nikolaj Bjørner Rapporteur
Sharad Malik Rapporteur
Kenneth McMillan Rapporteur
Armin Biere Examinateur
Eugene Asarin Examinateur
Andreas Podelski Examinateur
Oded Maler Directeur de Thèse
