A New Prenexing Strategy for Quantified Boolean Formulae with Bi-Implications - Université d'Angers Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

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

Résumé

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

Fichier principal
Vignette du fichier
cfv09.pdf (259.22 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03350660 , version 1 (21-09-2021)

Identifiants

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

Citer

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⟩

Collections

UNIV-ANGERS LERIA
5 Consultations
9 Téléchargements

Partager

Gmail Facebook X LinkedIn More