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 28/6 - 2014  - pp.645-663  - doi:10.3166/ria.28.645-663
TITRE
Résolution étendue par substitution dynamique des fonctions booléennes

TITLE
Extending resolution by dynamic substitution of boolean functions

RÉSUMÉ

Ce papier présente une technique originale de substitution dynamique de fonctions booléennes. Notre technique procède en deux étapes. Dans une phase de prétraitement, nous effectuons une reconnaissance d’un ensemble de fonctions booléennes à partir d’une formule booléenne sous forme normale conjonctive (CNF). Ces fonctions sont ensuite utilisées pour réduire la taille des différentes clauses apprises en substituant les arguments d’entrée par les arguments de sortie. Ceci conduit à une façon originale d’intégrer une forme restreinte de résolution étendue, l’un des plus puissants systèmes de preuve par résolution. En effet, la plupart des fonctions booléennes extraites correspondent à celles introduites au cours de la phase de transformation vers CNF en appliquant le principe d’extension Tseitin. Substituer les entrées par les sorties peut être vu comme une façon élégante de mimer la résolution étendue avec la manipulation des sous-formules. Des expérimentations préliminaires montrent la faisabilité de notre approche sur certaines classes d’instances SAT prises des récentes compétitions SAT et SAT-Race.



ABSTRACT

This paper presents a dynamic substitution technique of Boolean functions. It first recovers a set of Boolean functions from propositional formula in conjunctive normal form (CNF). Then these functions are used to reduce the size of the learnt clauses by substituting the input arguments by the output ones. This leads to an original way to integrate a restricted form of extended resolution, one of the most powerful resolution proof system. Indeed, most of the extracted Boolean functions corresponds to those introduced during the CNF encoding phase by applying the Tseitin extension principle. Substituting the inputs by the outputs can be seen as an elegant way to mimic extended resolution with sub-formulas manipulation. Preliminary experiments show the feasibility of our approach on some classes of SAT instances taken from the recent SAT Race and competitions.



AUTEUR(S)
Saïd JABBOUR, Jerry LONLAC, Lakhdar SAÏS, Clémentin TAYOU DJAMÉGNI

MOTS-CLÉS
SAT, résolution étendue

KEYWORDS
SAT, extended resolution

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



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier