TY - JOUR
T1 - Space proof complexity for random 3-CNFs
AU - Bennett, Patrick
AU - Bonacina, Ilario
AU - Galesi, Nicola
AU - Huynh, Tony
AU - Molloy, Mike
AU - Wollan, Paul
PY - 2017/8/1
Y1 - 2017/8/1
N2 - 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 of φ 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) and answer questions about space complexity of 3-CNFs. The main technical innovation is a variant of Hall's Lemma. We show that in bipartite graphs 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/5.
AB - 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 of φ 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) and answer questions about space complexity of 3-CNFs. The main technical innovation is a variant of Hall's Lemma. We show that in bipartite graphs 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/5.
KW - Monomial space
KW - Polynomial calculus
KW - Proof complexity
KW - Random CNFs
KW - Resolution
KW - Total space
UR - http://www.scopus.com/inward/record.url?scp=85021162863&partnerID=8YFLogxK
U2 - 10.1016/j.ic.2017.06.003
DO - 10.1016/j.ic.2017.06.003
M3 - Article
AN - SCOPUS:85021162863
SN - 0890-5401
VL - 255
SP - 165
EP - 176
JO - Information and Computation
JF - Information and Computation
ER -