{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,3]],"date-time":"2025-11-03T23:00:31Z","timestamp":1762210831378,"version":"3.41.0"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T00:00:00Z","timestamp":1459987200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006769","name":"Russian Science Foundation","doi-asserted-by":"crossref","award":["# 14-50-00005"],"award-info":[{"award-number":["# 14-50-00005"]}],"id":[{"id":"10.13039\/501100006769","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2016,5,4]]},"abstract":"<jats:p>\n            We exhibit an unusually strong tradeoff in propositional proof complexity that significantly deviates from the established pattern of almost all results of this kind. Namely, restrictions on one resource (width, in our case) imply an increase in another resource (tree-like size) that is exponential not only with respect to the complexity of the original problem, but also to the whole class of\n            <jats:italic>all<\/jats:italic>\n            problems of the same bit size. More specifically, we show that for any parameter\n            <jats:italic>k<\/jats:italic>\n            =\n            <jats:italic>k<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            ), there are unsatisfiable\n            <jats:italic>k<\/jats:italic>\n            -CNFs that possess refutations of width\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>k<\/jats:italic>\n            ), but such that any tree-like refutation of width\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>1 \u2212 \u03f5<\/jats:sup>\n            \/\n            <jats:italic>k<\/jats:italic>\n            must necessarily have\n            <jats:italic>doubly<\/jats:italic>\n            exponential size exp\u2009(\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              \u03a9(\n              <jats:italic>k<\/jats:italic>\n              )\n            <\/jats:sup>\n            ). This means that there exist contradictions that allow narrow refutations, but in order to keep the size of such a refutation even within a single exponent, it must necessarily use a high degree of parallelism.\n          <\/jats:p>\n          <jats:p>\n            Our construction and proof methods combine, in a non-trivial way, two previously known techniques: the hardness escalation method based on substitution formulas and expansion. This combination results in a\n            <jats:italic>hardness compression<\/jats:italic>\n            approach that strives to preserve hardness of a contradiction while significantly decreasing the number of its variables.\n          <\/jats:p>","DOI":"10.1145\/2858790","type":"journal-article","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T22:16:10Z","timestamp":1460067370000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["A New Kind of Tradeoffs in Propositional Proof Complexity"],"prefix":"10.1145","volume":"63","author":[{"given":"Alexander","family":"Razborov","sequence":"first","affiliation":[{"name":"University of Chicago, Departments of Mathematics and Computer Science, Chicago IL, USA"}]}],"member":"320","published-online":{"date-parts":[[2016,4,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539701389944"},{"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\/1806689.1806703"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488711"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/080723880"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-004-0036-5"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2012.48"},{"volume-title":"Proceedings of the 40th IEEE FOCS. 422--431","author":"Bonet M.","key":"e_1_2_1_12_1","unstructured":"M. Bonet and N. Galesi . 1999. A study of proof search algorithms for resolution and polynomial calculus . In Proceedings of the 40th IEEE FOCS. 422--431 . M. Bonet and N. Galesi. 1999. A study of proof search algorithms for resolution and polynomial calculus. In Proceedings of the 40th IEEE FOCS. 422--431."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/646336.688272"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213977.2214025"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the International Congress of Mathematicians","author":"Braverman M.","year":"2014","unstructured":"M. Braverman . 2014 . Interactive information and coding theory . In Proceedings of the International Congress of Mathematicians , Seoul 2014. 535--559. M. Braverman. 2014. Interactive information and coding theory. In Proceedings of the International Congress of Mathematicians, Seoul 2014. 535--559."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"volume-title":"Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science. 300--311","author":"Filmus Y.","key":"e_1_2_1_18_1","unstructured":"Y. Filmus , M. Lauria , M. Mik\u0161a , J. Nordstr\u00f6m , and M. Vinyals . 2014. From small space to small width in resolution . In Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science. 300--311 . Y. Filmus, M. Lauria, M. Mik\u0161a, J. Nordstr\u00f6m, and M. Vinyals. 2014. From small space to small width in resolution. In Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science. 300--311."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2014.27"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2009.06.006"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:15)2013"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-011-9356-9"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2858790","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2858790","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:43Z","timestamp":1750225723000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2858790"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,7]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,5,4]]}},"alternative-id":["10.1145\/2858790"],"URL":"https:\/\/doi.org\/10.1145\/2858790","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2016,4,7]]},"assertion":[{"value":"2015-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-04-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}