{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:58:36Z","timestamp":1781078316448,"version":"3.54.1"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T00:00:00Z","timestamp":1605571200000},"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":["J. ACM"],"published-print":{"date-parts":[[2021,2,28]]},"abstract":"<jats:p>We prove that a small-depth Frege refutation of the Tseitin contradiction on the grid requires subexponential size. We conclude that polynomial size Frege refutations of the Tseitin contradiction must use formulas of almost logarithmic depth.<\/jats:p>","DOI":"10.1145\/3425606","type":"journal-article","created":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T03:07:47Z","timestamp":1606273667000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["On Small-depth Frege Proofs for Tseitin for Grids"],"prefix":"10.1145","volume":"68","author":[{"given":"Johan","family":"H\u00e5stad","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01302964"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/0221068"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-002-0172-5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273826"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746539.2746551"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01744431"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/12130.12132"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"key":"e_1_2_1_12_1","unstructured":"J. Mehta. 2017. Tree tribes and lower bounds for switching lemmas. Retrieved from http:\/\/arxiv.org\/abs\/1703.00043.  J. Mehta. 2017. Tree tribes and lower bounds for switching lemmas. Retrieved from http:\/\/arxiv.org\/abs\/1703.00043."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897518.2897637"},{"key":"e_1_2_1_15_1","unstructured":"A. Razborov. 1988. Bounded-depth formulae over the basis AND XOR and some combintorial problems (in Russian). Problems of Cybernetics. Complexity Theory and Applied Mathematical Logic. 149--166.  A. Razborov. 1988. Bounded-depth formulae over the basis AND XOR and some combintorial problems (in Russian). Problems of Cybernetics. Complexity Theory and Applied Mathematical Logic. 149--166."},{"key":"e_1_2_1_16_1","volume-title":"Bounded Arithmetic and Lower Bounds in Boolean Complexity","author":"Razborov A. A.","unstructured":"A. A. Razborov . 1995. Bounded Arithmetic and Lower Bounds in Boolean Complexity . Birkh\u00e4user , Boston, MA , 344--386. Peter Clote and Jeffrey Remmel (Eds.). A. A. Razborov. 1995. Bounded Arithmetic and Lower Bounds in Boolean Complexity. Birkh\u00e4user, Boston, MA, 344--386. Peter Clote and Jeffrey Remmel (Eds.)."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2015.67"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808733"},{"key":"e_1_2_1_19_1","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part II","author":"Tseitin G. S.","unstructured":"G. S. Tseitin . 1968. On the complexity of derivation in the proposistional calculus . In Studies in Constructive Mathematics and Mathematical Logic, Part II , A. O. Slisenko (Ed.), Springer . G. S. Tseitin. 1968. On the complexity of derivation in the proposistional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part II, A. O. Slisenko (Ed.), Springer."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1040046140"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.49"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3425606","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3425606","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:55Z","timestamp":1750195915000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3425606"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,17]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,2,28]]}},"alternative-id":["10.1145\/3425606"],"URL":"https:\/\/doi.org\/10.1145\/3425606","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,17]]},"assertion":[{"value":"2017-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-11-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}