The Logic Behind Colour Refinement

Abstract

Colour Refinement is a combinatorial algorithm that computes a vertex colouring for an input graph to reveal its structural properties. Each iteration of the algorithm refines the current colouring by assessing local information. More precisely, the new colour of a vertex is determined by its current colour and the multiset of colours in its neighbourhood. This refinement procedure continues until it reaches a stable partition of the vertex set into colour classes.

On the practical side, the algorithm admits fast implementations. Because the final colouring is isomorphism-invariant, executing the algorithm on two graphs in parallel can be used to demonstrate that they are not isomorphic. From a theoretical perspective, the algorithm is arguably the most straightforward combinatorial approach to detecting asymmetries—specifically for distinguishing vertices that do not belong to the same orbit of the automorphism group of the graph. Its numerous connections to other areas in computer science stand as evidence of its robustness and naturalness and make it a fascinating object of research.

Among the most elegant connections is the link to counting logic. Colour Refinement assigns distinct final colours to two vertices in a graph if and only if there is a formula in the two-variable fragment ${\text{C}}^2$ of the logic C that distinguishes them, meaning that the formula holds for precisely one of the two vertices. In fact, the vertex colours translate directly into logical formulas with one free variable. As a consequence, Colour Refinement distinguishes two graphs if and only if there is a ${\text{C}}^2$-sentence that distinguishes them. This correspondence extends to higher dimensions: the $k$-variable fragment ${\text{C}}^k$ of C corresponds to the $(k-1)$-dimensional extension of Colour Refinement, the $(k-1)$-dimensional Weisfeiler–Leman algorithm. This algorithm computes a unique colouring for a graph $G$ if and only if $G$ is definable in ${\text{C}}^k$, i.e. there is a sentence in ${\text{C}}^k$ whose only models are $G$ and its isomorphic copies.

As a matter of fact, the link to the logic C goes even deeper: the number of Colour Refinement iterations required to compute distinct colours corresponds exactly to the quantifier depth of a distinguishing formula. Since the iterations induce a sequence of strictly nested vertex partitions, the process must terminate after at most $n-1$ rounds, where $n$ is the number of vertices. Consequently, the value $n-1$ serves as a trivial upper bound on both the number of iterations and the quantifier depth required to distinguish any two (distinguishable) vertices in ${\text{C}}^2$.

My talk provides an introduction to the link between the Colour Refinement procedure and the logic ${\text{C}}^2$. We revisit a simple characterisation of their expressivity on graphs and on general relational structures. The characterisation implies that the definability of a graph in ${\text{C}}^2$ can be checked very efficiently.

We then discuss tight lower bounds on the quantifier depth of ${\text{C}}^2$-formulas required to distinguish vertices. Through a thorough analysis of computational data from Colour Refinement executions, we constructed infinite families of graphs that witness those bounds. We finish with a presentation of a recent purely theoretical reverse-engineering approach to finding long-refinement graphs and a classification of all such graphs with small (or, equivalently, large) degrees.

The talk is based on the collaborations [1, 2, 3] and unpublished work.