Supercritical space-width trade-offs for resolution

Christoph Berkholz; Jakob Nordström

doi:10.1137/16M1109072

Supercritical space-width trade-offs for resolution

Christoph Berkholz
, Jakob Nordström

Algorithms and Complexity

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › peer review

52 Downloads (Pure)

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

Originalsprog	Engelsk
Tidsskrift	SIAM Journal on Computing
Vol/bind	49
Udgave nummer	1
Sider (fra-til)	98-118
ISSN	0097-5397
DOI	https://doi.org/10.1137/16M1109072
Status	Udgivet - 2020

Finansiering

∗Received by the editors December 21, 2016; accepted for publication (in revised form) July 30, 2018; published electronically February 4, 2020. A preliminary version of this work appeared in Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP′16). https://doi.org/10.1137/16M1109072 Funding: The first author was supported by a fellowship within the Postdoc-Programme of the German Academic Exchange Service (DAAD). The second author was supported by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007–2013) ERC grant agreement 279611 and by Swedish Research Council grants 621-2010-4797, 621-2012-5645, and 2016-00782.

Adgang til dokumentet

10.1137/16M1109072

FulltextAccepteret manuskript, 500 KBLicens: CC BY

Biblioteksadgang?

Tjek tilgængelighed hos det Kgl. Bibliotek

Citationsformater

@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 Publications",

number = "1",

}

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

SN - 0097-5397

VL - 49

SP - 98

EP - 118

JO - SIAM Journal on Computing

JF - SIAM Journal on Computing

IS - 1

ER -