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

DOI10.1145/2933575.2934560zbMATH Open1394.03052arXiv1608.08704OpenAlexW2963494352MaRDI QIDQ4635882FDOQ4635882

Jakob Nordstrom, Christoph Berkholz

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)

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.

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)

Cited In (5)

• Tight lower and upper bounds for the complexity of canonical colour refinement
• Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic
• Cutting planes width and the complexity of graph isomorphism refutations
• Supercritical Space-Width Trade-offs for Resolution
• On space and depth in resolution

Recommendations

• Title not available (Why is that?) 👍 👎
• Lower bounds to the size of constant-depth propositional proofs 👍 👎
• Lower bounds for RAMs and quantifier elimination 👍 👎
• Lower bounds: from circuits to QBF proof systems 👍 👎
• Bounds for the Quantifier Depth in Finite-Variable Logics 👍 👎
• Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic 👍 👎
• 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 👍 👎

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)