Supercritical space-width trade-offs for resolution

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-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 languageEnglish
Title of host publication43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016
EditorsYuval Rabani, Ioannis Chatzigiannakis, Davide Sangiorgi, Michael Mitzenmacher
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication date1 Aug 2016
Article number57
ISBN (Electronic)9783959770132
DOIs
Publication statusPublished - 1 Aug 2016
Externally publishedYes
Event43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016 - Rome, Italy
Duration: 12 Jul 201615 Jul 2016

Conference

Conference43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016
LandItaly
ByRome
Periode12/07/201615/07/2016
SponsorAICA, Austrian, Facebook, Microsoft, Microsoft Research, Sapienza University of Rome, Department of Informatics
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume55
ISSN1868-8969

    Research areas

  • Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width

ID: 251868331