Skip to Main content Skip to Navigation
Conference papers

Détection et élimination dynamique de la symétrie dans le problème de satisfiabilité

Résumé : Le problème SAT est connu pour être le premier problème de décision de classe NP-complet (Cook,71). C'est un problème central dans la théorie de la complexité. Dans la dernière décennie, les procédures prouvant la satisfiabilité ont été améliorées par l'élimination de la symétrie. Une formule CNF contient usuellement un nombre intéressant de symétries. Il y a deux types d'exploitions des symétries. La première correspond à l'élimination des symétries globales, c'est à dire, seules les symétries initiales du problème (le problème à la racine de l'arbre de recherche) sont détectées et éliminées. La seconde exploite toutes les symétries locales qui apparaissent à chaque noeud de l'arbre de recherche. Les symétries locales doivent être détectées et éliminées dynamiquement durant la recherche. Exploiter ce genre de symétrie semble être une tâche difficile. Quasiment tous les travaux sur l'exploitation de la symétrie dans le problème de la satisfiabilité traitent uniquement le cas des symétries globales. En dépit de leur importance en pratique, seuls quelques travaux étudient les symétries locales. Détecter et éliminer efficacement les symétries locales durant la recherche est un challenge important. Le travail que nous présentons ici est une contribution pour répondre à ce difficile challenge. Nous présentons une nouvelle méthode pour l'élimination des symétries locales qui consiste à réduire l'instance partielle SAT, non encore résolue correspondante à chaque noeud de l'arbre de recherche, à un graphe dont le groupe d'automorphismes est équivalent au groupe de symétries de l'instance partielle SAT. Nous avons utilisé l'outil Saucy pour le calcul du groupe d'automorphisme et nous avons implémenté une technique de coupure de symétrie dans un solveur SAT. Nous avons expérimenté cette méthode sur plusieurs instances SAT et nous l'avons comparé à une méthode qui exploite les symétries globales. Les résultats obtenus sont prometteurs. L'exploitation des symétries locales améliore l'exploitation des seules symétries globales dans la résolution de nombreux problèmes difficiles et elles leurs sont complémentaires si nous combinons les deux techniques.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/inria-00519156
Contributor : Christophe Lecoutre Connect in order to contact the contributor
Submitted on : Saturday, September 18, 2010 - 3:29:45 PM
Last modification on : Saturday, June 25, 2022 - 7:48:40 PM
Long-term archiving on: : Sunday, December 19, 2010 - 2:43:03 AM

File

benhamou2.pdf
Explicit agreement for this submission

Identifiers

  • HAL Id : inria-00519156, version 1

Citation

Belaïd Benhamou, Tarek Nabhani, Richard Ostrowski, Mohamed Réda Saïdi. Détection et élimination dynamique de la symétrie dans le problème de satisfiabilité. JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.81-90. ⟨inria-00519156⟩

Share

Metrics

Record views

82

Files downloads

88