{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T19:38:00Z","timestamp":1787341080727,"version":"build-2736575974"},"reference-count":37,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Comput."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats: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 proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [E. Ben-Sasson, SIAM J. Comput., 38 (2009), pp. 2511--2525], and provides one more example of trade-offs in the \"supercritical\" regime above worst case recently identified by [A.A. Razborov, J. ACM, 63 (2016), 16]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [E. Ben-Sasson and J. Nordstr\u00f6m, Short proofs may be spacious: An optimal separation of space and length in resolution, in Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS '08), 2008, pp. 709--718].<\/jats:p>","DOI":"10.1137\/16m1109072","type":"journal-article","created":{"date-parts":[[2020,2,4]],"date-time":"2020-02-04T13:02:35Z","timestamp":1580821355000},"page":"98-118","source":"Crossref","is-referenced-by-count":5,"title":["Supercritical Space-Width Trade-offs for Resolution"],"prefix":"10.1137","volume":"49","author":[{"given":"Christoph","family":"Berkholz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2700-4285","authenticated-orcid":true,"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2020,2,4]]},"reference":[{"key":"atypb1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"atypb2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"atypb3","doi-asserted-by":"publisher","DOI":"10.1145\/2898435"},{"key":"atypb4","unstructured":"R. J. Bayardo, Jr. and R. Schrag,\n                      Using CSP look-back techniques to solve real-world SAT instances\n                      , in Proceedings of the 14th National Conference on Artificial Intelligence (AAAI '97), 1997, pp. 203-208."},{"key":"atypb5","doi-asserted-by":"publisher","DOI":"10.1137\/130914085"},{"key":"atypb6","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700369156"},{"key":"atypb7","doi-asserted-by":"crossref","unstructured":"C. Beck, J. Nordstr\u00f6m, and B. Tang,\n                      Some trade-off results for polynomial calculus\n                      , in Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC '13), 2013, pp. 813-822.","DOI":"10.1145\/2488608.2488711"},{"key":"atypb8","doi-asserted-by":"publisher","DOI":"10.1137\/080723880"},{"key":"atypb9","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.10089"},{"key":"atypb10","doi-asserted-by":"crossref","unstructured":"E. Ben-Sasson and J. Nordstr\u00f6m,\n                      Short proofs may be spacious: An optimal separation of space and length in resolution\n                      , in Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS '08), 2008, pp. 709-718.","DOI":"10.1109\/FOCS.2008.42"},{"key":"atypb11","unstructured":"E. Ben-Sasson and J. Nordstr\u00f6m,\n                      Understanding space in proof complexity: Separations and trade-offs via substitutions\n                      , in Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11), 2011, pp. 401-416."},{"key":"atypb12","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"atypb13","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.06.003"},{"key":"atypb14","doi-asserted-by":"crossref","unstructured":"C. Berkholz,\n                      On the complexity of finding narrow proofs\n                      , in Proceedings of the 53rd Annual IEEE Symposium on Foundations of Computer Science (FOCS '12), 2012, pp. 351-360.","DOI":"10.1109\/FOCS.2012.48"},{"key":"atypb15","doi-asserted-by":"crossref","unstructured":"C. Berkholz and J. Nordstr\u00f6m,\n                      Near-optimal lower bounds on quantifier depth and Weisfeiler-Leman refinement steps\n                      , in Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS '16), 2016, pp. 267-276.","DOI":"10.1145\/2933575.2934560"},{"key":"atypb16","doi-asserted-by":"crossref","unstructured":"C. Berkholz and J. Nordstr\u00f6m,\n                      Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps\n                      , Technical Report TR16-135, Electronic Colloquium on Computational Complexity (ECCC), 2016; preliminary version in LICS '16.","DOI":"10.1145\/2933575.2934560"},{"key":"atypb17","unstructured":"A. Blake,\n                      Canonical Expressions in Boolean Algebra\n                      , Ph.D. thesis, University of Chicago, Chicago, IL, 1937."},{"key":"atypb18","unstructured":"I. Bonacina,\n                      Total space in resolution is at least width squared\n                      , in Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP '16), Leibniz International Proceedings in Informatics (LIPIcs) 55, 2016, 56."},{"key":"atypb19","doi-asserted-by":"crossref","unstructured":"I. Bonacina, N. Galesi, and N. Thapen,\n                      Total space in resolution\n                      , in Proceedings of the 55th Annual IEEE Symposium on Foundations of Computer Science (FOCS '14), 2014, pp. 641-650.","DOI":"10.1109\/FOCS.2014.74"},{"key":"atypb20","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"atypb21","doi-asserted-by":"crossref","unstructured":"M. Clegg, J. Edmonds, and R. Impagliazzo,\n                      Using the Groebner basis algorithm to find proofs of unsatisfiability\n                      , in Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC '96), 1996, pp. 174-183.","DOI":"10.1145\/237814.237860"},{"key":"atypb22","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"atypb23","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"atypb24","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"atypb25","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"atypb26","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"atypb27","unstructured":"A. Hertel,\n                      Applications of Games to Propositional Proof Complexity\n                      , Ph.D. thesis, University of Toronto, Toronto, ON, Canada, 2008, available athttp:\/\/www.cs.utoronto.ca\/~ahertel\/."},{"key":"atypb28","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"atypb29","doi-asserted-by":"crossref","unstructured":"M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik,\n                      Chaff: Engineering an efficient SAT solver\n                      , in Proceedings of the 38th Design Automation Conference (DAC '01), 2001, pp. 530-535.","DOI":"10.1145\/378239.379017"},{"key":"atypb30","doi-asserted-by":"publisher","DOI":"10.1137\/060668250"},{"key":"atypb31","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:15)2013"},{"key":"atypb32","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2013.v009a014"},{"key":"atypb33","unstructured":"A. A. Razborov,\n                      An Ultimate Trade-Off in Propositional Proof Complexity\n                      , Technical Report TR15-033, Electronic Colloquium on Computational Complexity (ECCC), 2015."},{"key":"atypb34","doi-asserted-by":"publisher","DOI":"10.1145\/2858790"},{"key":"atypb35","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"atypb36","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2016.v012a005"},{"key":"atypb37","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/16M1109072","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T19:04:47Z","timestamp":1787339087000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/16M1109072"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1137\/16M1109072"],"URL":"https:\/\/doi.org\/10.1137\/16m1109072","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,1]]}}}