4 ms·
Conflict explanation in CDCL is entirely based around resolution, the idea being to take a conflicting set of clauses and apply resolution a bunch of times to “
by xavxav 3y ago
Conflict explanation in CDCL is entirely based around resolution, the idea being to take a conflicting set of clauses and apply resolution a bunch of times to “simplify” the conflict into its most general form.
- YeGoblynQueenne 3y agoIf I understand correctly what "conflicting" means, that process can't possibly result in an empty clause, as in Resolution refutation proofs, correct? What would be the gold standard reference for CDCL? Something that would be taught at an undergraduate class, say? Edit: after reading a bit on the net it seems like clause learning in CDCL is basically Resolution-derivation by input Resolution. Cool beans.