Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution

Abstract

We offer a new understanding of some aspects of practical SAT-solvers that are based on DPLL with unit-clause propagation, clause-learning, and restarts. On the theoretical side, we do so by analyzing a concrete algorithm which we claim is faithful to what practical solvers do. In particular, before making any new decision or restart, the solver repeatedly applies the unit-resolution rule until saturation, and leaves no component to the mercy of non-determinism except for some internal randomness. We prove the perhaps surprising fact that, although the solver is not explicitely designed for it, it ends up behaving as width-k resolution after no more than n ^2k + 1 conflicts and restarts, where n is the number of variables. In other words, width-k resolution can be thought as n ^2k + 1 restarts of the unit-resolution rule with learning. On the experimental side, we give evidence for the claim that this theoretical result describes real world solvers. We do so by running some of the most prominent solvers on some CNF formulas that we designed to have resolution refutations of width k. It turns out that the upper bound of the theoretical result holds for these solvers and that the true performance appears to be not very far from it.

Partially supported by project CICYT TIN2007-68005-C04-03.