Dynamic Symmetry Breaking by Simulating Zykov Contraction

Abstract. We present a new method to break symmetry in graph coloring problems. While most alternative techniques add symmetry breaking predicates in a pre-processing step, we developed a learning scheme that translates each encountered conflict into one conflict clause which covers equivalent conflicts arising from any permutation of the colors. Our technique introduces new Boolean variables during the search. For many problems the size of the resolution refutation can be significantly reduced by this technique. Although this is shown for various hand-made refutations, it is rarely used in practice, because it is hard to determine which variables to introduce defining useful predicates. In case of graph coloring, the reason for each conflicting coloring can be expressed as a node in the Zykov-tree, that stems from merging some vertices and adding some edges. So, we focus on variables that represent the Boolean expression that two vertices can be merged (if set to true), or that ...

• Type: Conference
• Year: 2009
• Where: SAT
• Authors: Bas Schaafsma, Marijn Heule, Hans van Maaren
• Keywords: Graph Coloring, Graph Coloring Problems, Hardware, SAT 2009, Symmetry Breaking Predicates