一句话：证明2-WL稳定需O(n^2/log n)次迭代，将C3区分n点图的量词深度上界改进至同阶。
本文研究 n 个顶点图上二维 Weisfeiler-Leman 算法达到稳定所需的迭代次数，以及一阶逻辑中图区分公式的量词深度上界。此前仅知平凡的 O(n^2) 上界，作者证明该上界渐近并不紧。方法上，他们定义了一个双人博弈，用以解耦算法多次迭代中同时发生过程的因果依赖，从而分别处理大颜色类与小颜色类；并证明当颜色类大小有界时，稳定所需迭代次数至多与顶点数线性相关。该结果翻译到逻辑侧，意味着若两个 n 点图可由带计数量词的 3 变量一阶逻辑 C3 区分，则也可由量词深度至多 O(n^2/log n) 的 C3 公式区分。类似结论也可推广到不带计数量词的 L3。
We show that on graphs with n vertices, the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n^2/log(n)) iterations to reach stabilization. This in particular shows that the previously best, trivial upper bound of O(n^2) 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(n^2/log(n)). To prove the result we define a game between two players that enables us to decouple the causal dependencies between the processes happening simultaneously over several iterations of the algorithm. This allows us to treat large color classes and small color classes separately. As part of our proof we show that for graphs with bounded color class size, the number of iterations until stabilization is at most linear in the number of vertices. This also yields a corresponding statement in first-order logic with counting. Similar results can be obtained for the respective logic without counting quantifiers, i.e., for the logic L3.
@article{paperbot787,
title = {Upper Bounds on the Quantifier Depth for Graph Differentiation in First-Order Logic},
author = {Sandra Kiefer and Pascal Schweitzer},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 2},
year = {2019},
doi = {10.23638/lmcs-15(2:19)2019}
}