Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

A New Prenexing Strategy for Quantified Boolean Formulae with Bi-Implications

Abstract :

Most of the recent and effcient decision pro cedures for quan-tified Bo olean formulae accept formulae in negation normal form as input or in an even more restrictive format such conjunctive normal form. But real problems are rarely expressed in such forms. For instance, in specification, intermediate prop ositional symb ols are used to capture lo cal results with always the same pattern. So, in order to use most of the state-of-the-art solvers the original formula has firstly to b e converted in prenex form. A drawback of this preliminary step is to destroy completely the original structures of the formula. Furthermore, during the prenexing pro cess, bi-implications are translated in such a way that there is a du- plication of their sub-formulae including the quantifiers. In general, this pro cess leads to an exp onential growth of the formula. In this work, we fo cus on this very common pattern of intermediate result. We intro duce new logical equivalences allowing us to extract these sub-formulae in a way that can improve the p erformance of the state-of-the-art quantified Boolean solvers

Type de document :
Communication dans un congrès
Liste complète des métadonnées
Contributeur : Okina Univ Angers Connectez-vous pour contacter le contributeur
Soumis le : mardi 21 septembre 2021 - 14:45:28
Dernière modification le : mercredi 20 octobre 2021 - 03:19:09
Archivage à long terme le : : mercredi 22 décembre 2021 - 19:05:13


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-03350660, version 1
  • OKINA : ua4541



Benoit da Mota, Igor Stéphan, Pascal Nicolas. A New Prenexing Strategy for Quantified Boolean Formulae with Bi-Implications. Sixth International Workshop on Constraints in Formal Verification, CFV 2009, 2009, Grenoble, France. ⟨hal-03350660⟩



Consultations de la notice


Téléchargements de fichiers