Supercritical space-width trade-offs for resolution
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
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].
Original language | English |
---|---|
Title of host publication | 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016 |
Editors | Yuval Rabani, Ioannis Chatzigiannakis, Davide Sangiorgi, Michael Mitzenmacher |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Publication date | 1 Aug 2016 |
Article number | 57 |
ISBN (Electronic) | 9783959770132 |
DOIs | |
Publication status | Published - 1 Aug 2016 |
Externally published | Yes |
Event | 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016 - Rome, Italy Duration: 12 Jul 2016 → 15 Jul 2016 |
Conference
Conference | 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016 |
---|---|
Land | Italy |
By | Rome |
Periode | 12/07/2016 → 15/07/2016 |
Sponsor | AICA, Austrian, Facebook, Microsoft, Microsoft Research, Sapienza University of Rome, Department of Informatics |
Series | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 55 |
ISSN | 1868-8969 |
- Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width
Research areas
ID: 251868331