Supercritical Space-Width Trade-offs for Resolution

TL;DR

This paper demonstrates that certain CNF formulas exhibit a supercritical trade-off between resolution proof space and width, showing that small-width proofs can require significantly more space than previously bounded.

Contribution

It extends the understanding of space-width trade-offs in resolution by establishing supercritical regimes using Razborov's hardness condensation and prior space lower bounds.

Findings

Existence of CNF formulas with supercritical space-width trade-offs

Small-width proofs can require much larger space than linear bounds

Strengthens previous trade-off results in resolution proof complexity

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 [Ben-Sasson '09]}, and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov '16]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordstrom '08].