Skip to Main content Skip to Navigation
Conference papers

Utilisation de la Propagation de Contraintes Booléennes pour la Production de Sous-Clauses

Résumé : La propagation de contraintes booléennes (BCP) est la technique la plus utile et la plus utilisÈe dans les solveurs SAT. Dans cet article, nous proposons une autre utilisation de cette technique dans le but de réduire, en termes de nombre de clauses et de longueur des clauses, la formule initiale. En considérant le graphe d'implications généré par la procédure BCP comme un arbre de résolution, nous pouvons déduire des sous-clauses de la formule initiale. Nous montrons ensuite, comment une telle extension peut être implémentée dans les solveurs actuels où la procédure BCP est utilisée à chaque noeud de l'arbre de recherche. Nous présentons une première implémentation de cette approche dans le cadre d'un pré-traitement pour le solveur Zchaff. Pour finir, des résultats comparatifs préliminaires montrant les points forts et les faiblesses de l'approche sont fournis sur certaines classes d'instances de nature structurées.
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000058
Contributor : Christine Solnon <>
Submitted on : Wednesday, May 25, 2005 - 11:14:44 AM
Last modification on : Wednesday, March 17, 2021 - 6:40:02 PM
Long-term archiving on: : Thursday, April 1, 2010 - 9:32:00 PM

File

Identifiers

  • HAL Id : inria-00000058, version 1

Collections

Citation

Sylvain Darras, Gilles Dequen, Laure Devendeville, Bertrand Mazure, Richard Ostrowski, et al.. Utilisation de la Propagation de Contraintes Booléennes pour la Production de Sous-Clauses. Premières Journées Francophones de Programmation par Contraintes, CRIL - CNRS FRE 2499, Jun 2005, Lens, pp.69-78. ⟨inria-00000058⟩

Share

Metrics

Record views

291

Files downloads

401