Encadrement : Gilles Audemard et Lakhdar Saïs

Centre de Recherche en Informatique de Lens

E-mail : audemard@cril.univ-artois.fr - sais@cril.univ-artois.fr

Web : http://www.cril.univ-artois.fr/ãudemard - http://www.cril.univ-artois.fr/~sais

Les formules booléennes quantifiées (QBF) constituent une extension des formules booléennes classiques (Problème SAT). En effet, une formule QBF est tout simplement une formule booléenne dont les variables sont quantifiées existentiellement ($ ) et universellement (" ).

Cette simple extension joue un rôle théorique et pratique fondamental. En effet, le problème de la validité des formules QBF joue un rôle important en théorie de la complexité. Dans le cas général, i.e. lorsque le nombre d'alternances de quantificateurs n'est pas borné a priori, il constitue le problème PSPACE-complet canonique. D’un point de vu pratique, une quantité importante de problèmes d'IA (mais aussi d'autres domaines) ont une complexité théorique dans ces classes. C'est le cas par exemple pour divers problèmes d'inférence (abduction, révision, mise à jour, circonscription, inférence en logique des défauts, etc.) et de planification non déterministe.

Le développement d’une algorithmique efficace pour résoudre les formules QBFs, reste un problème important si on veut envisager la résolution de ses différentes applications. De nombreux algorithmes ont été proposés, or la plupart ne sont que des extensions de la procédure bien connue de Davis et Putnam. Une différence importante par rapport à sa version propositionnelle réside dans l’utilisation d’un ordre partiel d’affectation fixé par les quantificateurs de la formule. Cette restriction réduit l’ensemble des ordres d’affectation possible, et par conséquent, les possibilités de réduction de l’arbre de recherche. Ceci constitue de notre point de vue un des obstacles à l’adaptation des meilleures heuristiques développées dans le cadre SAT. Récemment, nous avons montré comment il est possible de s’affra! nchir de l’ordre imposé par le préfixe de la QBF, en développant une approche mixte combinant les approches SAT et celles issues des diagrammes binaires de décision [1].

Après une recherche bibliographique sur les formules booléennes quantifiées, l’étude concernera les points ci-dessous (liste non exhaustive) :

• Etendre et améliorer notre approche mixte. En effet, l’approche QBFBDD [1] combine la procédure de Davis Putnam et les ROBDD, il ‘agit de proposer d’autres types d’hybridation en considérant d’autres algorithmes comme par exemple la recherche locale ou encore d’autres types de BDD comme les ZBDD.

• Développer des heuristiques robustes et spécialisé pour les QBFs
• Développer et/ou d’étendre des techniques de simplifications de formules QBFs.

Remarque :

Ce sujet comporte une partie théorique et une autre pratique (développement). Il est donc souhaitable d’avoir des connaissances en programmation (langage C et Java).

Ce sujet peut donner lieu à une poursuite en thèse.

[1] Gilles Audemard et Lakdhar Sais "SAT Based BDD Solver for Quantified Boolean Formulas", The 16th IEEE International Conference on Tools with Artificial Intelligence. A paraître, Novembre 2004.