Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic
Sandra Kiefer, Pascal Schweitzer · 2016
We show that on graphs with n vertices the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n2 / log(n)) iterations to reach stabilization. This in particular shows that the previously best, trivial upper bound of O(n2) is asymptotically not tight. In the logic setting this translates to the statement that if two graphs of size n can be distinguished by a formula in first order logic with counting with 3 variables (i.e., in C3) then they can also be distinguished by a C3-formula that has quantifier depth at most O(n2 / log(n)).