New Lower Bounds for Polynomial Calculus Over Non-Boolean Bases

01 April 2025
Abstract: The Polynomial Calculus PC is an algebraic proof system based on Hilbert's Nullstellensatz, in which the unsatisfiability of polynomial equations in general, and CNF formulas in particular, can be certified. While several size lower bounds have long been known for PC over 0-1 encodings of Boolean variables, no lower bounds were known over the +1/-1 encoding until a recent work by Sokolov in STOC 2020; he established an exponential lower bound over the reals using a lifting technique with a symmetric gadget.

We show how to use an asymmetric gadget and obtain a stronger lower bound that works over any field. In a different setting, we also strengthen the lower bounds obtained recently by Impagliazzo, Mouli, Pitassi, in CCC 2023: over finite fields, when extension variables are allowed, we obtain size lower bounds in terms of the number and arity of the extension axioms. In both these results, the notion of quadratic degree introduced by Sokolov plays a crucial role. The talk will give an overview of the setting, the results, and the techniques.

Based on joint work with Yogesh Dahiya and Sasank Mouli https://doi.org/10.4230/LIPIcs.SAT.2024.10

Link to the talk: https://www.csa.iisc.ac.in/theoryseminars/?talk=20250401_MeenaMahajan