Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Supercritical space-width trade-offs for resolution

Berkholz, Christoph and Nordström, Jakob LU (2016) 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016 In Leibniz International Proceedings in Informatics, LIPIcs 55.
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 resolution proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [Ben- Sasson 2009], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov 2016]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordström 2008].

Please use this url to cite or link to this publication:
author
and
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width
host publication
43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016
series title
Leibniz International Proceedings in Informatics, LIPIcs
editor
Rabani, Yuval ; Chatzigiannakis, Ioannis ; Sangiorgi, Davide and Mitzenmacher, Michael
volume
55
article number
57
publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
conference name
43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016
conference location
Rome, Italy
conference dates
2016-07-12 - 2016-07-15
external identifiers
  • scopus:85012892631
ISSN
1868-8969
ISBN
9783959770132
DOI
10.4230/LIPIcs.ICALP.2016.57
language
English
LU publication?
no
id
f83f2a47-abdb-4420-98fc-130e246b274a
date added to LUP
2020-12-18 22:21:05
date last changed
2022-02-01 18:41:07
@inproceedings{f83f2a47-abdb-4420-98fc-130e246b274a,
  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 resolution proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [Ben- Sasson 2009], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov 2016]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordström 2008].</p>}},
  author       = {{Berkholz, Christoph and Nordström, Jakob}},
  booktitle    = {{43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016}},
  editor       = {{Rabani, Yuval and Chatzigiannakis, Ioannis and Sangiorgi, Davide and Mitzenmacher, Michael}},
  isbn         = {{9783959770132}},
  issn         = {{1868-8969}},
  keywords     = {{Proof complexity; Resolution; Space; Supercritical; Trade-offs; Width}},
  language     = {{eng}},
  month        = {{08}},
  publisher    = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
  series       = {{Leibniz International Proceedings in Informatics, LIPIcs}},
  title        = {{Supercritical space-width trade-offs for resolution}},
  url          = {{http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.57}},
  doi          = {{10.4230/LIPIcs.ICALP.2016.57}},
  volume       = {{55}},
  year         = {{2016}},
}