Abstract

Strong algebraic proof systems such as IPS (Ideal Proof System;

Grochow-Pitassi 2018)

offer a general model for deriving polynomials in an ideal and refuting

unsatisfiable propositional

formulas, subsuming most standard propositional proof systems. A major

approach for lower bounding the size of IPS refutations is the Functional

Lower Bound Method (Forbes, Shpilka,

Tzameret and Wigderson 2021), which reduces the hardness of refuting a

polynomial equation f(x) = 0 with no Boolean solutions to the hardness of

computing the function 1/f(x) over the Boolean cube with an algebraic

circuit. Using symmetry we provide a general way to obtain many new hard

instances against fragments of IPS via the functional lower bound method.

This includes hardness over finite fields and hard instances different from

Subset Sum variants both of which were unknown before, and significantly

improved constant-depth IPS lower bounds.

Conversely, we expose the limitation of this method by showing it cannot

lead to proof complexity lower bounds for any hard Boolean instance (e.g.,

CNFs) for any sufficiently strong proof systems (including AC0[p]-Frege).



Joint work with Tuomas Hakoniemi and Nutan Limaye