Skip to Main content Skip to Navigation
Conference papers

Une approche symbolique pour les formules booléennes quantifiées

Résumé : Depuis quelques années, la résolution des formules booléennes quantifiées (QBF) est devenu un domaine de recherche important et attractif. En effet, de nombreuses classes de problèmes peuvent être formulées efficacement en des instances QBF (planification, raisonnement non monotone, model checking). Beaucoup de solveurs ont été proposé. La majorité d'entre eux explorent un arbre de recherche en utilisant des techniques basés sur la procédure DLL. Or, les quantificateurs des formules QBF imposent un ordre partiel d'affectation des variables. Pour passer outre cette imposition, nous proposons une nouvelle approche symbolique (QBdd(SAT)). Elle utilise de façon originale les diagrammes de décision binaires pour représenter l'ensemble des modèles (ou impliquants premiers) de la formule booléenne en utilisant des algorithmes de recherches pour SAT. Deux extensions améliorent notre approche. Tout d'abord, nous introduisons un opérateur de réduction sur les BDD afin de limiter leur taille et de pouvoir répondre à la question de la validité des formules QBF. Ensuite, grâce à des nogoods générés à partir du BDD, des coupures sont réalisés dans l'arbre de recherche. En utilisant des techniques basées sur DLL (resp. recherche stochastique), notre approche peut facilement donner lieu à un solveur complet QBdd(DLL) (resp. incomplet QBdd(LS)). Les premières expérimentations montrent de bonnes performances de ces deux solveurs sur certaines classes d'instances de l'évaluation QBF03.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000047
Contributor : Christine Solnon <>
Submitted on : Tuesday, May 24, 2005 - 6:36:06 PM
Last modification on : Thursday, January 11, 2018 - 6:19:28 AM
Long-term archiving on: : Thursday, April 1, 2010 - 9:31:16 PM

Files

Identifiers

  • HAL Id : inria-00000047, version 1

Collections

Citation

Gilles Audemard, Lakhdar Saïs. Une approche symbolique pour les formules booléennes quantifiées. Premières Journées Francophones de Programmation par Contraintes, CRIL - CNRS FRE 2499, Jun 2005, Lens, pp.59-68. ⟨inria-00000047⟩

Share

Metrics

Record views

116

Files downloads

164