Supercritical space-width trade-offs for resolution

Forskningsoutput: TidskriftsbidragArtikel i vetenskaplig tidskrift


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].


Externa organisationer
  • Humboldt University of Berlin
  • University of Copenhagen
  • KTH Royal Institute of Technology

Ämnesklassifikation (UKÄ) – OBLIGATORISK

  • Datavetenskap (datalogi)


Sidor (från-till)98-118
Antal sidor21
TidskriftSIAM Journal on Computing
Utgåva nummer1
StatusPublished - 2020
Peer review utfördJa
Externt publiceradJa