Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?

Question

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!

Answer 1

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

Answer 2

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.)