LIPIcs.ICALP.2020.63.pdf
- Filesize: 441 kB
- 14 pages
Document
Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares
Author
-
Part of:
Volume:
47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Colloquium on Automata, Languages, and Programming (ICALP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-06-29
File
Document Identifiers
Acknowledgements
I want to thank Albert Atserias for thorough comments on a preliminary versions of this work. I would also want to thank the anonymous reviewers who helped vastly to improve the presentation of this paper.
Cite AsGet BibTex
Tuomas Hakoniemi. Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 63:1-63:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ICALP.2020.63
https://doi.org/10.4230/LIPIcs.ICALP.2020.63
Abstract
We prove that both Polynomial Calculus and Sums-of-Squares proof systems admit a strong form of feasible interpolation property for sets of polynomial equality constraints. Precisely, given two sets P(x,z) and Q(y,z) of equality constraints, a refutation Π of P(x,z) ∪ Q(y,z), and any assignment a to the variables z, one can find a refutation of P(x,a) or a refutation of Q(y,a) in time polynomial in the length of the bit-string encoding the refutation Π. For Sums-of-Squares we rely on the use of Boolean axioms, but for Polynomial Calculus we do not assume their presence.
Subject Classification
ACM Subject Classification
- Theory of computation → Proof complexity
Keywords
- Proof Complexity
- Feasible Interpolation
- Sums-of-Squares
- Polynomial Calculus
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relative complexity of NP search problems. In Frank Thomson Leighton and Allan Borodin, editors, Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory of Computing, 29 May-1 June 1995, Las Vegas, Nevada, USA, pages 303-314. ACM, 1995. URL: https://doi.org/10.1145/225058.225147.
- Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and Toniann Pitassi. Non-automatizability of bounded-depth frege proofs. Computational Complexity, 13(1-2):47-68, 2004. URL: https://doi.org/10.1007/s00037-004-0183-5.
- Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for frege systems. SIAM J. Comput., 29(6):1939-1967, 2000. URL: https://doi.org/10.1137/S0097539798353230.
- Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the groebner basis algorithm to find proofs of unsatisfiability. In Gary L. Miller, editor, Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996, pages 174-183. ACM, 1996. URL: https://doi.org/10.1145/237814.237860.
- David A. Cox, John Little, and Donal O'Shea. Ideals, Varieties, and Algorithms. Undergraduate Texts in Mathematics. Springer, fourth edition, 2015. URL: https://doi.org/10.1007/978-3-319-16721-3.
- Dima Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theor. Comput. Sci., 259(1-2):613-622, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00157-2.
- Martin Grötschel, László Lovász, and Alexander Schrijver. Geometric Algorithms and Combinatorial Optimization, volume 2 of Algorithms and Combinatorics. Springer, 1988. URL: https://doi.org/10.1007/978-3-642-97881-4.
- Jan Krajíček and Pavel Pudlák. Some consequences of cryptographical conjectures for s^1_2 and EF. Inf. Comput., 140(1):82-94, 1998. URL: https://doi.org/10.1006/inco.1997.2674.
- Jan Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997. URL: http://www.jstor.org/stable/2275541.
- Monique Laurent. Sums of squares, moment matrices and optimization over polynomials. In Mihai Putinar and Seth Sullivant, editors, Emerging Applications of Algebraic Geometry, pages 157-270. Springer New York, New York, NY, 2009. URL: https://doi.org/10.1007/978-0-387-09686-5_7.
- Ryan O'Donnell. SOS Is Not Obviously Automatizable, Even Approximately. In Christos H. Papadimitriou, editor, 8th Innovations in Theoretical Computer Science Conference (ITCS 2017), volume 67 of Leibniz International Proceedings in Informatics (LIPIcs), pages 59:1-59:10, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ITCS.2017.59.
- Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
- Pavel Pudlák and Jirí Sgall. Algebraic models of computation and interpolation for algebraic proof systems. In Paul Beame and Samuel R. Buss, editors, Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, April 21-24, 1996, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 279-295. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/dimacs/039/15.
- Prasad Raghavendra and Benjamin Weitz. On the Bit Complexity of Sum-of-Squares Proofs. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017), volume 80 of Leibniz International Proceedings in Informatics (LIPIcs), pages 80:1-80:13, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.80.
- Alexander A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291-324, 1998. URL: https://doi.org/10.1007/s000370050013.