Supercritical Space-Width Trade-offs for Resolution
Computational Complexity
2016-12-22 v1 Discrete Mathematics
Logic in Computer Science
Combinatorics
Logic
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].
Cite
@article{arxiv.1612.07162,
title = {Supercritical Space-Width Trade-offs for Resolution},
author = {Christoph Berkholz and Jakob Nordström},
journal= {arXiv preprint arXiv:1612.07162},
year = {2016}
}