TR23-132 Authors: Yogesh Dahiya, Meena Mahajan, Sasank Mouli

Publication: 12th September 2023 07:27

Downloads: 177

Keywords:

In this paper, we obtain new size lower bounds for proofs in the

Polynomial Calculus (PC) proof system, in two different settings.

1. When the Boolean variables are encoded using $\pm 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 \circ G$ requires PC size $2^{\Omega(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^{\Omega((d-d_0)^2/n)}$ (where $d_0$ 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

$\mathbb{F}_p$ and is allowed to use extension variables: We show

that there is an unsatisfiable 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}/\poly\log

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 [ImpagliazzoMouliPitassi, 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.