Theory of Computing
-------------------
Title     : Towards an Understanding of Polynomial Calculus: New
Separations and Lower Bounds
Authors   : Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordstrom, and Marc Vinyals
Volume    : 21
Number    : 4
Pages     : 1-48
URL       : https://theoryofcomputing.org/articles/v021a004

Abstract
--------

During the last two decades, an active line of research in proof
complexity has been into the space complexity of proofs and how space
is related to other measures. By now these aspects of the resolution
proof system are fairly well understood, but many open problems remain
for the related but stronger proof system polynomial calculus
(PC/PCR). For instance, the space complexity of many standard
"benchmark formulas" is still open, as well as the relation of space
to size and degree in PC/PCR.

We prove that if a formula requires large resolution width, then
making XOR substitution yields a formula requiring large PCR space
(and hence also PC space), providing some circumstantial evidence that
degree might be a lower bound for space. More importantly, this
immediately yields formulas that are very hard for space but very easy
for size, exhibiting a size-space separation similar to what is known
for resolution. Using related ideas, we show that if a graph has good
expansion and if in addition its edge set can be partitioned into
short cycles, then the Tseitin formula over this graph requires large
PCR space. In particular, Tseitin formulas over random $4$-regular
graphs almost surely require space at least $\Omega(\sqrt{n})$.

Our proofs use techniques introduced by Bonacina and Galesi (ITCS'13).
Our final contribution, however, is to show that these techniques
provably cannot yield non-constant space lower bounds for the
functional pigeonhole principle, delineating the limitations of this
framework.

-------------------

An extended abstract of this paper appeared in the Proceedings of
the 40th International Colloquium on Automata, Languages and
Programming (ICALP'13).