Skip to Main content Skip to Navigation
Conference papers

Vivification de formules propositionnelles clausales

Résumé : Dans cet article, nous présentons une nouvelle technique de prétraitement d'une formule booléenne mise sous forme normale conjonctive (CNF). A la différence de la plupart des approches actuelles, notre procédure vise à améliorer la capacité de propagation des clauses de la formule tout en produisant un nombre limité de clauses utiles. Plus précisément, un test incomplet de redondance est effectué sur chaque clause d'une formule. Celui-ci est basé sur la propagation unitaire, et peut conduire soit à la production d'une sous-clause ou à la génération d'une nouvelle clause, via les techniques d'apprentissage implémenté dans les solveurs modernes. Cette nouvelle approche est comparée empiriquement au meilleur préprocesseur actuel, en terme de réduction de la formule considérée et d'amélioration pratique de sa résolution par l'un des meilleurs solveurs SAT.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00292663
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Wednesday, July 2, 2008 - 11:57:45 AM
Last modification on : Thursday, September 9, 2021 - 3:10:37 PM
Long-term archiving on: : Friday, May 28, 2010 - 11:04:31 PM

File

pages-277-285-article49.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00292663, version 1

Collections

Citation

Cédric Piette, Youssef Hamadi, Lakhdar Saïs. Vivification de formules propositionnelles clausales. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, LINA - Université de Nantes - Ecole des Mines de Nantes, Jun 2008, Nantes, France. pp.277-285. ⟨inria-00292663⟩

Share

Metrics

Record views

197

Files downloads

269