Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-00820039
Contributor : Said Jabbour <>
Submitted on : Friday, May 3, 2013 - 11:57:17 AM
Last modification on : Sunday, March 7, 2021 - 10:52:03 AM
Long-term archiving on: : Sunday, August 4, 2013 - 4:03:22 AM

File

jfpc2012SubFonctions.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00820039⟩

Share

Metrics

Record views

135

Files downloads

289