ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique

APPEL À
CONTRIBUTION
Masses de données hétérogènes
En savoir plus >>
Autres revues >>

Revue d'Intelligence Artificielle

0992-499X
Revue des Sciences et Technologies de l'Information
 

 ARTICLE VOL 25/6 - 2011  - pp.717-742  - doi:10.3166/ria.25.717-742
TITRE
Équivalences et forme prénexe pour les formules booléennes quantifiées

TITLE
Equivalences and prenex form for quantified Boolean formulas

RÉSUMÉ
De nombreux problèmes d’intelligence artificielle et de vérification formelle se ramènent à un test de validité d’une formule booléenne quantifiée (QBF). Pour effectuer ce test, les solveurs QBF actuels ont besoin d’une formule sous une forme syntaxique restrictive prénexe, comme la forme normale conjonctive ou la forme normale de négation. La mise sous cette forme prénexe préalable peut mener à une explosion de la taille de la formule en présence de bi-implications et de ou exclusifs. Dans ce travail, nous décrivons une nouvelle méthode de mise sous forme prénexe à l’aide d’un motif particulier. Nos résultats expérimentaux montrent l’intérêt d’une telle approche pour les solveurs QBF actuels.


ABSTRACT
Many problems in artificial intelligence and in formal verification can be reduced to a validity test of a quantified boolean formula (QBF). To perform this test, existing QBF solvers need the formula to be in a restrictive prenex form, as conjunctive normal form or negation normal form. This prior prenexing process can lead to an exponential growth of the formula in presence of bi-implications and exclusive disjunctions. In this work, we describe a new method of prenexing with a particular pattern. Our experimental results show the interest of such a method with actual QBF solvers.


AUTEUR(S)
Benoît DA MOTA

MOTS-CLÉS
formules booléennes quantifiées, forme prénexe, fusion de quantificateurs.

KEYWORDS
quantified boolean formulae, prenex form, fusion of quantifiers.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (304 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier