Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi ‍[J. ‍ACM, 65(6):37:1–55, 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 ‍[Theory ‍Comput., 17: 1-88, 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 stronger constant-depth 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. Specifically, we show the following:

We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically, we show that the subset-sum variant $\displaystyle \sum_{i,j,k,\ell\in[n]}Z_{i_{J}^{\prime}k}\ell x_{i}x_{j}x_{k}x_{\ell}-\beta=0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as constant-depth circuits. Andrews and Forbes (STOC’22) established recently a constant-depth IPS lower bound, but their hard instance does not have itself small constant-depth circuits, while our instance is computable already with small depth-2 circuits. Our argument relies on extending the recent breakthrough lower bounds against constant-depth algebraic circuits by Limaye, Srinivasan and Tavenas (FOCS’21) to the functional lower bound framework of Forbes, Shpilka, Tzameret and Wigderson (ToC’21), and may be of independent interest. Specifically, we construct a polynomial f computable with small-size constant-depth circuits, such that the multilinear polynomial computing $1/f$ over Boolean values and its appropriate set-multilinear projection are hard for constant-depth circuits.

In this paper we consider the relationship between monomial-size and bit-complexity in Sums-of-Squares (SOS) in Polynomial Calculus Resolution over rationals (PCR/ℚ). We show that there is a set of polynomial constraints Qnover Boolean variables that has both SOS and PCR/ℚ refutations of degree 2 and thus with only polynomially many monomials, but for which any SOS or PCR/ℚ refutation must have exponential bit-complexity, when the rational coefficients are represented with their reduced fractions written in binary.

We prove that both Polynomial Calculus and Sums-of-Squares proof systems admit a strong form of feasible interpolation property for sets of polynomial equality constraints. Precisely, given two sets P(x,z) and Q(y,z) of equality constraints, a refutation Π of P(x,z) ∪ Q(y,z), and any assignment a to the variables z, one can find a refutation of P(x,a) or a refutation of Q(y,a) in time polynomial in the length of the bit-string encoding the refutation Π. For Sums-of-Squares we rely on the use of Boolean axioms, but for Polynomial Calculus we do not assume their presence.

We show that if a system of degree-$k$ polynomial constraints on~$n$ Boolean variables has a Sums-of-Squares (SOS) proof of unsatisfiability with at most~$s$ many monomials, then it also has one whose degree is of the order of the square root of~$n \log s$ plus~$k$. A similar statement holds for the more general Positivstellensatz (PS) proofs. This establishes size-degree trade-offs for SOS and PS that match their analogues for weaker proof systems such as Resolution, Polynomial Calculus, and the proof systems for the LP and SDP hierarchies of Lovász and Schrijver. As a corollary to this, and to the known degree lower bounds, we get optimal integrality gaps for exponential size SOS proofs for sparse random instances of the standard NP-hard constraint optimization problems. We also get exponential size SOS lower bounds for Tseitin and Knapsack formulas. The proof of our main result relies on a zero-gap duality theorem for pre-ordered vector spaces that admit an order unit, whose specialization to PS and SOS may be of independent interest.