Logarithmic Weisfeiler-Leman Identifies All Planar Graphs

The Weisfeiler-Leman (WL) algorithm is a well-known combinatorial procedure for detecting symmetries in graphs that is widely used in graph-isomorphism tests. It proceeds by iteratively computing vertex colours. The number of iterations needed to obtain the final output is crucial for the parallelisability of the algorithm. We show that there is a constant k such that every planar graph can be identified (that is, distinguished from every non-isomorphic graph) by the k-dimensional WL algorithm within a logarithmic number of iterations. This generalises a result due to Verbitsky, who proved the same for 3-connected planar graphs. The number of iterations needed by the k-dimensional WL algorithm to identify a graph corresponds to the quantifier depth of a sentence that defines the graph in the (k+1)-variable fragment C^(k+1) of first-order logic with counting quantifiers. Thus, our result implies that every planar graph is definable by a C^(k+1)-sentence of logarithmic quantifier depth. This is joint work with Martin Grohe.