| 1. |
- Berkholz, Christoph, et al.
(author)
-
Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps
- 2016
-
In: PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016). - New York, NY, USA : Institute of Electrical and Electronics Engineers (IEEE). - 9781450343916 ; , s. 267-276
-
Conference paper (peer-reviewed)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(Omega(k/logk)). 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.
|
|
| 3. |
- Berkholz, Christoph, et al.
(author)
-
Supercritical space-width trade-offs for resolution
- 2020
-
In: SIAM journal on computing (Print). - : Society for Industrial & Applied Mathematics (SIAM). - 0097-5397 .- 1095-7111. ; 49:1, s. 98-118
-
Journal article (peer-reviewed)abstract
- We show that there are CNF formulas which can be refuted in resolution in both small space and small width, but for which any small-width proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [E. Ben-Sasson, SIAM J. Comput., 38 (2009), pp. 2511-2525], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [A.A. Razborov, J. ACM, 63 (2016), 16]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [E. Ben-Sasson and J. Nordström, Short proofs may be spacious: An optimal separation of space and length in resolution, in Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS '08), 2008, pp. 709-718].
|
|
