{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,11]],"date-time":"2024-07-11T15:59:05Z","timestamp":1720713545874},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,12,20]],"date-time":"2018-12-20T00:00:00Z","timestamp":1545264000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/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":[[2019,1,31]]},"abstract":"We analyze how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semialgebraic proof systems, the classical constructions of pp-interpretability, homomorphic equivalence, and addition of constants to a core preserve the proof complexity of the CSP. As a result, for those proof systems, the classes of constraint languages for which small unsatisfiability certificates exist can be characterized algebraically. We illustrate our results by a gap theorem saying that a constraint language either has resolution refutations of constant width or does not have bounded-depth Frege refutations of subexponential size. The former holds exactly for the widely studied class of constraint languages of bounded width. This class is also known to coincide with the class of languages with refutations of sublinear degree in Sums of Squares and Polynomial Calculus over the real field, for which we provide alternative proofs. We then ask for the existence of a natural proof system with good behavior with respect to reductions and simultaneously small-size refutations beyond bounded width. We give an example of such a proof system by showing that bounded-degree Lov\u00e1sz-Schrijver satisfies both requirements. Finally, building on the known lower bounds, we demonstrate the applicability of the method of reducibilities and construct new explicit hard instances of the graph three-coloring problem for all studied proof systems.<\/jats:p>","DOI":"10.1145\/3265985","type":"journal-article","created":{"date-parts":[[2018,12,20]],"date-time":"2018-12-20T13:35:46Z","timestamp":1545312946000},"page":"1-46","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Proof Complexity Meets Algebra"],"prefix":"10.1145","volume":"20","author":[{"given":"Albert","family":"Atserias","sequence":"first","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Barcelona, Catalonia, Spain"}]},{"ORCID":"http:\/\/orcid.org\/0000-0003-0945-0801","authenticated-orcid":false,"given":"Joanna","family":"Ochremiak","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Diderot, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2018,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21951"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"e_1_2_2_3_1","first-page":"18","article-title":"Lower bounds for polynomial calculus: Non-binomial case","volume":"242","author":"Alekhnovich M.","year":"2003","unstructured":"M. Alekhnovich and A. Razborov . 2003 . Lower bounds for polynomial calculus: Non-binomial case . Proc. Steklov Institute Math. 242 (2003), 18 -- 35 . M. Alekhnovich and A. Razborov. 2003. Lower bounds for polynomial calculus: Non-binomial case. Proc. Steklov Institute Math. 242 (2003), 18--35.","journal-title":"Proc. Steklov Institute Math."},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the 43rd Symposium on Foundations of Computer Science (FOCS\u201902)","author":"Alon N.","unstructured":"N. Alon and M. R. Capalbo . 2002. Explicit unique-neighbor expanders . In Proceedings of the 43rd Symposium on Foundations of Computer Science (FOCS\u201902) . IEEE Computer Society. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=645413.652127. N. Alon and M. R. Capalbo. 2002. Explicit unique-neighbor expanders. In Proceedings of the 43rd Symposium on Foundations of Computer Science (FOCS\u201902). IEEE Computer Society. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=645413.652127."},{"key":"e_1_2_2_5_1","volume-title":"A note on semi-algebraic proofs and gaussian elimination over prime fields. CoRR abs\/1502.03974","author":"Atserias A.","year":"2015","unstructured":"A. Atserias . 2015. A note on semi-algebraic proofs and gaussian elimination over prime fields. CoRR abs\/1502.03974 ( 2015 ). arxiv:1502.03974. Retrieved from http:\/\/arxiv.org\/abs\/1502.03974. A. Atserias. 2015. A note on semi-algebraic proofs and gaussian elimination over prime fields. CoRR abs\/1502.03974 (2015). arxiv:1502.03974. Retrieved from http:\/\/arxiv.org\/abs\/1502.03974."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.12.049"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2007.06.025"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30201-8_9"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2898435"},{"key":"e_1_2_2_10_1","volume-title":"44th International Colloquium on Automata, Languages, and Programming (ICALP\u201917)","author":"Atserias A.","unstructured":"A. Atserias and J. Ochremiak . 2017. Proof complexity meets algebra. In 44th International Colloquium on Automata, Languages, and Programming (ICALP\u201917) . 110:1--110:14. A. Atserias and J. Ochremiak. 2017. Proof complexity meets algebra. In 44th International Colloquium on Automata, Languages, and Programming (ICALP\u201917). 110:1--110:14."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/bsl.2015.25"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2556646"},{"key":"e_1_2_2_13_1","unstructured":"L. Barto A. A. Krokhin and R. Willard. 2017. Polymorphisms and how to use them. In The Constraint Satisfaction Problem Andrei Krokhin and Stanislav \u017divn\u00fd (Eds.) Vol. 7. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik 1--44. L. Barto A. A. Krokhin and R. Willard. 2017. Polymorphisms and how to use them. In The Constraint Satisfaction Problem Andrei Krokhin and Stanislav \u017divn\u00fd (Eds.) Vol. 7. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik 1--44."},{"key":"e_1_2_2_14_1","unstructured":"L. Barto J. Opr\u0161al and M. Pinsker. 2015. The wonderland of reflections. CoRR abs\/1510.04521 (2015). Retrieved from http:\/\/arxiv.org\/abs\/1510.04521. L. Barto J. Opr\u0161al and M. Pinsker. 2015. The wonderland of reflections. CoRR abs\/1510.04521 (2015). Retrieved from http:\/\/arxiv.org\/abs\/1510.04521."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-73.1.1"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129733"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/509907.509988"},{"key":"e_1_2_2_18_1","unstructured":"C. Berkholz. 2017. The relation between polynomial calculus Sherali-Adams and sum-of-squares proofs. In Electronic Colloquium on Computational Complexity (ECCC\u201917). Retrieved from https:\/\/eccc.weizmann.ac.il\/report\/2017\/154. C. Berkholz. 2017. The relation between polynomial calculus Sherali-Adams and sum-of-squares proofs. In Electronic Colloquium on Computational Complexity (ECCC\u201917). Retrieved from https:\/\/eccc.weizmann.ac.il\/report\/2017\/154."},{"key":"e_1_2_2_19_1","unstructured":"A. Bulatov. 2009. Bounded relational width. (2009). Manuscript. https:\/\/www.cs.sfu.ca\/∼abulatov\/papers\/relwidth.pdf. A. Bulatov. 2009. Bounded relational width. (2009). Manuscript. https:\/\/www.cs.sfu.ca\/∼abulatov\/papers\/relwidth.pdf."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2017.37"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700376676"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1726"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873054"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237860"},{"key":"e_1_2_2_25_1","volume-title":"32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201917)","author":"Dawar A.","unstructured":"A. Dawar and P. Wang . 2017. Definability of semidefinite programming and lasserre lower bounds for CSPs . In 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201917) . 1--12. A. Dawar and P. Wang. 2017. Definability of semidefinite programming and lasserre lower bounds for CSPs. In 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201917). 1--12."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794266766"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/227683.227684"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00157-2"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00446-2"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.17323\/1609-4514-2002-2-4-647-679"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0273-0979-06-01126-8"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1137\/090775646"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539705447372"},{"key":"e_1_2_2_35_1","volume-title":"Proceedings of the 17th National Conference on Artificial Intelligence and 12th Conference on Innovative Applications of Artificial Intelligence. AAAI Press, 175--181","author":"Kolaitis Ph. G.","unstructured":"Ph. G. Kolaitis and M. Y. Vardi . 2000. A game-theoretic approach to constraint satisfaction . In Proceedings of the 17th National Conference on Artificial Intelligence and 12th Conference on Innovative Applications of Artificial Intelligence. AAAI Press, 175--181 . Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=647288.721266. Ph. G. Kolaitis and M. Y. Vardi. 2000. A game-theoretic approach to constraint satisfaction. In Proceedings of the 17th National Conference on Artificial Intelligence and 12th Conference on Innovative Applications of Artificial Intelligence. AAAI Press, 175--181. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=647288.721266."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1137\/S1052623400366802"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.28.3.470.16391"},{"key":"e_1_2_2_40_1","volume-title":"Nullstellensatz and Gr\u00f6bner Bases. In 32nd Computational Complexity Conference (CCC\u201917)","author":"Lauria M.","unstructured":"M. Lauria and J. Nordstr\u00f6m . 2017. Graph colouring is hard for algorithms based on Hilbert\u2019s Nullstellensatz and Gr\u00f6bner Bases. In 32nd Computational Complexity Conference (CCC\u201917) . 2:1--2:20. M. Lauria and J. Nordstr\u00f6m. 2017. Graph colouring is hard for algorithms based on Hilbert\u2019s Nullstellensatz and Gr\u00f6bner Bases. In 32nd Computational Complexity Conference (CCC\u201917). 2:1--2:20."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1137\/0801013"},{"key":"e_1_2_2_42_1","volume-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","volume":"31","author":"Pitassi T.","year":"1997","unstructured":"T. Pitassi . 1997 . Algebraic propositional proof systems. In Descriptive Complexity and Finite Models, N. Immerman and Ph. G. Kolaitis (Eds.) . DIMACS Series in Discrete Mathematics and Theoretical Computer Science , Vol. 31 . American Mathematical Society, 68--96. T. Pitassi. 1997. Algebraic propositional proof systems. In Descriptive Complexity and Finite Models, N. Immerman and Ph. G. Kolaitis (Eds.). DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 31. American Mathematical Society, 68--96."},{"key":"e_1_2_2_43_1","volume-title":"Sets and Proofs, Invited Papers from Logic Colloquium","author":"Pudl\u00e1k P.","year":"1997","unstructured":"P. Pudl\u00e1k . 1999. On the complexity of the propositional calculus . In Sets and Proofs, Invited Papers from Logic Colloquium 1997 . Cambridge University Press , 197--218. P. Pudl\u00e1k. 1999. On the complexity of the propositional calculus. In Sets and Proofs, Invited Papers from Logic Colloquium 1997. Cambridge University Press, 197--218."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2008.74"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1137\/0403036"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005087"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1137\/16M1079245"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536414.1536457"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2017.38"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3265985","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,15]],"date-time":"2023-04-15T02:10:28Z","timestamp":1681524628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3265985"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,20]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1,31]]}},"alternative-id":["10.1145\/3265985"],"URL":"http:\/\/dx.doi.org\/10.1145\/3265985","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,20]]},"assertion":[{"value":"2017-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}