Name
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 [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. Nordstrom, 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]. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1137/16M1109072 | SIAM JOURNAL ON COMPUTING |
Keywords | Field | DocType |
proof complexity,resolution,space,width,trade-offs,supercritical | Discrete mathematics,Supercritical fluid,Trade offs,Proof complexity,Mathematics | Journal |
Volume | Issue | ISSN |
49 | 1 | 0097-5397 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christoph Berkholz | 1 | 49 | 7.03 |
| Jakob Nordström | 2 | 0 | 1.01 |