Document Open Access Logo

Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields

Authors Russell Impagliazzo, Sasank Mouli, Toniann Pitassi

PDF
Thumbnail PDF

File

LIPIcs.CCC.2023.7.pdf
  • Filesize: 0.81 MB
  • 24 pages

Document Identifiers

Author Details

Russell Impagliazzo
  • University of California San Diego, CA, USA
Sasank Mouli
  • Hyderabad, India
Toniann Pitassi
  • Columbia University, New York, NY, USA

Funding

  • Impagliazzo, Russell: Supported by the Simons Foundation and NSF grant CCF-1909634.
  • Mouli, Sasank: Supported by the Simons Foundation, NSF grant CCF-1909634 and the Swiss National Science Foundation project n. 200021_207429 / 1 "Ideal Membership Problems and the Bit Complexity of Sum of Squares Proofs".
  • Pitassi, Toniann: Supported by NSF grant CCF-1900460, and by the IAS School of Mathematics.

Acknowledgements

The authors would like to thank Paul Beame and Dmitry Sokolov for helpful discussions.

Cite AsGet BibTex

Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi. Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields. In 38th Computational Complexity Conference (CCC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 264, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CCC.2023.7

Abstract

For every prime p > 0, every n > 0 and κ = O(log n), we show the existence of an unsatisfiable system of polynomial equations over O(n log n) variables of degree O(log n) such that any Polynomial Calculus refutation over 𝔽_p with M extension variables, each depending on at most κ original variables requires size exp(Ω(n²)/10^κ(M + n log n))

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof complexity
  • Algebraic proof systems
  • Polynomial Calculus
  • Extension variables
  • AC⁰[p]-Frege

Metrics

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

References

  1. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. In 42nd Annual Symposium on Foundations of Computer Science, FOCS 2001, 14-17 October 2001, Las Vegas, Nevada, USA, pages 190-199. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/SFCS.2001.959893.
  2. Yaroslav Alekseev. A lower bound for polynomial calculus with extension rule. In Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021, July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 21:1-21:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.21.
  3. Robert Andrews and Michael A. Forbes. Ideals, determinants, and straightening: Proving and using lower bounds for polynomial ideals. CoRR, abs/2112.00792, 2021. URL: https://arxiv.org/abs/2112.00792.
  4. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on hilbert’s nullstellensatz and propositional proofs. Proceedings of the London Mathematical Society, 3(1):1-26, 1996. Google Scholar
  5. Paul Beame, Richard Karp, Toniann Pitassi, and Michael Saks. The efficiency of resolution and davis-putnam procedures. SIAM Journal on Computing, 31(4):1048-1075, 2002. Google Scholar
  6. Eli Ben-Sasson and Russell Impagliazzo. Random cnfs are hard for the polynomial calculus. In 40th Annual Symposium on Foundations of Computer Science (Cat. No. 99CB37039), pages 415-421. IEEE, 1999. Google Scholar
  7. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - Resolution made simple. In Proceedings of the thirty-first annual ACM symposium on Theory of computing, pages 517-526, 1999. Google Scholar
  8. 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. Google Scholar
  9. Vašek Chvátal and Endre Szemerédi. Many hard examples for resolution. Journal of the ACM (JACM), 35(4):759-768, 1988. Google Scholar
  10. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, pages 174-183, 1996. Google Scholar
  11. Stephen A Cook and Robert A Reckhow. The relative efficiency of propositional proof systems. The journal of symbolic logic, 44(1):36-50, 1979. Google Scholar
  12. Stefan S. Dantchev and Søren Riis. On relativisation and complexity gap. In Matthias Baaz and Johann A. Makowsky, editors, Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Gödel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings, volume 2803 of Lecture Notes in Computer Science, pages 142-154. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45220-1_14.
  13. Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. Proof complexity lower bounds from algebraic circuit complexity. Theory Comput., 17:1-88, 2021. URL: https://theoryofcomputing.org/articles/v017a010/.
  14. Nashlen Govindasamy, Tuomas Hakoniemi, and Iddo Tzameret. Simple hard instances for low-depth algebraic proofs. In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 188-199. IEEE, 2022. Google Scholar
  15. Armin Haken. The intractability of resolution. Theoretical computer science, 39:297-308, 1985. Google Scholar
  16. 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, pages 591-603, 2020. Google Scholar
  17. Russell Impagliazzo, Pavel Pudlák, and Jirí Sgall. Lower bounds for the polynomial calculus and the gröbner basis algorithm. Comput. Complex., 8(2):127-144, 1999. URL: https://doi.org/10.1007/s000370050024.
  18. Alexander A Razborov. Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Math. notes of the Academy of Sciences of the USSR, 41(4):333-338, 1987. Google Scholar
  19. Roman Smolensky. Algebraic methods in the theory of lower bounds for boolean circuit complexity. In Proceedings of the nineteenth annual ACM symposium on Theory of computing, pages 77-82, 1987. Google Scholar
  20. Dmitry Sokolov. (semi) algebraic proofs over ±1 variables. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, pages 78-90, 2020. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact