Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps

TL;DR

This paper establishes near-optimal lower bounds on the quantifier depth and Weisfeiler-Leman refinement steps needed to distinguish certain structures, advancing understanding of logical complexity and graph isomorphism tests.

Contribution

It introduces a new technique using hardness condensation to prove tight lower bounds on quantifier depth and refinement steps in first-order logic and counting logic.

Findings

Proves near-optimal trade-offs between quantifier depth and variables in first-order logic.

Establishes lower bounds on Weisfeiler-Leman refinement iterations.

Applies hardness condensation to reduce structure size while preserving logical complexity.

Abstract

We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of $n$-element structures that can be distinguished by a $k$-variable first-order sentence but where every such sentence requires quantifier depth at least $n^{\Omega(k/\log k)}$. Our trade-offs also apply to first-order counting logic, and by the known connection to the $k$-dimensional Weisfeiler--Leman algorithm imply near-optimal lower bounds on the number of refinement iterations. A key component in our proof is the hardness condensation technique recently introduced by [Razborov '16] in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the minimal quantifier depth to distinguish them in finite variable logics.