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

DOI10.1145/2933575.2934560MaRDI QIDQ4635882zbMATHOpenAlexFDO

Authors Christoph Berkholz, Jakob Nordstrom

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1608.08704

zbMATH Keywords

lower boundsfirst-order logictrade-offsquantifier depthWeisfeiler-Leman algorithmbounded-variable fragmentfirst-order counting logichardness condensationrefinement iterationsXORification

Mathematics Subject Classification ID

Graph algorithms (graph-theoretic aspects) (05C85) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Model theory of finite structures (03C13) Subsystems of classical logic (including intuitionistic logic) (03B20) Logic in computer science (03B70)

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/logk)}$. 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.

Recommendations

• Lower bounds for RAMs and quantifier elimination
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Lower bounds to the size of constant-depth propositional proofs
• Bounded-Depth Frege Lower Bounds for Weaker Pigeonhole Principles
• Degree lower bounds of tower-type for approximating formulas with parity quantifiers
• Degree lower bounds of tower-type for approximating formulas with parity quantifiers
• Lower bounds: from circuits to QBF proof systems

Cited in

(6)

• Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithm
• scientific article; zbMATH DE number 1754602 (Why is no real title available?)
• On space and depth in resolution
• Cutting planes width and the complexity of graph isomorphism refutations
• Supercritical space-width trade-offs for resolution
• Tight lower and upper bounds for the complexity of canonical colour refinement

This page was built for publication: Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler--Leman Refinement Steps

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635882)