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.