Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

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

Berkholz, Christoph and Nordström, Jakob LU (2016) 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 In Proceedings - Symposium on Logic in Computer Science 05-08-July-2016. p.267-276
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 (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... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
and
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
bounded variable fragment, first-order counting logic, First-order logic, hardness condensation, lower bounds, quantifier depth, refinement iterations, trade-offs, Weisfeiler - Leman, XORification
host publication
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016
series title
Proceedings - Symposium on Logic in Computer Science
volume
05-08-July-2016
pages
10 pages
publisher
Association for Computing Machinery (ACM)
conference name
31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
conference location
New York, United States
conference dates
2016-07-05 - 2016-07-08
external identifiers
  • scopus:84994626925
ISSN
1043-6871
ISBN
9781450343916
DOI
10.1145/2933575.2934560
language
English
LU publication?
no
id
98079e6a-7e7c-4e99-a5a1-93a8305c69e2
date added to LUP
2020-12-18 22:21:42
date last changed
2022-04-03 07:05:17
@inproceedings{98079e6a-7e7c-4e99-a5a1-93a8305c69e2,
  abstract     = {{<p>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.</p>}},
  author       = {{Berkholz, Christoph and Nordström, Jakob}},
  booktitle    = {{Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016}},
  isbn         = {{9781450343916}},
  issn         = {{1043-6871}},
  keywords     = {{bounded variable fragment; first-order counting logic; First-order logic; hardness condensation; lower bounds; quantifier depth; refinement iterations; trade-offs; Weisfeiler - Leman; XORification}},
  language     = {{eng}},
  month        = {{07}},
  pages        = {{267--276}},
  publisher    = {{Association for Computing Machinery (ACM)}},
  series       = {{Proceedings - Symposium on Logic in Computer Science}},
  title        = {{Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler - Leman Refinement Steps}},
  url          = {{http://dx.doi.org/10.1145/2933575.2934560}},
  doi          = {{10.1145/2933575.2934560}},
  volume       = {{05-08-July-2016}},
  year         = {{2016}},
}