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.
Type de document :
Communication dans un congrès
Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.277-285, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00292663
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : mercredi 2 juillet 2008 - 11:57:45
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28
Document(s) archivé(s) le : vendredi 28 mai 2010 - 23:04:31

Fichier

pages-277-285-article49.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00292663, version 1

Collections

Citation

Cédric Piette, Youssef Hamadi, Lakhdar Saïs. Vivification de formules propositionnelles clausales. Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.277-285, 2008. 〈inria-00292663〉

Partager

Métriques

Consultations de la notice

146

Téléchargements de fichiers

154