• PhD Student:
  • Florian Letombe
  • PhD defended on :
  • Dec 5, 2005

Doctorant : Florian Letombe

Date de soutenance :Mardi 13 Décembre 2005**

Résumé

Cette thèse est centrée sur le problème QBF de décision de la validité des formules booléennes quantifiées : étant donnée une formule de la forme S = A a1 E e2 … A aN E eN . P où P est une formule propositionnelle construite sur e1, a1, …, eN, aN (la matrice de S), il s’agit de déterminer si pour toute affectation d’une valeur de vérité à a1 dans P, il existe une affectation d’une valeur de vérité à e1 dans P, …, pour toute affectation d’une valeur de vérité à aN dans P, il existe une affectation d’une valeur de vérité à eN dans P qui rend P valide. Le problème QBF est calculatoirement difficile (PSPACE-complet). Il importe donc de mettre en évidence des cas particuliers où sa résolution pratique est envisageable. Dans cette thèse, nous avons considéré des restrictions de QBF portant sur la matrice des instances. Notre objectif principal était double : (1) identifier la complexité de QBF pour des restrictions non considérées jusqu’ici et (2) explorer dans quelle mesure les classes polynomiales pour QBF peuvent être exploitées au sein d’un prouveur QBF général afin d’améliorer son efficacité.

Concernant le premier point, nous avons montré que QBF restreint aux fragments cibles pour la compilation de “connaissances” étudiés dans [Darwiche 2002], qui sont traitables pour SAT, reste PSPACE-complet et donc intraitable en pratique. Nous avons également mis en évidence le lien étroit qui existe entre notre étude et le problème de compilabilité de QBF.

Concernant le second point, nous avons décrit une nouvelle heuristique de branchement Delta visant à promouvoir la génération de formules Horn renommables quantifiées durant le parcours de l’arbre de recherche effectué par une procédure de type Q-DPLL pour QBF. Les résultats expérimentaux présentés montrent qu’en pratique, hormis notre prouveur Qbfl, les prouveurs QBF actuels ne sont pas capables de résoudre facilement les instances Horn quantifiées ou Horn renommables quantifiées ; ceci suffit à justifier l’intérêt de l’approche suivie. Les résultats obtenus montrent également que, muni de l’heuristique Delta, Qbfl améliore significativement ses performances sur certains types d’instances, même s’il obtient des résultats moyens en général, comparé aux autres prouveurs QBF actuels.

Mots clé : formules booléennes quantifiées, logique propositionnelle, compilation de “connaissances”, restrictions traitables, complexité, heuristiques de branchement.

[Darwiche 2002] : DARWICHE A. & MARQUIS P. (2002). “A Knowledge Compilation Map”. Journal of Artificial Intelligence Research, 17, p. 229-264.