Supercritical space-width trade-offs for resolution
(2020) In SIAM Journal on Computing 49(1). p.98-118- 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... (More)
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].
(Less)
- author
- Berkholz, Christoph and Nordström, Jakob LU
- publishing date
- 2020
- type
- Contribution to journal
- publication status
- published
- subject
- keywords
- Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width
- in
- SIAM Journal on Computing
- volume
- 49
- issue
- 1
- pages
- 21 pages
- publisher
- Society for Industrial and Applied Mathematics
- external identifiers
-
- scopus:85079820313
- ISSN
- 0097-5397
- DOI
- 10.1137/16M1109072
- language
- English
- LU publication?
- no
- id
- 4b993597-44a9-4287-b48c-fc5ade3ce3a7
- date added to LUP
- 2020-12-18 22:14:35
- date last changed
- 2022-04-26 22:42:12
@article{4b993597-44a9-4287-b48c-fc5ade3ce3a7, abstract = {{<p>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].</p>}}, author = {{Berkholz, Christoph and Nordström, Jakob}}, issn = {{0097-5397}}, keywords = {{Proof complexity; Resolution; Space; Supercritical; Trade-offs; Width}}, language = {{eng}}, number = {{1}}, pages = {{98--118}}, publisher = {{Society for Industrial and Applied Mathematics}}, series = {{SIAM Journal on Computing}}, title = {{Supercritical space-width trade-offs for resolution}}, url = {{http://dx.doi.org/10.1137/16M1109072}}, doi = {{10.1137/16M1109072}}, volume = {{49}}, year = {{2020}}, }