Power and limits of the Weisfeiler-Leman algorithm
- Stärken und Grenzen des Weisfeiler-Leman-Algorithmus
Kiefer, Sandra; Grohe, Martin (Thesis advisor); Schweitzer, Pascal (Thesis advisor); Immerman, Neil (Thesis advisor)
Dissertation / PhD Thesis
Dissertation, RWTH Aachen University, 2020
The Weisfeiler-Leman (WL) algorithm is a fundamental combinatorial technique used to classify graphs and other relational structures. It dates back to the 1960s and has applications in numerous fields of theoretical and practical computer science, such as finite model theory, descriptive complexity theory, propositional proof complexity, and machine learning. Recently discovered links to graph kernels and neural networks demonstrate the persisting importance of the algorithm. It finds particularly prominent use in approaches to the graph isomorphism problem, the task to decide whether two graphs are structurally equivalent or not. Most notably, Babai's breakthrough result from 2016, a quasipolynomial-time graph isomorphism test, relies heavily on a high-dimensional version of the algorithm. Roughly speaking, for every natural number k, the k-dimensional version of the algorithm (k-WL) iteratively computes a colouring of the vertex k-tuples of the input graph. The larger k, the more powerful k-WL becomes. Still, there is no fixed dimension which decides graph isomorphism in general. On the other hand, it is usually highly non-trivial to tell if and when k-WL distinguishes two particular graphs. This thesis explores that frontier and aims at providing a better understanding of the dynamics, the power, and the limits of the WL algorithm. Through its connections to many research areas, beautiful and surprising characterisations of k-WL have been discovered. For example, its expressive power is captured by the counting logic C^(k+1) and also by a certain type of Ehrenfeucht-Fraïssé game. This thesis combines the three characterisations of the algorithm to obtain powerful proof techniques. We first study the number of iterations of the algorithm until stabilisation, which is closely connected to the quantifier depth of a distinguishing C^k-formula. Via the construction of infinite graph families, we show that the trivial upper bound n-1 on the number of iterations of 1-WL on n-vertex graphs is tight (up to an additive constant of 1). This improves upon the previous best lower bound of n-sqrt(n). In contrast to this, the situation for 2-WL is quite different: we prove that the trivial upper bound on the iteration number is not tight, not even asymptotically. As simple examples show, even if the algorithm needs few iterations to compute its output, this does not imply that it distinguishes the given graph from all others. The parameter to study concerning the expressive power of the algorithm is its dimension. In this direction, we present a complete characterisation of the graphs and all relational structures for which 1-WL correctly decides isomorphism. Proceeding to higher dimensions, we investigate the ability of the algorithm to decompose graphs. By applying the results, we show that 3-WL identifies every planar graph, which drastically improves upon all previously known bounds. Planar graphs constitute the base case in our further consideration of graph classes parameterised by their Euler genus. We show that the WL dimension of every graph is at most linear in its Euler genus. This result is the first explicit parametrisation of the WL dimension by the Euler genus of the input graph.