{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T14:45:29Z","timestamp":1787496329400,"version":"build-2736575974"},"publisher-location":"New York, NY, USA","reference-count":64,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,15]],"date-time":"2021-06-15T00:00:00Z","timestamp":1623715200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004063","name":"Knut och Alice Wallenbergs Stiftelse","doi-asserted-by":"publisher","award":["2018.0371"],"award-info":[{"award-number":["2018.0371"]}],"id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["1900460"],"award-info":[{"award-number":["1900460"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6,15]]},"DOI":"10.1145\/3406325.3451080","type":"proceedings-article","created":{"date-parts":[[2021,6,15]],"date-time":"2021-06-15T21:26:13Z","timestamp":1623792373000},"page":"209-222","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Automating algebraic proof systems is NP-hard"],"prefix":"10.1145","author":[{"given":"Susanna F.","family":"de Rezende","sequence":"first","affiliation":[{"name":"Czech Academy of Sciences, Czechia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mika","family":"G\u00f6\u00f6s","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[{"name":"University of Copenhagen, Denmark \/ Lund University, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Toniann","family":"Pitassi","sequence":"additional","affiliation":[{"name":"University of Toronto, Canada \/ Institute for Advanced Study at Princeton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert","family":"Robere","sequence":"additional","affiliation":[{"name":"McGill University, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dmitry","family":"Sokolov","sequence":"additional","affiliation":[{"name":"St. Petersburg State University, Russia \/ Russian Academy of Sciences, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,6,15]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2307\/2694916"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1137\/06066850X"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.10.004"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CCC.2019.24"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409472"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746539.2746605"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence (AAAI). Pages 203\u2013208","author":"Bayardo Roberto J.","unstructured":"Roberto J. Bayardo Jr. and Robert Schrag. 1997. Using CSP Look-Back Techniques to Solve Real-World SAT Instances. In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI). Pages 203\u2013208."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1575"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365714"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1410"},{"key":"e_1_3_2_1_13_1","unstructured":"Zo\u00eb Bell. 2020. Automating Regular or Ordered Resolution is NP-Hard. https:\/\/eccc.weizmann.ac.il\/report\/2020\/105\/"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2018.11"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-004-0183-5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370100000"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1997.646114"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539798353230"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-002-0171-6"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1726"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45220-1_14"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/focs46700.2020.00011"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2016.40"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000086"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-009-9195-5"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838556"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188745.3188838"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS.2019.37"},{"key":"e_1_3_2_1_31_1","unstructured":"Michal Garl\u00edk. 2020. Failure of Feasible Disjunction Property for k-DNF Resolution and NP-hardness of Automating It. https:\/\/eccc.weizmann.ac.il\/report\/2020\/037\/"},{"key":"e_1_3_2_1_32_1","unstructured":"Konstantinos Georgiou and Avner Magen. 2008. Limitations of the Sherali-Adams lift and project system: Compromising local and global arguments. http:\/\/www.cs.utoronto.ca\/pub\/reports\/csrg\/587\/CSRG-587.pdf"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITCS.2019.38"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357713.3384248"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1137\/16M1082007"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2017.72"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213977.2214000"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Kazuo Iwama. 1997. Complexity of finding short resolution proofs. In Mathematical Foundations of Computer Science (MFCS). Pages 309\u2013318. https:\/\/doi.org\/10.1007\/BFb0029974 10.1007\/BFb0029974","DOI":"10.1007\/BFb0029974"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom"},{"key":"e_1_3_2_1_41_1","volume-title":"Boolean Function Complexity: Advances and Frontiers. Algorithms and Combinatorics. 27","author":"Jukna Stasys","unstructured":"Stasys Jukna. 2012. Boolean Function Complexity: Advances and Frontiers. Algorithms and Combinatorics. 27, Springer."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188745.3188970"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2674"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45535-3_23"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CCC.2017.2"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-017-0152-4"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2016.54"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.84"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITCS.2017.59"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CCC.2019.8"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973105.111"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80063-7"},{"key":"e_1_3_2_1_55_1","unstructured":"Pablo Parrilo. 2000. Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1137\/100816833"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CCC.2020.38"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.2307\/2589349"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00411-5"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-019-00182-7"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2017.80"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050013"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(92)00190-W"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01074929"}],"event":{"name":"STOC '21: 53rd Annual ACM SIGACT Symposium on Theory of Computing","location":"Virtual Italy","acronym":"STOC '21","sponsor":["SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406325.3451080","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406325.3451080","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406325.3451080","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:24:53Z","timestamp":1750181093000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406325.3451080"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,15]]},"references-count":64,"alternative-id":["10.1145\/3406325.3451080","10.1145\/3406325"],"URL":"https:\/\/doi.org\/10.1145\/3406325.3451080","relation":{},"subject":[],"published":{"date-parts":[[2021,6,15]]},"assertion":[{"value":"2021-06-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}