Supercritical space-width trade-offs for resolution

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

Supercritical space-width trade-offs for resolution. / Berkholz, Christoph; Nordström, Jakob.

In: SIAM Journal on Computing, Vol. 49, No. 1, 2020, p. 98-118.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Berkholz, C & Nordström, J 2020, 'Supercritical space-width trade-offs for resolution', SIAM Journal on Computing, vol. 49, no. 1, pp. 98-118. https://doi.org/10.1137/16M1109072

APA

Berkholz, C., & Nordström, J. (2020). Supercritical space-width trade-offs for resolution. SIAM Journal on Computing, 49(1), 98-118. https://doi.org/10.1137/16M1109072

Vancouver

Berkholz C, Nordström J. Supercritical space-width trade-offs for resolution. SIAM Journal on Computing. 2020;49(1):98-118. https://doi.org/10.1137/16M1109072

Author

Berkholz, Christoph ; Nordström, Jakob. / Supercritical space-width trade-offs for resolution. In: SIAM Journal on Computing. 2020 ; Vol. 49, No. 1. pp. 98-118.

Bibtex

@article{ace663fefa4d4e1394a29b8f7d9bd48f,
title = "Supercritical space-width trade-offs for resolution",
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. Nordstr{\"o}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].",
keywords = "Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width",
author = "Christoph Berkholz and Jakob Nordstr{\"o}m",
year = "2020",
doi = "10.1137/16M1109072",
language = "English",
volume = "49",
pages = "98--118",
journal = "SIAM Journal on Computing",
issn = "0097-5397",
publisher = "Society for Industrial and Applied Mathematics",
number = "1",

}

RIS

TY - JOUR

T1 - Supercritical space-width trade-offs for resolution

AU - Berkholz, Christoph

AU - Nordström, Jakob

PY - 2020

Y1 - 2020

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

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

KW - Proof complexity

KW - Resolution

KW - Space

KW - Supercritical

KW - Trade-offs

KW - Width

U2 - 10.1137/16M1109072

DO - 10.1137/16M1109072

M3 - Journal article

AN - SCOPUS:85079820313

VL - 49

SP - 98

EP - 118

JO - SIAM Journal on Computing

JF - SIAM Journal on Computing

SN - 0097-5397

IS - 1

ER -

ID: 250606016