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

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps. / Berkholz, Christoph; Nordström, Jakob.

In: Journal of the ACM, Vol. 70, No. 5, 32, 2023, p. 1-32.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Berkholz, C & Nordström, J 2023, 'Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps', Journal of the ACM, vol. 70, no. 5, 32, pp. 1-32. https://doi.org/10.1145/3195257

APA

Berkholz, C., & Nordström, J. (2023). Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps. Journal of the ACM, 70(5), 1-32. [32]. https://doi.org/10.1145/3195257

Vancouver

Berkholz C, Nordström J. Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps. Journal of the ACM. 2023;70(5):1-32. 32. https://doi.org/10.1145/3195257

Author

Berkholz, Christoph ; Nordström, Jakob. / Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps. In: Journal of the ACM. 2023 ; Vol. 70, No. 5. pp. 1-32.

Bibtex

@article{b0dee9dfe6874945a910011a797e9c60,
title = "Near-optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps",
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 maintaining the minimal quantifier depth needed to distinguish them in finite variable logics.",
keywords = "bounded variable fragment, first-order counting logic, First-order logic, hardness condensation, lower bounds, quantifier depth, refinement iterations, tradeoffs, Weisfeiler-Leman, XORification",
author = "Christoph Berkholz and Jakob Nordstr{\"o}m",
note = "Publisher Copyright: {\textcopyright} 2023 Association for Computing Machinery.",
year = "2023",
doi = "10.1145/3195257",
language = "English",
volume = "70",
pages = "1--32",
journal = "Journal of the ACM",
issn = "0004-5411",
publisher = "Association for Computing Machinery",
number = "5",

}

RIS

TY - JOUR

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

AU - Berkholz, Christoph

AU - Nordström, Jakob

N1 - Publisher Copyright: © 2023 Association for Computing Machinery.

PY - 2023

Y1 - 2023

N2 - 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.

AB - 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.

KW - bounded variable fragment

KW - first-order counting logic

KW - First-order logic

KW - hardness condensation

KW - lower bounds

KW - quantifier depth

KW - refinement iterations

KW - tradeoffs

KW - Weisfeiler-Leman

KW - XORification

UR - http://www.scopus.com/inward/record.url?scp=85174930971&partnerID=8YFLogxK

U2 - 10.1145/3195257

DO - 10.1145/3195257

M3 - Journal article

AN - SCOPUS:85174930971

VL - 70

SP - 1

EP - 32

JO - Journal of the ACM

JF - Journal of the ACM

SN - 0004-5411

IS - 5

M1 - 32

ER -

ID: 372610177