Des ensembles Horn strong backdoor aux ensembles ordonnés strong backdoor

Résumé : L'identification et l'exploitation de structures cachées dans un problème est reconnue comme étant un moyen fondamental pour contrecarrer l'explosion combinatoire de sa résolution. Récemment, une structure particulière appelée (strong) backdoor a été identifiée pour le problème de satisfaisabilité de formule CNF (SAT). Certaines connexions entre les ensembles strong backdoor et la difficulté intrinsèque des problèmes SAT ont été mises en évidence, permettant une meilleure approximation de la borne de complexité en temps dans le pire des cas. On peut calculer des ensembles strong backdoor pour chaque classe polynomiale. Dans [Parisetals06], une méthode d'approximation d'ensembles strong backdoor pour la classe des formules de Horn a été proposée. Cette approximation est réalisée en deux étapes. Dans un premier temps, on calcule le meilleur Horn renommage du point de vue du nombre de clauses de Horn de la CNF de départ. Ensuite on extrait un ensemble Horn strong backdoor de la partie non Horn de la formule renommée. Dans cet article, nous proposons de calculer des ensembles Horn strong backdoor en utilisant le même procédé mais en minimisant le nombre de littéraux positifs dans la partie non Horn de la formule renommée au lieu du nombre de clauses. Puis nous étendons cette méthode à la classe des formules ordonnée [benoist99] qui est une extension de la classe des formules de Horn. Cette méthode nous garantit l'obtention d'ensembles Ordonné strong backdoor de taille plus petite ou égale à ceux des ensembles Horn strong backdoor (jamais plus grande). Les résultats expérimentaux montrent que ces nouvelles méthodes permettent de réduire la taille des ensembles strong backdoor sur certaines instances et que leur exploitation permet également d'améliorer les performances des solveurs SAT.
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 [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00151052
Contributeur : Sylvain Soliman <>
Soumis le : vendredi 1 juin 2007 - 15:06:03
Dernière modification le : jeudi 15 mars 2018 - 16:56:06
Document(s) archivé(s) le : vendredi 21 septembre 2012 - 16:02:06

Fichier

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

Identifiants

  • HAL Id : inria-00151052, version 1

Collections

Citation

Lionel Paris, Richard Ostrowski, Pierre Siegel. Des ensembles Horn strong backdoor aux ensembles ordonnés strong backdoor. Troisièmes Journées Francophones de Programmationpar Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France, 2007, JFPC07. 〈inria-00151052〉

Partager

Métriques

Consultations de la notice

93

Téléchargements de fichiers

132