Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00151052
Contributor : Sylvain Soliman <>
Submitted on : Friday, June 1, 2007 - 3:06:03 PM
Last modification on : Monday, March 30, 2020 - 8:53:49 AM
Long-term archiving on: : Friday, September 21, 2012 - 4:02:06 PM

File

44.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00151052, version 1

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. ⟨inria-00151052⟩

Share

Metrics

Record views

122

Files downloads

171