Loading...
Please wait, while we are loading the content...
Similar Documents
On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas (1997)
| Content Provider | CiteSeerX |
|---|---|
| Author | Beame, Paul Karp, Richard Pitassi, Toniann Saks, Michael |
| Description | We study the complexity of proving unsatisfiability for random k-CNF formulas with clause density D = m=n where m is number of clauses and n is the number of variables. We prove the first nontrivial general upper bound, giving algorithms that, in particular, for k = 3 produce refutations almost certainly in time 2 O(n=D) . This is polynomial when m n 2 =logn. We show that our upper bounds are tight for certain natural classes of Davis-Putnam algorithms. We show further that random 3-CNF formulas of clause density D almost certainly have no resolution refutation of size smaller than 2 W(n=D 4+e ) , which implies the same lower bound on any Davis-Putnam algorithm. We also give a much simpler argument based on a novel form of self-reduction that yields a slightly weaker 2 W(n=D 5+e ) lower bound. 1 Introduction The random k-CNF model has been widely studied for several good reasons. First, it is an intrinsically natural model, analogous to the random graph model, that shed... In 30th Annual ACM Symposium on the Theory of Computing |
| File Format | |
| Language | English |
| Publisher Date | 1997-01-01 |
| Access Restriction | Open |
| Subject Keyword | Random 3-cnf Formula Certain Natural Class Clause Density Random K-cnf Model First Nontrivial General Upper Bound Simpler Argument Upper Bound Random K-cnf Formula Random Graph Model Unsatisfiability Proof Novel Form Natural Model Produce Refutation Davis-putnam Algorithm Resolution Refutation Several Good Reason |
| Content Type | Text |
| Resource Type | Article |
