{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T04:48:07Z","timestamp":1769748487672,"version":"3.49.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T00:00:00Z","timestamp":1674000000000},"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":[[2023,1,31]]},"abstract":"<jats:p>\n            We study the MaxSAT Resolution (MaxRes) rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weakening (the system MaxResW),\n            <jats:italic>p<\/jats:italic>\n            -simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and not merely inheriting lower bounds from Res), we define a new proof system called the SubCubeSums proof system. This system, which\n            <jats:italic>p<\/jats:italic>\n            -simulates MaxResW, can be viewed as a special case of the semi-algebraic Sherali\u2013Adams proof system. In expressivity, it is the integral restriction of conical juntas studied in the contexts of communication complexity and extension complexity. We show that it is not simulated by Res. Using a proof technique qualitatively different from the lower bounds that MaxResW inherits from Res, we show that Tseitin contradictions on expander graphs are hard to refute in SubCubeSums. We also establish a lower bound technique via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums.\n          <\/jats:p>","DOI":"10.1145\/3565363","type":"journal-article","created":{"date-parts":[[2022,10,17]],"date-time":"2022-10-17T13:09:26Z","timestamp":1666012166000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["MaxSAT Resolution and Subcube Sums"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1739-0872","authenticated-orcid":false,"given":"Yuval","family":"Filmus","sequence":"first","affiliation":[{"name":"Technion \u2013 Israel Institute of Technology, Haifa, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9116-4398","authenticated-orcid":false,"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[{"name":"The Institute of Mathematical Sciences (CI of HomiBhabha National Institute), Taramani, India"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6501-6589","authenticated-orcid":false,"given":"Gaurav","family":"Sood","sequence":"additional","affiliation":[{"name":"The Institute of Mathematical Sciences (CI of HomiBhabha National Institute), Taramani, India"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1487-445X","authenticated-orcid":false,"given":"Marc","family":"Vinyals","sequence":"additional","affiliation":[{"name":"Technion \u2013 Israel Institute of Technology, Haifa, Israel"}]}],"member":"320","published-online":{"date-parts":[[2023,1,18]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090"},{"key":"e_1_3_2_3_2","volume-title":"Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs","author":"Atserias Albert","year":"2018","unstructured":"Albert Atserias and Tuomas Hakoniemi. 2018. Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs. Technical Report 1811.01351. arXiv.org."},{"key":"e_1_3_2_4_2","first-page":"24:1\u201324:20","volume-title":"Proceedings of the 34th Computational Complexity Conference (CCC\u201919)","author":"Atserias Albert","year":"2019","unstructured":"Albert Atserias and Tuomas Hakoniemi. 2019. Size-degree trade-offs for sums-of-squares and positivstellensatz proofs. In Proceedings of the 34th Computational Complexity Conference (CCC\u201919). 24:1\u201324:20."},{"key":"e_1_3_2_5_2","first-page":"1","volume-title":"Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT\u201919)","author":"Atserias Albert","year":"2019","unstructured":"Albert Atserias and Massimo Lauria. 2019. Circular (yet sound) proofs. In Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT\u201919). 1\u201318."},{"key":"e_1_3_2_6_2","first-page":"286","volume-title":"Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC\u201914)","author":"Atserias Albert","year":"2014","unstructured":"Albert Atserias, Massimo Lauria, and Jakob Nordstr\u00f6m. 2014. Narrow proofs may be maximally long. In Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC\u201914). 286\u2013297."},{"issue":"3","key":"e_1_3_2_7_2","first-page":"19","article-title":"Narrow proofs may be maximally long","volume":"17","author":"Atserias Albert","year":"2016","unstructured":"Albert Atserias, Massimo Lauria, and Jakob Nordstr\u00f6m. 2016. Narrow proofs may be maximally long. ACM Transactions on Computational Logic 17, 3, Article 19 (May2016), 19:1\u201319:30.Preliminary version in CCC\u201914.","journal-title":"ACM Transactions on Computational Logic"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1137\/080723880"},{"issue":"4","key":"e_1_3_2_9_2","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/s00493-004-0036-5","article-title":"Near optimal separation of tree-like and general resolution","volume":"24","author":"Ben-Sasson Eli","year":"2004","unstructured":"Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. 2004. Near optimal separation of tree-like and general resolution. Combinatorica 24, 4 (Sept.2004), 585\u2013603.","journal-title":"Combinatorica"},{"issue":"2","key":"e_1_3_2_10_2","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1145\/375827.375835","article-title":"Short proofs are narrow\u2014resolution made simple","volume":"48","author":"Ben-Sasson Eli","year":"2001","unstructured":"Eli Ben-Sasson and Avi Wigderson. 2001. Short proofs are narrow\u2014resolution made simple. J. ACM 48, 2 (March2001), 149\u2013169. Preliminary version in STOC\u201999.","journal-title":"J. ACM"},{"key":"e_1_3_2_11_2","first-page":"11:1\u201311:14","volume-title":"Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS\u201918) (Leibniz International Proceedings in Informatics (LIPIcs))","volume":"96","author":"Berkholz Christoph","year":"2018","unstructured":"Christoph Berkholz. 2018. The relation between polynomial calculus, Sherali-Adams, and sum-of-squares proofs. In Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS\u201918) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 96. 11:1\u201311:14."},{"key":"e_1_3_2_12_2","volume-title":"Canonical expressions in Boolean algebra","author":"Blake Archie","year":"1937","unstructured":"Archie Blake. 1937. Canonical expressions in Boolean algebra. Ph.D. Dissertation. University of Chicago."},{"key":"e_1_3_2_13_2","first-page":"6565","volume-title":"Proceedings of the 32nd AAAI Conference on Artificial Intelligence, (AAAI\u201918)","author":"Bonet Maria Luisa","year":"2018","unstructured":"Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Jo\u00e3o Marques-Silva, and Ant\u00f3nio Morgado. 2018. MaxSAT resolution with the dual rail encoding. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence, (AAAI\u201918). 6565\u20136572."},{"key":"e_1_3_2_14_2","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/978-3-030-51825-7_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"Bonet Maria Luisa","year":"2020","unstructured":"Maria Luisa Bonet and Jordi Levy. 2020. Equivalence between systems stronger than resolution. In Theory and Applications of Satisfiability Testing \u2013 SAT 2020, Luca Pulina and Martina Seidl (Eds.). Springer International Publishing, 166\u2013181."},{"issue":"8","key":"e_1_3_2_15_2","doi-asserted-by":"crossref","first-page":"606","DOI":"10.1016\/j.artint.2007.03.001","article-title":"Resolution for Max-SAT","volume":"171","author":"Bonet Mar\u00eda Luisa","year":"2007","unstructured":"Mar\u00eda Luisa Bonet, Jordi Levy, and Felip Many\u00e0. 2007. Resolution for Max-SAT. Artificial Intelligence 171, 8 (2007), 606\u2013618.","journal-title":"Artificial Intelligence"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(74)80046-2"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_3_2_18_2","first-page":"69:1\u201369:25","volume-title":"Proceedings of the 13th Annual Innovations in Theoretical Computer Science Conference, ITCS 2022, (LIPIcs)","volume":"215","author":"Fleming Noah","year":"2022","unstructured":"Noah Fleming, Mika G\u00f6\u00f6s, Stefan Grosser, and Robert Robere. 2022. On semi-algebraic proofs and algorithms. In Proceedings of the 13th Annual Innovations in Theoretical Computer Science Conference, ITCS 2022, (LIPIcs), (January 31 - February 3, 2022, Berkeley, CA), Mark Braverman (Ed.), Vol. 215. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 69:1\u201369:25. DOI:10.4230\/LIPIcs.ITCS.2022.69"},{"issue":"1","key":"e_1_3_2_19_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1561\/0400000086","article-title":"Semialgebraic proofs and efficient algorithm design","volume":"14","author":"Fleming Noah","year":"2019","unstructured":"Noah Fleming, Pravesh Kothari, and Toniann Pitassi. 2019. Semialgebraic proofs and efficient algorithm design. Foundations and Trends in Theoretical Computer Science 14, 1-2 (2019), 1\u2013221.","journal-title":"Foundations and Trends in Theoretical Computer Science"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2205.02168."},{"key":"e_1_3_2_21_2","first-page":"419","volume-title":"Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS\u201902) (Lecture Notes in Computer Science)","volume":"2285","author":"Grigoriev Dima","year":"2002","unstructured":"Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. 2002. Complexity of semi-algebraic proofs. In Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS\u201902) (Lecture Notes in Computer Science), Vol. 2285. Springer, 419\u2013430."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1137\/16M109884X"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1137\/15M103145X"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_3_2_25_2","first-page":"164","volume-title":"Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201917)","author":"Ignatiev Alexey","year":"2017","unstructured":"Alexey Ignatiev, Ant\u00f3nio Morgado, and Joao Marques-Silva. 2017. On tackling the limits of resolution in SAT solving. In Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201917). 164\u2013183."},{"key":"e_1_3_2_26_2","first-page":"29","volume-title":"Structure in Complexity Theory Conference","author":"Iwama Kazuo","year":"1995","unstructured":"Kazuo Iwama and Eiji Miyano. 1995. Intractability of read-once resolution. In Structure in Complexity Theory Conference. IEEE Computer Society, 29\u201336."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24508-4"},{"issue":"2","key":"e_1_3_2_28_2","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1016\/j.artint.2007.05.006","article-title":"A logical approach to efficient Max-SAT solving","volume":"172","author":"Larrosa Javier","year":"2008","unstructured":"Javier Larrosa, Federico Heras, and Simon de Givry. 2008. A logical approach to efficient Max-SAT solving. Artifical Intelligence 172, 2-3 (2008), 204\u2013233.","journal-title":"Artifical Intelligence"},{"key":"e_1_3_2_29_2","volume-title":"Proceedings of the 34th AAAI Conference on Artificial Intelligence","author":"Larrosa Javier","year":"2020","unstructured":"Javier Larrosa and Emma Rollon. 2020. Augmenting the power of (partial) MaxSAT resolution with extension. In Proceedings of the 34th AAAI Conference on Artificial Intelligence."},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/978-3-030-51825-7_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"Larrosa Javier","year":"2020","unstructured":"Javier Larrosa and Emma Rollon. 2020. Towards a better understanding of (partial weighted) MaxSAT proof systems. In Theory and Applications of Satisfiability Testing \u2013 SAT 2020, Luca Pulina and Martina Seidl (Eds.). Springer International Publishing, 218\u2013232."},{"issue":"3","key":"e_1_3_2_31_2","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1007\/s00037-017-0152-4","article-title":"Tight size-degree bounds for sums-of-squares proofs","volume":"26","author":"Lauria Massimo","year":"2017","unstructured":"Massimo Lauria and Jakob Nordstr\u00f6m. 2017. Tight size-degree bounds for sums-of-squares proofs. Computational Complexity 26, 3 (Dec.2017), 911\u2013948. Preliminary version in CCC\u201915.","journal-title":"Computational Complexity"},{"key":"e_1_3_2_32_2","first-page":"50:1\u201350:19","volume-title":"Proceedings of the 36th Symposium on Theoretical Aspects of Computer Science (STACS\u201919)","author":"Loff Bruno","year":"2019","unstructured":"Bruno Loff and Sagnik Mukhopadhyay. 2019. Lifting theorems for equality. In Proceedings of the 36th Symposium on Theoretical Aspects of Computer Science (STACS\u201919). 50:1\u201350:19."},{"key":"e_1_3_2_33_2","first-page":"681","volume-title":"Proceedings of the 18th EPIA Conference on Artificial Intelligence","author":"Marques-Silva Joao","year":"2017","unstructured":"Joao Marques-Silva, Alexey Ignatiev, and Ant\u00f3nio Morgado. 2017. Horn maximum satisfiability: Reductions, algorithms and applications. In Proceedings of the 18th EPIA Conference on Artificial Intelligence. 681\u2013694."},{"key":"e_1_3_2_34_2","first-page":"121","volume-title":"Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914)","author":"Mik\u0161a Mladen","year":"2014","unstructured":"Mladen Mik\u0161a and Jakob Nordstr\u00f6m. 2014. Long proofs of (seemingly) simple formulas. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914). 121\u2013137."},{"key":"e_1_3_2_35_2","first-page":"2717","volume-title":"Proceedings of the 28th AAAI Conference on Artificial Intelligence","author":"Narodytska Nina","year":"2014","unstructured":"Nina Narodytska and Fahiem Bacchus. 2014. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of the 28th AAAI Conference on Artificial Intelligence. 2717\u20132723."},{"key":"e_1_3_2_36_2","first-page":"128","volume-title":"Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA\u201900)","author":"Pudl\u00e1k Pavel","year":"2000","unstructured":"Pavel Pudl\u00e1k and Russell Impagliazzo. 2000. A lower bound for DLL algorithms for k-SAT (preliminary version). In Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA\u201900). 128\u2013136."},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson John Alan","year":"1965","unstructured":"John Alan Robinson. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12 (1965), 23\u201341.","journal-title":"J. ACM"},{"key":"e_1_3_2_38_2","first-page":"1.2","article-title":"SGEN1: A generator of small but difficult satisfiability benchmarks","volume":"15","author":"Spence Ivor","year":"2010","unstructured":"Ivor Spence. 2010. SGEN1: A generator of small but difficult satisfiability benchmarks. Journal of Experimental Algorithmics 15, Article 1.2 (March2010), 1.2:1\u20131.2:15 pages.","journal-title":"Journal of Experimental Algorithmics"},{"issue":"1","key":"e_1_3_2_39_2","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","article-title":"Hard examples for resolution","volume":"34","author":"Urquhart Alasdair","year":"1987","unstructured":"Alasdair Urquhart. 1987. Hard examples for resolution. J. ACM 34, 1 (Jan.1987), 209\u2013219.","journal-title":"J. ACM"},{"issue":"4","key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2307\/421131","article-title":"The complexity of propositional proofs","volume":"1","author":"Urquhart Alasdair","year":"1995","unstructured":"Alasdair Urquhart. 1995. The complexity of propositional proofs. Bulletin of Symbolic Logic 1, 4 (1995), 425\u2013467.","journal-title":"Bulletin of Symbolic Logic"},{"key":"e_1_3_2_41_2","first-page":"388","volume-title":"Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201910)","author":"Gelder Allen Van","year":"2010","unstructured":"Allen Van Gelder and Ivor Spence. 2010. Zero-one designs produce small hard SAT instances. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201910). 388\u2013397."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3565363","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3565363","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:12Z","timestamp":1750178232000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3565363"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,18]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3565363"],"URL":"https:\/\/doi.org\/10.1145\/3565363","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,18]]},"assertion":[{"value":"2020-09-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-08-05","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}