## Abstract

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 language | English (US) |
---|---|

Pages (from-to) | 628-637 |

Number of pages | 10 |

Journal | Annual Symposium on Foundations of Computer Science - Proceedings |

State | Published - 1998 |

Externally published | Yes |

Event | Proceedings of the 1998 39th Annual Symposium on Foundations of Computer Science - Palo Alto, CA, USA Duration: Nov 8 1998 → Nov 11 1998 |

## All Science Journal Classification (ASJC) codes

- Hardware and Architecture