Space proof complexity for random 3-CNFs

Patrick Bennett, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, Paul Wollan

Research output: Contribution to journalArticleResearchpeer-review

5 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)165-176
Number of pages12
JournalInformation and Computation
Publication statusPublished - 1 Aug 2017
Externally publishedYes


  • Monomial space
  • Polynomial calculus
  • Proof complexity
  • Random CNFs
  • Resolution
  • Total space

Cite this