Improved exponential-time algorithm for k-SAT

Ramamohan Paturi, Payel Pudlak, Michael E. Saks, Francis Zane

Research output: Contribution to journalConference articlepeer-review

93 Scopus citations


An algorithm, ResolveSat, a randomized variant of Davis, Longeman and Loveland (DLL) or Davis-Putnam procedure, for finding satisfying assignments of Boolean formulae in conjunctive normal form is presented. Rather than applying the DLL procedure to the input formula F, ResolveSat enlarges F by adding additional clauses using limited resolution before performing DLL. The basic idea behind the analysis is the same: a critical clause for a variable at a satisfying assignment gives rise to a unit clause in the DLL procedure with sufficiently high probability, thus increasing the probability of finding a satisfying assignment. The effect of multiple critical clauses in producing unit clauses is examined.

Original languageEnglish (US)
Pages (from-to)628-637
Number of pages10
JournalAnnual Symposium on Foundations of Computer Science - Proceedings
StatePublished - 1998
Externally publishedYes
EventProceedings of the 1998 39th Annual Symposium on Foundations of Computer Science - Palo Alto, CA, USA
Duration: Nov 8 1998Nov 11 1998

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture

Cite this