Supercritical space-width trade-offs for resolution
Research output: Contribution to journal › Journal article › Research › peer-review
Documents
- Fulltext
Accepted author manuscript, 500 KB, PDF document
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].
Original language | English |
---|---|
Journal | SIAM Journal on Computing |
Volume | 49 |
Issue number | 1 |
Pages (from-to) | 98-118 |
ISSN | 0097-5397 |
DOIs | |
Publication status | Published - 2020 |
- Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width
Research areas
ID: 250606016