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

Albert Atserias, Johannes Klaus Fichte, Marc Thurley

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. We do so by analyzing a co…