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 26/1-2 - 2012  - pp.103-125  - doi:10.3166/ria.26.103-125
TITRE
Symétries et QBF

TITLE
Symmetries and QBFs

RÉSUMÉ
Dans ce papier, nous décrivons un nouveau cadre pour l’élimination des symétries dans les formules booléennes quantifiées (QBF). Notre cadre est basé sur une approche classique par ajout de contraintes, appelées Symmetry breaking predicates (SBP), largement utilisée pour éliminer les symétries dans les formules booléennes (SAT) et dans les réseaux de contraintes (CSP). Un des obstacles à l’extension de cette approche au cadre QBF réside dans la présence de variables quantifiées universellement. Ajouter de manière conjonctive le SBP à la formule booléenne quantifiée peut conduire à rendre la formule non valide. Dans ce travail, une nouvelle approche pour éliminer les symétries dans les QBF est proposée. Cette approche basée sur les modèles combine à la fois l’ajout de contraintes et de modèles prédéfinis contrairement aux approches classiques d’élimination de symétries. Une transformation de la formule obtenue sous forme clausale est présentée. Les résultats expérimentaux obtenus par les différents solveurs QBF état de l’art montrent l’efficacité de notre approche d’élimination des symétries.


ABSTRACT
In this paper, we describe a new framework for breaking symmetries in quantified boolean formula (QBF). It is based on the classical symmetry breaking predicates (SBP) usually used in both constraint satisfaction and satisfiability problems. One of the main challenge behind the extension of the classical SBP to QBF rise in the presence of universally quantified variables. Adding conjunctively the SBP to QBF might lead to a non valid QBF formula. In this work, a new symmetry breaking approach for QBF is proposed. Contrary to classical symmetry breaking, our model-based approach combines both the addition of new constraints with predefined models. A linear transformation of the obtained formula to prenex clausal form is presented. Experimental evaluation performed on state-of-the-art solvers shows the efficiency of our symmetry breaking approach.


AUTEUR(S)
Saïd JABBOUR, Lakhdar SAÏS

MOTS-CLÉS
symétries, formules booléennes quantifiées.

KEYWORDS
symmetries, quantified boolean formulas.

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  (186 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier