<p>It is indeed and here is the reference for it if needed:</p>
<p>Pipatsrisawat, K., &amp; Darwiche, A. (2011). On the power of clause-learning SAT solvers as resolution engines. Artificial intelligence, 175(2), 512-525</p>

CC BY-SA 4.0
2023-12-06T06:31:43.923Z
More generally, in [handbook of satisfiability](http://satlive.org/2021/01/26/handbook2.html), edition2, page 142.
Jxb
CC BY-SA 4.0
2023-11-27T09:21:05.167Z
2023-11-27T09:21:05.167Z
holf
<p>Yes, anything learned by conflict analysis in conflict-driven clause learning can be derived by resolution from the original formula. The technically slightly more precise claim is that any newly learned clause is derived by so-called trivial resolution from previously derived clauses and the input formula.</p>
<p>This goes back much further than Pipatsrisawat and Darwiche. I believe that the first authors that pointed out explicitly that conflict-driven clause learning SAT solvers generate resolution proofs might be Beame, Kautz, and Sabharwal in &quot;Towards Understanding and Harnessing the Potential of Clause Learning&quot;, Journal of Artificial Intelligence Research, 2004 (<a href="https://www.jair.org/index.php/jair/article/view/10392" rel="noreferrer">https://www.jair.org/index.php/jair/article/view/10392</a>).</p>
<p>However, the proofs generated by SAT solvers have a very peculiar structure. It is a natural question to ask whether SAT solvers are weaker than resolution or whether resolution proofs with the extra structural restrictions imposed by CDCL could in principle be as short as general resolution proofs (expect possibly for polynomial blow-up). This is the question answered affirmatively by Pipatsrisawat and Darwiche in their 2011 paper. (The same result can be read off independent work by Atserias, Fichte, and Thurley in 2011, though they did not state it explicitly in the earlier conference version of their paper --- conference versions of PD and AFT appeared in 2009.)</p>

CC BY-SA 4.0
2024-02-06T22:15:26.730Z
2024-02-06T22:15:26.730Z
Jakob Nordstrom
<p>I have a question regarding the Conflict-Driven Clause Learning (CDCL) algorithm applied to an unsatisfiable CNF formula <span class="math-container">$F$</span>.</p>
<p><strong>Specifically, can all the conflict clauses learned by the CDCL algorithm be derived from the original formula <span class="math-container">$F$</span> through resolution?</strong></p>
<p>I believe the answer should be affirmative. My reasoning is that if this were not the case, I would have trouble understanding why the general resolution size of
<span class="math-container">$F$</span> can serve as a lower bound for the runtime of the CDCL algorithm. However, I'm seeking clarification or confirmation on this point.</p>
<p>Could someone provide insights or references that confirm or refute this understanding? Thank you!</p>

CC BY-SA 4.0
2023-11-27T08:12:19.670Z
Yes, all the learned clauses in CDCL are proven by resolution. This should be mentioned in textbook expositions of CDCL.
Laakeri
<sat><proof-complexity>
Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?
Jxb
# Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?

(Asked by: username_0 on 2023-11-27)

I have a question regarding the Conflict-Driven Clause Learning (CDCL) algorithm applied to an unsatisfiable CNF formula $F$.

**Specifically, can all the conflict clauses learned by the CDCL algorithm be derived from the original formula $F$ through resolution?**

I believe the answer should be affirmative. My reasoning is that if this were not the case, I would have trouble understanding why the general resolution size of
$F$ can serve as a lower bound for the runtime of the CDCL algorithm. However, I'm seeking clarification or confirmation on this point.

Could someone provide insights or references that confirm or refute this understanding? Thank you!

**Tags:** sat, proof-complexity
> **Comments:**
> **username_1**: Yes, all the learned clauses in CDCL are proven by resolution. This should be mentioned in textbook expositions of CDCL.  

---

## 2 answers

### Answer by username_2 on 2023-11-27. Score: 6 | Accepted answer

It is indeed and here is the reference for it if needed:

Pipatsrisawat, K., & Darwiche, A. (2011). On the power of clause-learning SAT solvers as resolution engines. Artificial intelligence, 175(2), 512-525

> **Comments:**
> **username_0**: More generally, in [handbook of satisfiability](http://satlive.org/2021/01/26/handbook2.html), edition2, page 142.  

---

### Answer by username_3 on 2024-02-06. Score: 5

Yes, anything learned by conflict analysis in conflict-driven clause learning can be derived by resolution from the original formula. The technically slightly more precise claim is that any newly learned clause is derived by so-called trivial resolution from previously derived clauses and the input formula.

This goes back much further than Pipatsrisawat and Darwiche. I believe that the first authors that pointed out explicitly that conflict-driven clause learning SAT solvers generate resolution proofs might be Beame, Kautz, and Sabharwal in "Towards Understanding and Harnessing the Potential of Clause Learning", Journal of Artificial Intelligence Research, 2004 (<https://www.jair.org/index.php/jair/article/view/10392>).

However, the proofs generated by SAT solvers have a very peculiar structure. It is a natural question to ask whether SAT solvers are weaker than resolution or whether resolution proofs with the extra structural restrictions imposed by CDCL could in principle be as short as general resolution proofs (expect possibly for polynomial blow-up). This is the question answered affirmatively by Pipatsrisawat and Darwiche in their 2011 paper. (The same result can be read off independent work by Atserias, Fichte, and Thurley in 2011, though they did not state it explicitly in the earlier conference version of their paper --- conference versions of PD and AFT appeared in 2009.)


---

