On the complexity of unsatisfiability proofs for random k-CNF formulas

Paul Beame, Richard Karp, Toniann Pitassi, Michael Saks

Research output: Contribution to journalConference articlepeer-review

70 Scopus citations


The complexity of proving unsatisfiability for random k-CNF formulas with clause density Δ = m/n where m is number of clauses and n is the number of variables is studied. The random 3-CNF formulas of clause density Δ almost certainly have no resolution refutation of size smaller than 2Ω(n/Δ(5+ε)), which implies the same lower bound on any Davis-Putnam algorithm.

Original languageEnglish (US)
Pages (from-to)561-571
Number of pages11
JournalConference Proceedings of the Annual ACM Symposium on Theory of Computing
StatePublished - 1998
Externally publishedYes
EventProceedings of the 1998 30th Annual ACM Symposium on Theory of Computing - Dallas, TX, USA
Duration: May 23 1998May 26 1998

All Science Journal Classification (ASJC) codes

  • Software

Cite this