{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:28:09Z","timestamp":1759638489482,"version":"3.41.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2010,10,1]],"date-time":"2010-10-01T00:00:00Z","timestamp":1285891200000},"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":[[2010,10]]},"abstract":"<jats:p>\n            There are methods to turn short refutations in\n            <jats:italic>polynomial calculus<\/jats:italic>\n            (Pc) and\n            <jats:italic>polynomial calculus with resolution<\/jats:italic>\n            (Pcr) into refutations of low degree. Bonet and Galesi [1999, 2003] asked if such size-degree tradeoffs for Pc [Clegg et al. 1996; Impagliazzo et al. 1999] and Pcr [Alekhnovich et al. 2004] are optimal.\n          <\/jats:p>\n          <jats:p>\n            We answer this question by showing a polynomial encoding of the\n            <jats:italic>graph ordering principle<\/jats:italic>\n            on\n            <jats:italic>m<\/jats:italic>\n            variables which requires Pc and Pcr refutations of degree \u03a9(\u221a\n            <jats:italic>m<\/jats:italic>\n            ). Tradeoff optimality follows from our result and from the short refutations of the graph ordering principle in Bonet and Galesi [1999, 2001].\n          <\/jats:p>\n          <jats:p>\n            We then introduce the algebraic proof system Pcr\n            <jats:italic>\n              <jats:sub>k<\/jats:sub>\n            <\/jats:italic>\n            which combines together polynomial calculus and\n            <jats:italic>k-DNF resolution<\/jats:italic>\n            (Res\n            <jats:italic>\n              <jats:sub>k<\/jats:sub>\n            <\/jats:italic>\n            ). We show a size hierarchy theorem for Pcr\n            <jats:italic>\n              <jats:sub>k<\/jats:sub>\n            <\/jats:italic>\n            : Pcr\n            <jats:italic>\n              <jats:sub>k<\/jats:sub>\n            <\/jats:italic>\n            is exponentially separated from Pcr\n            <jats:italic>\n              <jats:sub>k+1<\/jats:sub>\n            <\/jats:italic>\n            . This follows from the previous degree lower bound and from techniques developed for Res\n            <jats:italic>\n              <jats:sub>k<\/jats:sub>\n            <\/jats:italic>\n            .\n          <\/jats:p>\n          <jats:p>\n            Finally we show that random formulas in conjunctive normal form (3-CNF) are hard to refute in Pcr\n            <jats:italic>\n              <jats:sub>k<\/jats:sub>\n            <\/jats:italic>\n            .\n          <\/jats:p>","DOI":"10.1145\/1838552.1838556","type":"journal-article","created":{"date-parts":[[2010,11,3]],"date-time":"2010-11-03T14:16:37Z","timestamp":1288793797000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Optimality of size-degree tradeoffs for polynomial calculus"],"prefix":"10.1145","volume":"12","author":[{"given":"Nicola","family":"Galesi","sequence":"first","affiliation":[{"name":"Sapienza\u2014Universit\u00e0 di Roma, Rome, Italy"}]},{"given":"Massimo","family":"Lauria","sequence":"additional","affiliation":[{"name":"Sapienza\u2014Universit\u00e0 di Roma, Rome, Italy"}]}],"member":"320","published-online":{"date-parts":[[2010,11,26]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060590.1060628"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539701389944"},{"volume-title":"Proceedings of the 42nd Annual Symposium on Foundations of Computer Science. 190--199","author":"Alekhnovich M.","key":"e_1_2_1_3_1","unstructured":"Alekhnovich , M. and Razborov , A. A . 2001. Lower bounds for polynomial calculus: Non-binomial case . In Proceedings of the 42nd Annual Symposium on Foundations of Computer Science. 190--199 . Alekhnovich, M. and Razborov, A. A. 2001. Lower bounds for polynomial calculus: Non-binomial case. In Proceedings of the 42nd Annual Symposium on Foundations of Computer Science. 190--199."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-73.1.1"},{"key":"e_1_2_1_5_1","unstructured":"Beame P. and Pitassi T. 2001. Propositional proof complexity: Past present and future. In Current Trends in Theoretical Computer Science: Entering the 21st Century. 42--70.   Beame P. and Pitassi T. 2001. Propositional proof complexity: Past present and future. In Current Trends in Theoretical Computer Science: Entering the 21st Century. 42--70."},{"volume-title":"Proceedings of the 40th Annual Symposium on Foundations of Computer Science. 415--421","author":"Ben-Sasson E.","key":"e_1_2_1_6_1","unstructured":"Ben-Sasson , E. and Impagliazzo , R . 1999. Random CNF's are hard for the polynomial calculus . In Proceedings of the 40th Annual Symposium on Foundations of Computer Science. 415--421 . Ben-Sasson, E. and Impagliazzo, R. 1999. Random CNF's are hard for the polynomial calculus. In Proceedings of the 40th Annual Symposium on Foundations of Computer Science. 415--421."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/301250.301392"},{"volume-title":"Proceedings of the 40th Annual Symposium on Foundations of Computer Science. 422--432","author":"Bonet M. L.","key":"e_1_2_1_8_1","unstructured":"Bonet , M. L. and Galesi , N . 1999. A study of proof search algorithms for resolution and polynomial calculus . In Proceedings of the 40th Annual Symposium on Foundations of Computer Science. 422--432 . Bonet, M. L. and Galesi, N. 1999. A study of proof search algorithms for resolution and polynomial calculus. In Proceedings of the 40th Annual Symposium on Foundations of Computer Science. 422--432."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370100000"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001530200141"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1726"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_2_1_14_1","volume-title":"An Introduction to Computational Algebraic Geometry and Commutative Algebra","author":"Cox D.","unstructured":"Cox , D. , Little , J. , and O'Shea , D. 2007. Ideals , Varieties, and Algorithms : An Introduction to Computational Algebraic Geometry and Commutative Algebra 3 rd Ed. Springer . Cox, D., Little, J., and O'Shea, D. 2007. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra 3rd Ed. Springer.","edition":"3"},{"key":"e_1_2_1_15_1","unstructured":"Galesi N. and Lauria M. 2007. Extending polynomial calculus to k- DNF resolution. ECCC TR Series. TR07-41. www.eccc.hpi-web.de\/report\/2007\/041\/.  Galesi N. and Lauria M. 2007. Extending polynomial calculus to k- DNF resolution. ECCC TR Series. TR07-41. www.eccc.hpi-web.de\/report\/2007\/041\/."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0273-0979-06-01126-8"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"e_1_2_1_19_1","first-page":"253","article-title":"Short proofs for tricky formulas","volume":"22","author":"Krishnamurty B.","year":"1985","unstructured":"Krishnamurty , B. 1985 . Short proofs for tricky formulas . Acta Inform. 22 , 253 -- 257 . Krishnamurty, B. 1985. Short proofs for tricky formulas. Acta Inform. 22, 253--257.","journal-title":"Acta Inform."},{"key":"e_1_2_1_20_1","unstructured":"Razborov A. 2003. Pseudorandom generators hard for k-dnf resolution and polynomial calculus resolution. Manuscript availbale at author's Web page.  Razborov A. 2003. Pseudorandom generators hard for k-dnf resolution and polynomial calculus resolution. Manuscript availbale at author's Web page."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050013"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2307\/3062153"},{"key":"e_1_2_1_23_1","first-page":"482","article-title":"The complexity of propositional proofs","volume":"13","author":"Segerlind N.","year":"2006","unstructured":"Segerlind , N. 2006 . The complexity of propositional proofs . Bull. Symbol. Log. 13 , 4, 482 -- 537 . Segerlind, N. 2006. The complexity of propositional proofs. Bull. Symbol. Log. 13, 4, 482--537.","journal-title":"Bull. Symbol. Log."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703428555"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050044"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the International Congress of Mathematicians (ICM).","volume":"1","author":"Wigderson A.","year":"2006","unstructured":"Wigderson , A. 2006 . P, NP and mathematics\u2014a computational complexity perspective . In Proceedings of the International Congress of Mathematicians (ICM). Vol. 1 , 665--712. Wigderson, A. 2006. P, NP and mathematics\u2014a computational complexity perspective. In Proceedings of the International Congress of Mathematicians (ICM). Vol. 1, 665--712."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1838552.1838556","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1838552.1838556","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:41:11Z","timestamp":1750250471000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1838552.1838556"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,10]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,10]]}},"alternative-id":["10.1145\/1838552.1838556"],"URL":"https:\/\/doi.org\/10.1145\/1838552.1838556","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2010,10]]},"assertion":[{"value":"2008-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-11-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}