Résolution Etendue par Substitution Dynamique des Fonctions Booléennes

Résumé : Ce travail présente une technique originale de substitution dynamique des fonctions booléennes. Il détecte premièrement un ensemble de fonctions booléennes dans la 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éesolution é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 d'encodage CNF en appliquant le principe d'extension Tseitin. Substituer les entrées par les sorties peut être vu comme une façon élégante d'imiter 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 competitions SAT et SAT-Race.
Type de document :
Communication dans un congrès
JFPC, May 2012, Toulouse, France. 2012
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00820039
Contributeur : Said Jabbour <>
Soumis le : vendredi 3 mai 2013 - 11:57:17
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : dimanche 4 août 2013 - 04:03:22

Fichier

jfpc2012SubFonctions.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00820039, version 1

Collections

Citation

Said Jabbour, Jerry Lonlac, Lakhdar Sais. Résolution Etendue par Substitution Dynamique des Fonctions Booléennes. JFPC, May 2012, Toulouse, France. 2012. 〈hal-00820039〉

Partager

Métriques

Consultations de la notice

103

Téléchargements de fichiers

171