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 language||English (US)|
|Number of pages||11|
|Journal||Conference Proceedings of the Annual ACM Symposium on Theory of Computing|
|State||Published - 1998|
|Event||Proceedings of the 1998 30th Annual ACM Symposium on Theory of Computing - Dallas, TX, USA|
Duration: May 23 1998 → May 26 1998
All Science Journal Classification (ASJC) codes