Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps
(2023) In Journal of the ACM 70(5).- Abstract
We prove near-optimal tradeoffs for quantifier depth (also called quantifier rank) 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ω (k/log k). Our tradeoffs 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 introduced by Razborov in the context of proof complexity. We apply this method to reduce the domain size of relational structures while... (More)
We prove near-optimal tradeoffs for quantifier depth (also called quantifier rank) 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ω (k/log k). Our tradeoffs 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 introduced by Razborov in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the minimal quantifier depth needed to distinguish them in finite variable logics.
(Less)
- author
- Berkholz, Christoph and Nordström, Jakob LU
- organization
- publishing date
- 2023-10
- type
- Contribution to journal
- publication status
- published
- subject
- keywords
- bounded variable fragment, first-order counting logic, First-order logic, hardness condensation, lower bounds, quantifier depth, refinement iterations, tradeoffs, Weisfeiler-Leman, XORification
- in
- Journal of the ACM
- volume
- 70
- issue
- 5
- article number
- 32
- publisher
- Association for Computing Machinery (ACM)
- external identifiers
-
- scopus:85174930971
- ISSN
- 0004-5411
- DOI
- 10.1145/3195257
- language
- English
- LU publication?
- yes
- id
- 40b4192f-a8bf-49c3-8113-67478d591b97
- date added to LUP
- 2023-12-11 14:45:14
- date last changed
- 2024-02-09 11:30:51
@article{40b4192f-a8bf-49c3-8113-67478d591b97,
abstract = {{<p>We prove near-optimal tradeoffs for quantifier depth (also called quantifier rank) 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<sup>ω (k/log k)</sup>. Our tradeoffs 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 introduced by Razborov in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the minimal quantifier depth needed to distinguish them in finite variable logics.</p>}},
author = {{Berkholz, Christoph and Nordström, Jakob}},
issn = {{0004-5411}},
keywords = {{bounded variable fragment; first-order counting logic; First-order logic; hardness condensation; lower bounds; quantifier depth; refinement iterations; tradeoffs; Weisfeiler-Leman; XORification}},
language = {{eng}},
number = {{5}},
publisher = {{Association for Computing Machinery (ACM)}},
series = {{Journal of the ACM}},
title = {{Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps}},
url = {{http://dx.doi.org/10.1145/3195257}},
doi = {{10.1145/3195257}},
volume = {{70}},
year = {{2023}},
}