Document Open Access Logo

A Lower Bound for Polynomial Calculus with Extension Rule

Author Yaroslav Alekseev

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2021.21.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • algebraic proofs
  • polynomial calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

A major proof complexity problem is to prove a superpolynomial lower bound on the length of Frege proofs of arbitrary depth. A more general question is to prove an Extended Frege lower bound. Surprisingly, proving such bounds turns out to be much easier in the algebraic setting. In this paper, we study a proof system that can simulate Extended Frege: an extension of the Polynomial Calculus proof system where we can take a square root and introduce new variables that are equivalent to arbitrary depth algebraic circuits. We prove that an instance of the subset-sum principle, the binary value principle 1 + x₁ + 2 x₂ + … + 2^{n-1} x_n = 0 (BVP_n), requires refutations of exponential bit size over ℚ in this system. 
Part and Tzameret [Fedor Part and Iddo Tzameret, 2020] proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations [Ran Raz and Iddo Tzameret, 2008]) refutations of BVP_n. We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of BVP_n.

Cite As Get BibTex

Yaroslav Alekseev. A Lower Bound for Polynomial Calculus with Extension Rule. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CCC.2021.21

Author Details

Yaroslav Alekseev
  • Chebyshev Laboratory, St. Petersburg State University, Russia

Funding

  • Alekseev, Yaroslav: research is supported by «Native towns», a social investment program of PJSC «Gazprom Neft».

Acknowledgements

I would like to thank Edward A. Hirsch for guidance and useful discussions at various stages of this work. Also, I wish to thank Dmitry Itsykson and Dmitry Sokolov for very helpful comments concerning this work.

References

  1. Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, and Iddo Tzameret. Semi-algebraic proofs, IPS lower bounds and the τ-conjecture: Can a natural number be negative? In Proceedings of the 52th Annual ACM Symposium on Theory of Computing (STOC 2020), pages 54-67, 2020. Google Scholar
  2. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc. (3), 73(1):1-26, 1996. URL: https://doi.org/10.1112/plms/s3-73.1.1.
  3. Sam Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computer and System Sciences, 62(2):267-289, 2001. URL: https://doi.org/10.1006/jcss.2000.1726.
  4. Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiří Sgall. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity, 6(3):256-298, 1996. URL: https://doi.org/10.1007/BF01294258.
  5. V. Chvátal, W. Cook, and M. Hartmann. On cutting-plane proofs in combinatorial optimization. Linear Algebra and its Applications, 114-115:455-499, 1989. Special Issue Dedicated to Alan J. Hoffman. URL: https://doi.org/10.1016/0024-3795(89)90476-X.
  6. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on the Theory of Computing (Philadelphia, PA, 1996), pages 174-183, New York, 1996. ACM. Google Scholar
  7. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  8. W. Cook, C. R. Coullard, and G. Turan. On the complexity of cutting plane proofs. Discrete Applied Mathematics, 18:25-38, 1987. Google Scholar
  9. Dima Grigoriev and Edward A. Hirsch. Algebraic proof systems over formulas. Theoret. Comput. Sci., 303(1):83-102, 2003. Logic and complexity in computer science (Créteil, 2001). Google Scholar
  10. Joshua A. Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM, 65(6):37:1-37:59, 2018. URL: https://doi.org/10.1145/3230742.
  11. Armin Haken. The intractability of resolution. Theoret. Comput. Sci., 39(2-3):297-308, 1985. Google Scholar
  12. Johan Håstad. On small-depth Frege proofs for tseitin for grids. J. ACM, 68(1), 2020. URL: https://doi.org/10.1145/3425606.
  13. Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi. The surprising power of constant depth algebraic proofs. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, page 591–603, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394754.
  14. Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall. Lower bounds for the polynomial calculus and the gröbner basis algorithm. Computational Complexity, 8(2):127-144, 1999. URL: https://doi.org/10.1007/s000370050024.
  15. Dmitry Itsykson and Dmitry Sokolov. Resolution over linear equations modulo two. Annals of Pure and Applied Logic, 171(1):102722, 2020. URL: https://doi.org/10.1016/j.apal.2019.102722.
  16. Jan Krajíček. Discretely ordered modules as a first-order extension of the cutting planes proof system. The Journal of Symbolic Logic, 63(4):1582-1596, 1998. Google Scholar
  17. Jan Krajíček and Pavel Pudlák. Propositional proof systems, the consistency of first order theories and the complexity of computations. Journal of Symbolic Logic, 54(3):1063–1079, 1989. URL: https://doi.org/10.2307/2274765.
  18. Fedor Part and Iddo Tzameret. Resolution with counting: Different moduli and dag-like lower bounds. In 12th Innovations in Theoretical Computer Science Conference, ITCS 2020, January, 2020, Seattle, WA, USA, 2020. Google Scholar
  19. Toniann Pitassi. Algebraic propositional proof systems. In Descriptive complexity and finite models (Princeton, NJ, 1996), volume 31 of DIMACS Ser. Discrete Math. Theoret. Comput. Sci., pages 215-244. Amer. Math. Soc., Providence, RI, 1997. Google Scholar
  20. Toniann Pitassi. Unsolvable systems of equations and proof complexity. In Proceedings of the International Congress of Mathematicians, Vol. III (Berlin, 1998), pages 451-460, 1998. Google Scholar
  21. Toniann Pitassi, Benjamin Rossman, Rocco A. Servedio, and Li-Yang Tan. Poly-logarithmic Frege depth lower bounds via an expander switching lemma. In Proceedings of the Forty-Eighth Annual ACM Symposium on Theory of Computing, STOC '16, page 644–657, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2897518.2897637.
  22. Ran Raz and Iddo Tzameret. Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Logic, 155(3):194-224, 2008. URL: https://doi.org/10.1016/j.apal.2008.04.001.
  23. Alexander A. Razborov. Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Mathematical notes of the Academy of Sciences of the USSR, 41(4):333-338, 1987. URL: https://doi.org/10.1007/BF01137685.
  24. Alexander A. Razborov. Lower bounds for the polynomial calculus. Comput. Complexity, 7(4):291-324, 1998. Google Scholar
  25. Roman Smolensky. Algebraic methods in the theory of lower bounds for boolean circuit complexity. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing (STOC 1987), pages 77-82, 1987. URL: https://doi.org/10.1145/28395.28404.
  26. Dmitry Sokolov. (semi)algebraic proofs over ± 1 variables. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, page 78–90, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3357713.3384288.
  27. Grigori Tseitin. On the complexity of derivations in propositional calculus, pages 466-483. Studies in constructive mathematics and mathematical logic Part II. Consultants Bureau, New-York-London, 1968. Google Scholar
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