{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:47Z","timestamp":1750306607116,"version":"3.41.0"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,7,14]],"date-time":"2015-07-14T00:00:00Z","timestamp":1436832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,11,19]]},"abstract":"<jats:p>In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula. Their proof is beautiful but uses a nonconstructive argument based on Ehrenfeucht-Fra\u00efss\u00e9 games. We give an alternative, more explicit, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a \u201cblack-box\u201d technique for proving space lower bounds via a \u201cstatic\u201d complexity measure that works against any resolution refutation\u2014previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.<\/jats:p>","DOI":"10.1145\/2746339","type":"journal-article","created":{"date-parts":[[2015,7,17]],"date-time":"2015-07-17T13:21:25Z","timestamp":1437139285000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["From Small Space to Small Width in Resolution"],"prefix":"10.1145","volume":"16","author":[{"given":"Yuval","family":"Filmus","sequence":"first","affiliation":[{"name":"Institute for Advanced Study, Princeton, NJ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Lauria","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mladen","family":"Mik\u0161a","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Vinyals","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2014.36"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213977.2213999"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488711"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1137\/080723880"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.10089"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2008.42"},{"volume-title":"Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS\u201911)","year":"2011","author":"Ben-Sasson Eli","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422436.2422486"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39206-1_37"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 31st Symposium on Theoretical Aspects of Computer Science (STACS\u201914). Leibniz International Proceedings in Informatics","volume":"25","author":"Filmus Yuval","year":"2014"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2009.06.006"},{"volume-title":"Article 15 (Sept.","year":"2013","author":"Nordstr\u00f6m Jakob","key":"e_1_2_1_20_1"},{"key":"e_1_2_1_21_1","unstructured":"Alexander Razborov. 2014. Personal communication.  Alexander Razborov. 2014. Personal communication."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2746339","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2746339","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:58Z","timestamp":1750227418000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2746339"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,14]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,11,19]]}},"alternative-id":["10.1145\/2746339"],"URL":"https:\/\/doi.org\/10.1145\/2746339","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2015,7,14]]},"assertion":[{"value":"2014-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-07-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}