COPLAS talk by Jacob Nordström

Copenhagen Programming Language Seminar (COPLAS)


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


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^{Omega(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 introduced by Razborov (2016) 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.

Jacob Nordström
Find bio here.

Jakob Grue Simonsen (, +45 60757989)