Extraction de sous-formules minimales inconsistantes

Résumé : Une sous-formule minimale inconsistante (Minimally Unsatisfiable Subformula ou MUS en anglais) représente la plus petite cause d'incohérence d'une instance SAT en terme de nombre de clauses. Extraire un ou plusieurs MUS s'avère donc très utile, car ceux-ci circonscrivent les sources d'inconsistance d'une formule CNF. Dans ce papier, une nouvelle méta-heuristique permettant l'approximation ou le calcul d'un MUS est présentée. Une comparaison avec les méthodes les plus compétitives est effectuée, et montre que le plus souvent, en pratique, cette approche surpasse les résultats obtenus par les autres méthodes existantes.
Type de document :
Communication dans un congrès
Journées Francophones de Programmation par Contraintes, 2006, Ecole des Mines d'Alès - Nîmes, 2006
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00085769
Contributeur : Laurent Henocque <>
Soumis le : vendredi 14 juillet 2006 - 08:43:30
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:07:43

Fichier

Identifiants

  • HAL Id : inria-00085769, version 1

Collections

Citation

Eric Gregoire, Bertrand Mazure, Cédric Piette. Extraction de sous-formules minimales inconsistantes. Journées Francophones de Programmation par Contraintes, 2006, Ecole des Mines d'Alès - Nîmes, 2006. 〈inria-00085769〉

Partager

Métriques

Consultations de la notice

148

Téléchargements de fichiers

538