[Proof Complexity] New paper
Ilario Bonacina
bonacina at di.uniroma1.it
Thu Nov 6 16:46:06 CET 2014
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
More information about the Proof-Complexity
mailing list