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

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningfagfællebedømt

Dokumenter

  • Fulltext

    Forlagets udgivne version, 944 KB, PDF-dokument

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.

OriginalsprogEngelsk
Artikelnummer32
TidsskriftJournal of the ACM
Vol/bind70
Udgave nummer5
Sider (fra-til)1-32
ISSN0004-5411
DOI
StatusUdgivet - 2023

Bibliografisk note

Funding Information:
Part of the work of the first author was performed while at KTH Royal Institute of Technology supported by a fellowship within the Postdoc-Programme of the German Academic Exchange Service (DAAD). The research of the second author was also partially done at KTH Royal Institute of Technology, and was supported by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007–2013) / ERC grant agreement no. 279611, by the Swedish Research Council grants 621-2010-4797, 621-2012-5645, and 2016-00782, and by the Independent Research Fund Denmark grant 9040-00389B.

Publisher Copyright:
© 2023 Association for Computing Machinery.

ID: 372610177