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.
Type de document :
Communication dans un congrès
JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.81-90, 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00519156
Contributeur : Christophe Lecoutre <>
Soumis le : samedi 18 septembre 2010 - 15:29:45
Dernière modification le : jeudi 15 mars 2018 - 16:56:06
Document(s) archivé(s) le : dimanche 19 décembre 2010 - 02:43:03

Fichier

benhamou2.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : inria-00519156, version 1

Collections

Citation

Belaïd Benhamou, Tarek Nabhani, Richard Ostrowski, Mohamed 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, 2010. 〈inria-00519156〉

Partager

Métriques

Consultations de la notice

118

Téléchargements de fichiers

133