[Proof Complexity] Paper announcement: A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

[Jakob Nordstrom]

Dear colleagues,

This is just to announce that we have posted a full-length version at
http://eccc.hpi-web.de/report/2015/078 of the paper "A Generalized Method for
Proving Polynomial Calculus Degree Lower Bounds" by Mladen Miksa and myself,
to be presented at CCC this summer.

The abstract follows below. Any questions or comments would be much appreciated.

Best regards,
Jakob Nordstrom

**********

ABSTRACT

We study the problem of obtaining lower bounds for polynomial calculus (PC)
and polynomial calculus resolution (PCR) on proof degree, and hence by
[Impagliazzo et al. '99] also on proof size.  [Alekhnovich and Razborov '03]
established that if the clause-variable incidence graph of a CNF formula F is
a good enough expander, then proving that F is unsatisfiable requires high
PC/PCR degree. We further develop the techniques in [AR03] to show that if one
can "cluster" clauses and variables in a way that "respects the structure" of
the formula in a certain sense, then it is sufficient that the incidence graph
of this clustered version is an expander. As a corollary of this, we prove
that the functional pigeonhole principle (FPHP) formulas require high PC/PCR
degree when restricted to constant-degree expander graphs. This answers an
open question in [Razborov '02], and also implies that the standard CNF
encoding of the FPHP formulas require exponential proof size in polynomial
calculus resolution. Thus, while Onto-FPHP formulas are easy for polynomial
calculus, as shown in [Riis '93], both FPHP and Onto-PHP formulas are hard
even when restricted to bounded-degree expanders.