Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Supercritical space-width trade-offs for resolution

Berkholz, Christoph and Nordström, Jakob LU (2020) In SIAM Journal on Computing 49(1). p.98-118
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... (More)

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

(Less)
Please use this url to cite or link to this publication:
author
and
publishing date
type
Contribution to journal
publication status
published
subject
keywords
Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width
in
SIAM Journal on Computing
volume
49
issue
1
pages
21 pages
publisher
Society for Industrial and Applied Mathematics
external identifiers
  • scopus:85079820313
ISSN
0097-5397
DOI
10.1137/16M1109072
language
English
LU publication?
no
id
4b993597-44a9-4287-b48c-fc5ade3ce3a7
date added to LUP
2020-12-18 22:14:35
date last changed
2022-04-26 22:42:12
@article{4b993597-44a9-4287-b48c-fc5ade3ce3a7,
  abstract     = {{<p>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].</p>}},
  author       = {{Berkholz, Christoph and Nordström, Jakob}},
  issn         = {{0097-5397}},
  keywords     = {{Proof complexity; Resolution; Space; Supercritical; Trade-offs; Width}},
  language     = {{eng}},
  number       = {{1}},
  pages        = {{98--118}},
  publisher    = {{Society for Industrial and Applied Mathematics}},
  series       = {{SIAM Journal on Computing}},
  title        = {{Supercritical space-width trade-offs for resolution}},
  url          = {{http://dx.doi.org/10.1137/16M1109072}},
  doi          = {{10.1137/16M1109072}},
  volume       = {{49}},
  year         = {{2020}},
}