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

arXiv: https://arxiv.org/abs/1401.3868 · HTML: https://mlsanity.com/paper/1401.3868/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Jan 2014.

## Built on by (most cited first, 7 of 7)

- [Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All?](https://mlsanity.com/paper/2210.03553/) (2022)
- [Too much information: why CDCL solvers need to forget learned clauses](https://mlsanity.com/paper/2202.01030/) (2022)
- [On Dedicated CDCL Strategies for PB Solvers](https://mlsanity.com/paper/2109.01013/) (2021)
- [Advanced Tools and Methods for Treewidth-Based Problem Solving -- Extended Abstract](https://mlsanity.com/paper/2208.11340/) (2022)
- [Are Hitting Formulas Hard for Resolution?](https://mlsanity.com/paper/2206.15225/) (2022)
- [Characterizing Structural Hardness of Logic Programs: What makes Cycles and Reachability Hard for Treewidth?](https://mlsanity.com/paper/2301.07472/) (2023)
- [Extended Version of: On the Structural Hardness of Answer Set Programming: Can Structure Efficiently Confine the Power of Disjunctions?](https://mlsanity.com/paper/2402.03539/) (2024)

## Abstract (arXiv)

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 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 explicitly designed for it, with high probability it ends up behaving as width-k resolution after no more than O(n^2k+2) conflicts and restarts, where n is the number of variables. In other words, width-k resolution can be thought of as O(n^2k+2) restarts of the unit-resolution rule with learning.