Skip to Main content Skip to Navigation
Conference papers

Suppression de clauses redondantes dans des instances de SAT

Résumé : Dans ce papier, nous étudions comment la suppression d'une partie des clauses redondantes d'une instance de SAT permet d'améliorer l'efficacité des solveurs SAT modernes. Le problème consistant à détecter si une instance contient ou non des clauses redondantes est NP-Complet. Nous proposons une méthode de suppression des clauses redondantes incomplète mais polynomiale que nous utilisons comme pré-traitement pour des solveurs SAT. Cette méthode basée sur la propagation unitaire offre des résultats intéressants notamment sur des instances très difficiles issues du monde réel.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00151033
Contributor : Sylvain Soliman <>
Submitted on : Friday, June 1, 2007 - 2:51:14 PM
Last modification on : Thursday, January 11, 2018 - 6:19:28 AM
Long-term archiving on: : Thursday, April 8, 2010 - 6:41:03 PM

File

11.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00151033, version 1

Collections

Citation

Olivier Fourdrinoy, Eric Grégoire, Bertrand Mazure, Lakhdar Saïs. Suppression de clauses redondantes dans des instances de SAT. Troisièmes Journées Francophones de Programmationpar Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France. ⟨inria-00151033⟩

Share

Metrics

Record views

145

Files downloads

65