一句话：证明 2-维 Weisfeiler-Leman 算法至多 O(n log n) 次迭代稳定，并引入游走精化与游走逻辑给出匹配线性界。
本文研究 Weisfeiler-Leman（WL）算法的迭代收敛次数及其与计数一阶逻辑的关系。作者证明，2-维 WL 算法在 n 顶点图上至多经过 O(n log n) 次迭代即稳定，由此可得：若两个图可由带计数的三变量一阶逻辑区分，则也可由量词深度至多 O(n log n) 的公式区分。为获得该结果，作者引入一种基于计数游走的新精化——游走精化，并论证其迭代次数与经典 WL 精化至多相差对数因子。通过半单矩阵代数的代数方法，作者进一步证明游走精化的迭代次数具有匹配的线性上界和下界。文中还定义了与游走精化精确对应的游走逻辑和双射游走石子游戏。
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.
@inproceedings{paperbot4978,
title = {Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithm},
author = {Moritz Lichter and Ilia Ponomarenko and Pascal Schweitzer},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785694}
}