We show that on graphs with n vertices, the 2-dimensional Weisfeiler-Lemanalgorithm requires at most O(n^2/log(n)) iterations to reach stabilization.This in particular shows that the previously best, trivial upper bound ofO(n^2) is asymptotically not tight. In the logic setting, this translates tothe statement that if two graphs of size n can be distinguished by a formula infirst-order logic with counting with 3 variables (i.e., in C3), then they canalso be distinguished by a C3-formula that has quantifier depth at mostO(n^2/log(n)). To prove the result we define a game between two players that enables us todecouple the causal dependencies between the processes happening simultaneouslyover several iterations of the algorithm. This allows us to treat large colorclasses and small color classes separately. As part of our proof we show thatfor graphs with bounded color class size, the number of iterations untilstabilization is at most linear in the number of vertices. This also yields acorresponding statement in first-order logic with counting. Similar results can be obtained for the respective logic without countingquantifiers, i.e., for the logic L3.
展开▼
