Accidental Research: Scalable Algorithms for Graph Automorphism and Canonical Labeling

Accidental research is when you’re an expert in some domain and seek to solve problem A in that domain. You soon discover that to solve A you need to also solve B which, however, comes from a domain in which you have little, or even no, expertise. You, thus, explore existing solutions to B but are disappointed to find out that they just aren’t up to the task of solving A. Your options at this point are a) to abandon this futile project, or b) to try and find a solution to B that will help you solve A. While this might seem like a fool’s errand, you have the advantage over B experts of being unencumbered by their experience. You are a novice who does not, yet, appreciate the complexity of B, but are able to explore it from a fresh perspective. You also bring along expertise from your own domain to connect what you know with what you hope to learn. If you’re lucky, you may succeed in finding a solution to B that helps you solve A.

This scenario played out in two cases: developing the GRASP conflict-driven clause-learning (CDCL) SAT solver in the context of performing timing analysis of very large scale integrated (VLSI) circuits, and developing the saucy graph automorphism program to find and break symmetries in large SAT problems. Ironically, in both cases solving problem B (GRASP, saucy) turned out to be much more impactful than solving problem A (timing analysis, breaking symmetries.) Without the trigger of problem A, however, neither GRASP nor saucy would have been conceived.

In this talk I will trace the development of the saucy graph automorphism program. Breaking the symmetries of large SAT instances (millions of variables and clauses) was conjectured to be helpful in further scaling modern CDCL SAT solvers. Finding those symmetries, however, was a bottleneck since the sizes of the graphs encoding SAT instances were beyond the capabilities of existing automorphism algorithms. We developed saucy in stages as our understanding of classical graph automorphism algorithms evolved. We slowly learned that while these algorithms did produce a generator set for a garph’s symmetry group, they were in fact primarily concerned with deriving a canonical labeling of the graph. Since our goal was simply just finding an irredundant generator set, we replaced the canonical labeling search tree in these algorithms with a permutation search tree based on an ordered partition pair (OPP) data structure that implicitly encodes sets of vertex permutations. This change re-cast the problem as a direct search for vertex permutations that preserve a graph’s edge relation and enabled two powerful OPP pruning mechanisms allowing saucy to outperform standard algorithms by several orders of magnitude.