Document Open Access Logo

Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares

Author Tuomas Hakoniemi

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2020.63.pdf
  • Filesize: 441 kB
  • 14 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Tuomas Hakoniemi
  • Universitat Politècnica de Catalunya, Barcelona, Spain

Funding

Partially funded by European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreement ERC-2014-CoG 648276 (AUTAR) and MICCIN grant TIN2016-76573-C2-1P (TASSAT3).

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.

References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. Alexander A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291-324, 1998. URL: https://doi.org/10.1007/s000370050013.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact