2015/03/05 by Patrick Bennett, Ilario Bonacina, Bennett, Patrick +9
Computer Science · Mathematics · #Combinatorics (math.CO) #Computational Complexity (cs.CC) #FOS: Computer and information sciences #FOS: Mathematics #Probability (math.PR) #cs.CC #math.CO #math.PR
paper · pdf · doi:10.48550/arxiv.1503.01613
arXiv admin note: substantial text overlap with arXiv:1411.1619
arxiv created 2015/04/02 · arxiv updated 2015/04/03
We investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF ϕ in n variables requires, with high probability, Ω(n) distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation ϕ requires, with high probability, Ω(n) clauses each of width Ω(n) to be kept at the same time in memory. This gives a Ω(n2) lower bound for the total space needed in Resolution to refute ϕ. These results are best possible (up to a constant factor). The main technical innovation is a variant of Hall's Lemma. 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 VW-matchings, provided that L expands in R by a factor of (2-ε), for ε< 1/23.