{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,22]],"date-time":"2026-08-22T09:02:07Z","timestamp":1787389327443,"version":"build-2736575974"},"reference-count":55,"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":[[2009,1]]},"abstract":"<jats:p>The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory. Both of these measures have previously been studied and related to the resolution refutation size of unsatisfiable conjunctive normal form (CNF) formulas. Also, the minimum refutation space of a formula has been proven to be at least as large as the minimum refutation width, but it has been open whether space can be separated from width or the two measures coincide asymptotically. We prove that there is a family of k-CNF formulas for which the refutation width in resolution is constant but the refutation space is nonconstant, thus solving a problem mentioned in several previous papers.<\/jats:p>","DOI":"10.1137\/060668250","type":"journal-article","created":{"date-parts":[[2009,5,29]],"date-time":"2009-05-29T12:34:17Z","timestamp":1243600457000},"page":"59-121","source":"Crossref","is-referenced-by-count":22,"title":["Narrow Proofs May Be Spacious:Separating Space and Width in Resolution"],"prefix":"10.1137","volume":"39","author":[{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2009,5,28]]},"reference":[{"key":"R1","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(86)90060-9"},{"key":"R2","doi-asserted-by":"crossref","unstructured":"M. Alekhnovich,\n                      \n                        Lower bounds for\n                        k\n                        -DNF resolution on random\n                      \n                      3\n                      -CNFs\n                      , in Proceedings of the 37th Annual ACM Symposium on Theory of Computing (STOC '05), ACM, New York, 2005, pp. 251\u2013256.","DOI":"10.1145\/1060590.1060628"},{"key":"R3","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"R4","doi-asserted-by":"crossref","unstructured":"M. Alekhnovich, J. Johannsen, T. Pitassi, and A. Urquhart,\n                      An exponential separation between regular and general resolution\n                      , in Proceedings of the 34th Annual ACM Symposium on Theory of Computing (STOC '02), ACM, New York, 2002, pp. 448\u2013456.","DOI":"10.1145\/509907.509974"},{"key":"R5","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.10.004"},{"key":"R6","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3114"},{"key":"R7","doi-asserted-by":"crossref","unstructured":"A. Atserias and V. Dalmau,\n                      A combinatorical characterization of resolution width\n                      , in Proceedings of the 18th IEEE Annual Conference on Computational Complexity (CCC '03), IEEE Computer Society, Los Alamitos, CA, 2003, pp. 239\u2013247.","DOI":"10.1109\/CCC.2003.1214424"},{"key":"R8","first-page":"190","volume":"74","author":"Baumer S.","year":"2001","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci. EATCS"},{"key":"R9","doi-asserted-by":"crossref","unstructured":"P. Beame,\n                      Proof complexity\n                      , in Computational Complexity Theory, IAS\/Park City Mathematics Series 10, S. Rudich and A. Wigderson, eds., AMS, Providence, RI, 2004, pp. 199\u2013246.","DOI":"10.1090\/pcms\/010\/07"},{"key":"R10","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700369156"},{"key":"R11","doi-asserted-by":"crossref","unstructured":"P. Beame and T. Pitassi,\n                      Simplified and improved resolution lower bounds\n                      , in Proceedings of the 37th Annual IEEE Symposium on Foundations of Computer Science (FOCS '96), IEEE Computer Society, Los Alamitos, CA, 1996, pp. 274\u2013282.","DOI":"10.1109\/SFCS.1996.548486"},{"key":"R12","first-page":"66","volume":"65","author":"Beame P.","year":"1998","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci. EATCS"},{"key":"R13","doi-asserted-by":"crossref","unstructured":"E. Ben-Sasson,\n                      Size space tradeoffs for resolution\n                      , in Proceedings of the 34th Annual ACM Symposium on Theory of Computing (STOC '02), ACM, New York, 2002, pp. 457\u2013464.","DOI":"10.1145\/509907.509975"},{"key":"R14","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.10089"},{"key":"R15","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-004-0036-5"},{"key":"R16","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"R17","unstructured":"A. Blake,\n                      Canonical Expressions in Boolean Algebra\n                      , Ph.D. thesis, University of Chicago, Chicago, IL, 1937."},{"key":"R18","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"R19","doi-asserted-by":"publisher","DOI":"10.1007\/s000370100000"},{"key":"R20","doi-asserted-by":"crossref","unstructured":"J. Buresh-Oppenheim and T. Pitassi,\n                      The complexity of resolution refinements\n                      , in Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 03), IEEE Computer Society, Los Alamitos, CA, 2003, pp. 138\u2013147.","DOI":"10.1109\/LICS.2003.1210053"},{"key":"R21","unstructured":"S. R. Buss, ed.\n                      Handbook of Proof Theory\n                      , Elsevier Science, Amsterdam, 1998."},{"key":"R22","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90072-2"},{"key":"R23","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"R24","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"R25","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(76)80048-7"},{"key":"R26","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"R27","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"R28","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.004"},{"key":"R29","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"R30","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(03)00345-4"},{"key":"R31","doi-asserted-by":"publisher","DOI":"10.1137\/0206031"},{"key":"R32","unstructured":"J. R. Gilbert and R. E. Tarjan,\n                      Variations of a Pebble Game on Graphs\n                      , Tech. report STAN-CS-78-661, Stanford University, Stanford, CA, 1978, available at http:\/\/infolab.stanford. edu\/TR\/CS-TR-78-661.html."},{"key":"R33","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"R34","doi-asserted-by":"publisher","DOI":"10.1145\/322003.322015"},{"key":"R35","doi-asserted-by":"publisher","DOI":"10.1145\/2455.214115"},{"key":"R36","unstructured":"H. Kleine B\u00fcning and T. Letterman,\n                      Propositional Logic: Deduction and Algorithms\n                      , Cambridge University Press, Cambridge, UK, 1999."},{"key":"R37","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"R38","doi-asserted-by":"crossref","unstructured":"O. Kullmann,\n                      An application of matroid theory to the SAT problem\n                      , in Proceedings of the 15th Annual IEEE Conference on Computational Complexity (CCC '00), IEEE Computer Society, Los Alamitos, CA, 2000, pp. 116\u2013124.","DOI":"10.1109\/CCC.2000.856741"},{"key":"R39","doi-asserted-by":"crossref","unstructured":"T. Lengauer and R. E. Tarjan,\n                      Upper and lower bounds on time-space tradeoffs\n                      , in Proceedings of the 11th Annual ACM Symposium on Theory of Computing (STOC '79), ACM, New York, 1979, pp. 262\u2013277.","DOI":"10.1145\/800135.804420"},{"key":"R40","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(80)90136-2"},{"key":"R41","unstructured":"J. Nordstr\u00f6m,\n                      Narrow Proofs May Be Spacious: Separating Space and Width in Resolution\n                      , Tech. report TR05-066, Revision 02, Electronic Colloquium on Computational Complexity (ECCC), 2005."},{"key":"R42","doi-asserted-by":"crossref","unstructured":"J. Nordstr\u00f6m and J. H\u00c5stad,\n                      Towards an optimal separation of space and length in resolution (extended abstract)\n                      , in Proceedings of the 40th Annual ACM Symposium on Theory of Computing (STOC '08), ACM, New York, 2008, to appear.","DOI":"10.1145\/1374376.1374478"},{"key":"R43","unstructured":"N. Pippenger,\n                      Pebbling\n                      , Tech. report RC8258, IBM Watson Research Center, 1980, appeared in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer Science, Japan, 1980, pp. 1\u201319."},{"key":"R44","doi-asserted-by":"publisher","DOI":"10.1145\/972639.972640"},{"key":"R45","doi-asserted-by":"publisher","DOI":"10.1007\/s004930050062"},{"key":"R46","unstructured":"A. A. Razborov,\n                      \n                        Pseudorandom Generators Hard for\n                        k\n                        -DNF Resolution and Polynomial Calculus Resolution\n                      \n                      , manuscript, 2003, available at http:\/\/www.mi.ras.ru\/$\\!_{^{\\sim}}\\!$*.5ptrazborov\/."},{"key":"R47","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00453-X"},{"key":"R48","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2004.01.004"},{"key":"R49","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"R50","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703428555"},{"key":"R51","doi-asserted-by":"crossref","unstructured":"J. Tor\u00e1n,\n                      Lower bounds for space in resolution\n                      , in Proceedings of the 13th International Workshop on Computer Science Logic (CSL '99), Lecture Notes in Comput. Sci. 1683, Springer-Verlag, New York, 1999, pp. 362\u2013373.","DOI":"10.1007\/3-540-48168-0_26"},{"key":"R52","first-page":"86","volume":"83","author":"Tor\u00e1n J.","year":"2004","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci. EATCS"},{"key":"R53","doi-asserted-by":"crossref","unstructured":"G. Tseitin,\n                      On the complexity of derivation in propositional calculus\n                      , in Structures in Constructive Mathematics and Mathematical Logic, Part II, A. O. Silenko, ed., Consultants Bureau, New York, London, 1968, pp. 115\u2013125.","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"R54","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"},{"key":"R55","doi-asserted-by":"publisher","DOI":"10.2307\/421131"}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/060668250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T18:19:42Z","timestamp":1787336382000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/060668250"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":55,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["10.1137\/060668250"],"URL":"https:\/\/doi.org\/10.1137\/060668250","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1]]}}}