Supercritical space-width trade-offs for resolution
(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:
https://lup.lub.lu.se/record/f83f2a47-abdb-4420-98fc-130e246b274a
- author
- Berkholz, Christoph and Nordström, Jakob LU
- publishing date
- 2016-08-01
- 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}}, }