7
$\begingroup$

For an unsatisfiable CNF instance, CDCL will return a resolution refutation.

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

$\endgroup$

1 Answer 1

8
$\begingroup$

CDCL with restarts is more or less equivalent to general resolution, see Pipatsrisawat & Darwiche. 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 for a discussion. For a general survey, see §7.3 in Buss & Nordström’s chapter in the Handbook of Satisfiability.

$\endgroup$
2
  • 1
    $\begingroup$ Moreover, I want to confirm that DPLL will return a tree-like and regular resolution right? $\endgroup$
    – Jxb
    Commented Aug 2, 2023 at 1:22
  • 2
    $\begingroup$ 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). $\endgroup$ Commented Aug 2, 2023 at 6:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.