Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

27

Voted
SIAMCOMP

2002

2002

We consider several problems related to the use of resolution-based methods for determining whether a given boolean formula in conjunctive normal form is satisfiable. First, building on work of Clegg, Edmonds and Impagliazzo, we give an algorithm for satisfiability that when given an unsatisfiable formula of F finds a resolution proof of F, and the runtime of our algorithm is nontrivial as a function of the size of the shortest resolution proof of F. Next we investigate a class of backtrack search algorithms, commonly known as Davis-Putnam procedures and provide the first average-case complexity analysis for their behavior on random formulas. In particular, for a simple algorithm in this class, called ordered DLL we prove that the running time of the algorithm on a randomly generated k-CNF formula with n variables and m clauses is 2(n(n/m)1/(k-2)) with probability 1 - o(1). Finally, we give new lower bounds on res(F), the size of the smallest resolution refutation of F, for a class of...

Related Content

Added |
23 Dec 2010 |

Updated |
23 Dec 2010 |

Type |
Journal |

Year |
2002 |

Where |
SIAMCOMP |

Authors |
Paul Beame, Richard M. Karp, Toniann Pitassi, Michael E. Saks |

Comments (0)