Document

# New Lower Bounds for Polynomial Calculus over Non-Boolean Bases

## File

LIPIcs.SAT.2024.10.pdf
• Filesize: 0.81 MB
• 20 pages

## Cite As

Yogesh Dahiya, Meena Mahajan, and Sasank Mouli. New Lower Bounds for Polynomial Calculus over Non-Boolean Bases. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.10

## Abstract

In this paper, we obtain new size lower bounds for proofs in the Polynomial Calculus (PC) proof system, in two different settings. - When the Boolean variables are encoded using ±1 (as opposed to 0,1): We establish a lifting theorem using an asymmetric gadget G, showing that for an unsatisfiable formula F, the lifted formula F∘G requires PC size 2^{Ω(d)}, where d is the degree required to refute F. Our lower bound does not depend on the number of variables n, and holds over every field. The only previously known size lower bounds in this setting were established quite recently in [Sokolov, STOC 2020] using lifting with another (symmetric) gadget. The size lower bound there is 2^{Ω((d-d₀)²/n)} (where d₀ is the degree of the initial equations arising from the formula), and is shown to hold only over the reals. - When the PC refutation proceeds over a finite field 𝔽_p and is allowed to use extension variables: We show that there is an unsatisfiable AC⁰[p] formula with N variables for which any PC refutation using N^{1+ε(1-δ)} extension variables, each of arity at most N^{1-ε} and size at most N^c, must have size exp(Ω(N^{εδ}/polylog N)). Our proof achieves these bounds by an XOR-ification of the generalised PHP^{m,r}_n formulas from [Razborov, CC 1998]. The only previously known lower bounds for PC in this setting are those obtained in [Impagliazzo-Mouli-Pitassi, CCC 2023]; in those bounds the number of extension variables is required to be sub-quadratic, and their arity is restricted to logarithmic in the number of original variables. Our result generalises these, and demonstrates a tradeoff between the number and the arity of extension variables. Since our tautology is represented by a small AC⁰[p] formula, our results imply lower bounds for a reasonably strong fragment of AC⁰[p]-Frege.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Proof complexity
##### Keywords
• Proof Complexity
• Polynomial Calculus
• degree
• Fourier basis
• extension variables

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Michael Alekhnovich and Alexander A Razborov. Lower bounds for polynomial calculus: Non-binomial case. In Proceedings 42nd IEEE Symposium on Foundations of Computer Science, pages 190-199. IEEE, 2001.
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. Christoph Berkholz. The relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares proofs. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
4. 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.
5. 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.
6. Stephen A Cook and Robert A Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979.
7. Nicola Galesi and Massimo Lauria. Optimality of size-degree tradeoffs for Polynomial Calculus. ACM Transactions on Computational Logic (TOCL), 12(1):1-22, 2010.
8. Dima Grigoriev and Edward A Hirsch. Algebraic proof systems over formulas. Theoretical Computer Science, 303(1):83-102, 2003.
9. Dima Grigoriev, Edward A Hirsch, and Dmitrii V Pasechnik. Complexity of semi-algebraic proofs. In STACS 2002: 19th Annual Symposium on Theoretical Aspects of Computer Science Antibes-Juan les Pins, France, March 14-16, 2002 Proceedings 19, pages 419-430. Springer, 2002.
10. 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.
11. 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). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
12. Russell Impagliazzo, Pavel Pudlák, and Jiri Sgall. Lower bounds for the Polynomial Calculus and the Gröbner basis algorithm. Computational Complexity, 8:127-144, 1999.
13. Matthias Krause and Pavel Pudlák. On the computational power of depth 2 circuits with threshold and modulo gates. In Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, pages 48-57, 1994.
14. Mladen Miksa and Jakob Nordström. A generalized method for proving Polynomial Calculus degree lower bounds. In 30th Conference on Computational Complexity, CCC 2015, volume 33 of LIPIcs, pages 467-487, 2015.
15. Aaron Potechin. Sum of squares bounds for the ordering principle. In 35th Computational Complexity Conference, 2020.
16. Ran Raz and Iddo Tzameret. Resolution over linear equations and multilinear proofs. Annals of Pure and Applied Logic, 155(3):194-224, 2008.
17. Alexander A Razborov. Lower bounds for the Polynomial Calculus. Computational Complexity, 7:291-324, 1998.
18. 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.
X

Feedback for Dagstuhl Publishing