Vivification de formules propositionnelles clausales - Archive ouverte HAL Access content directly
Conference Papers Year : 2008

Vivification de formules propositionnelles clausales

(1) , (2) , (1)
1
2
Cédric Piette
Youssef Hamadi
  • Function : Author
  • PersonId : 840368
Lakhdar Saïs

Abstract

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.
Fichier principal
Vignette du fichier
pages-277-285-article49.pdf (293.34 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00292663 , version 1 (02-07-2008)

Identifiers

  • HAL Id : inria-00292663 , version 1

Cite

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⟩
67 View
159 Download

Share

Gmail Facebook Twitter LinkedIn More