Suppression de clauses redondantes dans des instances de SAT - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2007

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.
Fichier principal
Vignette du fichier
11.pdf (178.23 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00151033 , version 1 (01-06-2007)

Identifiants

  • HAL Id : inria-00151033 , version 1

Citer

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⟩
56 Consultations
46 Téléchargements

Partager

Gmail Facebook X LinkedIn More