{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,22]],"date-time":"2026-08-22T08:24:55Z","timestamp":1787387095663,"version":"build-2736575974"},"reference-count":24,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"5","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["(FP7\/2007-2013) 279611"],"award-info":[{"award-number":["(FP7\/2007-2013) 279611"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["(FP7\/2007-2013) 339691"],"award-info":[{"award-number":["(FP7\/2007-2013) 339691"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001824","name":"Grantov\u00c3\u00a1 Agentura \u00c4\u008cesk\u00c3\u00a9 Republiky","doi-asserted-by":"publisher","award":["P202\/12\/G061"],"award-info":[{"award-number":["P202\/12\/G061"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Comput."],"published-print":{"date-parts":[[2016,1]]},"abstract":"<jats:p>We show quadratic lower bounds on the total space used in resolution refutations of random $k$-CNFs over $n$ variables and of the graph pigeonhole principle and the bit pigeonhole principle for $n$ holes. This answers the open problem of whether there are families of $k$-CNF formulas of polynomial size that require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.<\/jats:p>","DOI":"10.1137\/15m1023269","type":"journal-article","created":{"date-parts":[[2016,10,20]],"date-time":"2016-10-20T12:03:09Z","timestamp":1476964989000},"page":"1894-1909","source":"Crossref","is-referenced-by-count":5,"title":["Total Space in Resolution"],"prefix":"10.1137","volume":"45","author":[{"given":"Ilario","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicola","family":"Galesi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Neil","family":"Thapen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2016,10,20]]},"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","unstructured":"E. Ben-Sasson,\n                      Expansion in Proof Complexity\n                      , Ph.D. thesis, Hebrew University, Jerusalem, 2001."},{"key":"atypb4","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.10089"},{"key":"atypb5","unstructured":"E. Ben-Sasson and J. Nordstr\u00f6m,\n                      Understanding space in resolution: Optimal lower bounds and exponential trade-offs\n                      , in Computational Complexity of Discrete Problems, P. B. Miltersen, R. Reischuk, G. Schnitger, and D. van Melkebeek, eds., Dagstuhl Seminar Proceedings, 08381, Schloss Dagstuhl, Leibniz-Zentrum f\u00fcr Informatik, Germany, 2008,http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2008\/1781\/."},{"key":"atypb6","first-page":"47","volume":"16","author":"Ben-Sasson E.","year":"2009","journal-title":"Electronic Colloquium on Computational Complexity"},{"key":"atypb7","unstructured":"E. Ben-Sasson and J. Nordstr\u00f6m,\n                      Understanding space in proof complexity: Separations and trade-offs via substitutions\n                      , in Proceedings of Innovations in Computer Science, ICS 2010, Tsinghua University, Beijing, China, B. Chazelle, ed., Tsinghua University Press, 2011, pp. 401-416,http:\/\/conference.itcs.tsinghua.edu.cn\/ICS2011\/content\/papers\/3.html."},{"key":"atypb8","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"atypb9","unstructured":"P. Bennett, I. Bonacina, N. Galesi, T. Huynh, M. Molloy, and P. Wollan,\n                      Space proof complexity for random 3-CNFs\n                      , CoRR abs\/1503.01613, 2015,https:\/\/arxiv.org\/abs\/1503.01613."},{"key":"atypb10","first-page":"170","author":"Beyersdorff O.","year":"2014","journal-title":"New York"},{"key":"atypb11","unstructured":"I. Bonacina,\n                      Space in Weak Propositional Proof Systems\n                      , Ph.D. thesis, Sapienza University of Rome, Italy, 2015."},{"key":"atypb12","unstructured":"I. Bonacina,\n                      Total space in resolution is at least width squared\n                      , in 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), LIPIcs. Leibniz Int. Proc. Inform 55, I. Chatzigiannakis, M. Mitzenmacher, Y. Rabani, and D. Sangiorgi, eds., Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2016, pp. 56:1-56:13."},{"key":"atypb13","doi-asserted-by":"publisher","DOI":"10.1145\/2699438"},{"key":"atypb14","first-page":"641","author":"Bonacina I.","year":"2014","journal-title":"IEEE Computer Society"},{"key":"atypb15","unstructured":"H. K. B\u00fcning and T. Lettmann,\n                      Propositional Logic-Deduction and Algorithms\n                      , Cambridge University Press, Cambridge, UK, 1999."},{"key":"atypb16","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"atypb17","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.004"},{"key":"atypb18","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"atypb19","doi-asserted-by":"crossref","unstructured":"Y. Filmus, M. Lauria, M. Mik\u0161a, J. Nordstr\u00f6m, and M. Vinyals,\n                      Towards an understanding of polynomial calculus: New separations and lower bounds\n                      , in Proceedings of Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, Part I, F. V. Fomin, R. Freivalds, M. Z. Kwiatkowska, and D. Peleg, eds., Lecture Notes in Comput. Sci. 7965, Springer, New York, 2013, pp. 437-448,https:\/\/doi.org\/10.1007\/978-3-642-39206-1_37.","DOI":"10.1007\/978-3-642-39206-1_37"},{"key":"atypb20","doi-asserted-by":"publisher","DOI":"10.1137\/120895950"},{"key":"atypb21","doi-asserted-by":"publisher","DOI":"10.1137\/060668250"},{"key":"atypb22","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:15)2013"},{"key":"atypb23","doi-asserted-by":"publisher","DOI":"10.1145\/2815493.2815497"},{"key":"atypb24","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2013.v009a014"}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/15M1023269","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T18:18:09Z","timestamp":1787336289000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/15M1023269"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1]]},"references-count":24,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,1]]}},"alternative-id":["10.1137\/15M1023269"],"URL":"https:\/\/doi.org\/10.1137\/15m1023269","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1]]}}}