<p>CDCL with restarts is more or less equivalent to general resolution, see <a href="https://doi.org/10.1016/j.artint.2010.10.002" rel="noreferrer">Pipatsrisawat &amp; Darwiche</a>. CDCL without restarts is more difficult to pin down. It sits somewhere between regular and general resolution; it can be formalized as either pool resolution or regWRTI. See <a href="https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/poolVsRegular2/" rel="noreferrer">Bonet, Buss &amp; Johannsen</a> for a discussion. For a general survey, see §7.3 in <a href="https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/ProofComplexitySAT/" rel="noreferrer">Buss &amp; Nordström’s chapter</a> in the Handbook of Satisfiability.</p>

CC BY-SA 4.0
2023-08-02T01:22:59.993Z
Moreover, I want to confirm that DPLL will return a tree-like and regular resolution right?
Jxb
CC BY-SA 4.0
2023-08-02T06:57:51.030Z
Yes. Note that there is no difference between tree-like and tree-like regular resolution (any tree-like refutation can be made regular by omitting redundant branches).
Emil Jeřábek
CC BY-SA 4.0
2023-08-01T10:13:41.363Z
2023-08-01T10:13:41.363Z
Emil Jeřábek
<p>For an unsatisfiable CNF instance, <a href="https://en.wikipedia.org/wiki/Conflict-driven_clause_learning" rel="noreferrer">CDCL</a> will return a resolution refutation.</p>
<p><strong>My question</strong> : what kind of resolution does it return? tree-like, regular or general?</p>

<sat><resolution>
What kind of resolution is CDCL corresponding to?
Jxb
# What kind of resolution is CDCL corresponding to?

(Asked by: username_0 on 2023-08-01)

For an unsatisfiable CNF instance, [CDCL](https://en.wikipedia.org/wiki/Conflict-driven_clause_learning) will return a resolution refutation.

**My question** : what kind of resolution does it return? tree-like, regular or general?

**Tags:** sat, resolution

---

## 1 answers

### Answer by username_1 on 2023-08-01. Score: 8 | Accepted answer

CDCL with restarts is more or less equivalent to general resolution, see [Pipatsrisawat & Darwiche](https://doi.org/10.1016/j.artint.2010.10.002). CDCL without restarts is more difficult to pin down. It sits somewhere between regular and general resolution; it can be formalized as either pool resolution or regWRTI. See [Bonet, Buss & Johannsen](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/poolVsRegular2/) for a discussion. For a general survey, see §7.3 in [Buss & Nordström’s chapter](https://mathweb.ucsd.edu/%7Esbuss/ResearchWeb/ProofComplexitySAT/) in the Handbook of Satisfiability.

> **Comments:**
> **username_0**: Moreover, I want to confirm that DPLL will return a tree-like and regular resolution right?  
> **username_1**: Yes. Note that there is no difference between tree-like and tree-like regular resolution (any tree-like refutation can be made regular by omitting redundant branches).  

---

