MiniMerge: Symmetry-Free Learning in Combinatorial Problems

MiniMerge: Symmetry-Free Learning in Combinatorial Problems

Schaafsma, B.J.

Heule, M.J.H. (mentor)
Van Maaren, H. (mentor)
Witteveen, C. (mentor)

Electrical Engineering, Mathematics and Computer Science

Algorithms

2009-05-29

We present a new method to break symmetry in graph coloring problems, which can be applied in many classes of combinatorial 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 combines Extended Resolution with domain specific knowledge. Although the Extended Resolution proof system is powerful in theory, 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 an edge can be placed between them (if set to false). Further, our algorithm reduces the number of introduced variables by reusing them as much as possible. We implemented our technique in the state-of-the-art solver MiniSat2. It is competitive with alternative SAT based techniques for graph coloring problems. Moreover, our technique can be used on top of other symmetry breaking techniques. In fact, combined with adding symmetry breaking predicates, huge performance gains are realized.

Satisfiability
Graph coloring
Symmetry breaking
Conflict-driven learning

http://resolver.tudelft.nl/uuid:9b00b409-d19b-4c15-9026-1e35fd2afdbb

2009-06-11

Student theses

master thesis

(c) 2009 Schaafsma, B.J.