Supercritical space-width trade-offs for resolution

Research output: Contribution to journalJournal articleResearchpeer-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 languageEnglish
JournalSIAM Journal on Computing
Volume49
Issue number1
Pages (from-to)98-118
ISSN0097-5397
DOIs
Publication statusPublished - 2020

    Research areas

  • Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width

ID: 250606016