2026-08-01T16:45:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6226 2024-03-06T10:37:45Z ddc:004 open_access

Supercritical Space-Width Trade-Offs for Resolution Berkholz, Christoph Nordström, Jakob Proof complexity resolution space width trade-offs supercritical 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]. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christoph Berkholz and Jakob Nordström 2016 Is Part Of LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2016.57 urn:nbn:de:0030-drops-62266 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.57 eng https://creativecommons.org/licenses/by/3.0/legalcode