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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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 (k= log k). 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 quantifier depth required to distinguish them.

Original languageEnglish
Title of host publicationProceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016
Number of pages10
PublisherInstitute of Electrical and Electronics Engineers Inc.
Publication date5 Jul 2016
Pages267-276
ISBN (Electronic)9781450343916
DOIs
Publication statusPublished - 5 Jul 2016
Externally publishedYes
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, United States
Duration: 5 Jul 20168 Jul 2016

Conference

Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
LandUnited States
ByNew York
Periode05/07/201608/07/2016
SponsorACM Special Interest Group on Logic and Computation (SIGLOG), Association for Computing Machinery, et al., European Association for Computer Science Logic, IEEE Computer Society, IEEE Technical Committee on Mathematical Foundations of Computer Science
SeriesProceedings - Symposium on Logic in Computer Science
Volume05-08-July-2016
ISSN1043-6871

    Research areas

  • bounded variable fragment, first-order counting logic, First-order logic, hardness condensation, lower bounds, quantifier depth, refinement iterations, trade-offs, Weisfeiler - Leman, XORification

ID: 251868527