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.
Type de document :
Communication dans un congrès
Troisièmes Journées Francophones de Programmationpar Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France, 2007, JFPC07
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00151033
Contributeur : Sylvain Soliman <>
Soumis le : vendredi 1 juin 2007 - 14:51:14
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28
Document(s) archivé(s) le : jeudi 8 avril 2010 - 18:41:03

Fichier

11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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, 2007, JFPC07. 〈inria-00151033〉

Partager

Métriques

Consultations de la notice

79

Téléchargements de fichiers

50