Supercritical Space-Width Trade-Offs for Resolution
international colloquium on automata languages and programming, pp. 57:1-57:14, 2016.
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...More
Full Text (Upload PDF)
PPT (Upload PPT)