[Proof Complexity] New paper

[Ilario Bonacina]

Dear colleagues,

a new paper, “Space proof complexity for random 3-CNFs via a (2 - Ï)-Hall's Theorem”, 
by Ilario Bonacina, Nicola Galesi, Tony Huynh and Paul Wollan, is available on ECCC, 
at http://eccc.hpi-web.de/report/2014/146/ <http://eccc.hpi-web.de/report/2014/146/>

Any comments or corrections are appreciated.

The abstract is the following:

We investigate the space complexity of refuting  3 -CNFs in Resolution and algebraic systems. No lower bound for refuting any family of 3 -CNFs was previously known for the total space in resolution or for the monomial space in algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3 -CNF ¶  in n  variables requires, with high probability, Ê(n=logn) distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation ¶  requires, with high probability, Ê(n=logn) clauses each of width Ê(n=logn) to be kept at the same time in memory. This gives a Ê(n2=log2n) lower bound for the total space needed in Resolution to refute ¶ . The main technical innovation is a variant of Hall's theorem. We show that in bipartite graphs G  with bipartition (L;R) and left-degree at most 3, L  can be covered by certain families of disjoint paths, called (2;4)-matchings, provided that L  expands in R  by a factor of (2ÀÏ) , for Ï<123.

Best,

Ilario