Alladi Ramakrishnan Hall

New lower bounds for Polynomial Calculus over non-Boolean bases

Yogesh Dahiya

TIFR, Mumbai

(Hybrid mode. Join remotely at
zoom.us/j/98920091030
Meeting ID: 989 2009 1030
Passcode: 042550
)

Propositional proof complexity is the field of study of the complexity of proofs for tautological Boolean formulas. Cook and Reckhow introduced this area in their seminal work with the ultimate goal of resolving the question of NP versus coNP using upper/lower bounds for stronger and stronger proof systems. Polynomial Calculus (PC) is one such propositional proof system that has received wide attention since its introduction by Clegg, Edmonds and Impagliazzo. Despite having a reasonable understanding of PC, there has been little progress towards lower bounds for the stronger system AC0[p]-Frege, which was one of the main motives for defining PC. This indicates that we have to look at systems stronger than PC in order to get new insights.

In this work, we present new size lower bounds for PC proofs in two settings:

1. When the Boolean variables are encoded using +1/−1 (as opposed to 0/1): We prove that for an unsatisfiable formula F, the lifted formula F composed with a 1-bit indexing gadget G requires a PC size of 2^{\Omega(d)}, where d is the degree needed 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^{\Omega((d−d0)^2/n) (where d0 is the degree of the initial equations arising from the formula), and is shown to hold only over the reals.

2. When the PC refutation proceeds over a finite field Fp and is allowed to use extension variables: We show that there is an unsatisfiable AC0[p] formula with N variables for which any PC refutation using N^{1+\epsilon(1−\delta)} extension variables, each of arity at most N^{1−\epsilon} and size at most N^c, must have size exp (\Omega(N\epsilon\delta/polylog N)). The only previously known lower bounds for PC in this setting are those obtained in [Impagliazzo-Mouli-Pitassi, CCC 2023]; Our result generalises these, and demonstrates a tradeoff between the number and the arity of extension variables.

This is joint work with Meena Mahajan and Sasank Mouli, and will appear at SAT 2024.