Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithm

TL;DR

This paper proves that the 2-dimensional Weisfeiler-Leman algorithm stabilizes graphs in O(n log n) iterations, introduces a new walk-based refinement, and establishes bounds using algebraic methods and logic.

Contribution

It introduces a new walk refinement, analyzes its iteration bounds, and connects it to logical definability and pebble games, advancing understanding of graph isomorphism algorithms.

Findings

We show the 2-dimensional Weisfeiler-Leman stabilizes in O(n log n) iterations.

The walk refinement differs from classic WL by at most a logarithmic factor.

Matching linear upper and lower bounds on walk refinement iterations are established.

Abstract

We show that the 2-dimensional Weisfeiler-Leman algorithm stabilizes n-vertex graphs after at most O(n log n) iterations. This implies that if such graphs are distinguishable in 3-variable first order logic with counting, then they can also be distinguished in this logic by a formula of quantifier depth at most O(n log n). For this we exploit a new refinement based on counting walks and argue that its iteration number differs from the classic Weisfeiler-Leman refinement by at most a logarithmic factor. We then prove matching linear upper and lower bounds on the number of iterations of the walk refinement. This is achieved with an algebraic approach by exploiting properties of semisimple matrix algebras. We also define a walk logic and a bijective walk pebble game that precisely correspond to the new walk refinement.