3 ms·

It's not just you. I found the technical sections of the article impenetrable. And yet my background is on resolution theorem-proving (I did my PhD research on

It's not just you. I found the technical sections of the article impenetrable. And yet my background is on resolution theorem-proving (I did my PhD research on Inductive Logic Programming) and I read the article wishing to understand how CDCL is related to Resolution, but I couldn't figure that out. I don't have a background in SAT solving but the "clause learning" in CDCL looks a lot like what we call a Resolution-derivation in Resolution theorem-proving. In short, given a conjunction of two (propositional or first order) clauses (¬φ ∨ ψ) ∧ (φ ∨ χ) Resolution eliminates the contradiction in the "complementary pair" (¬φ, φ) and derives the new clause ψ ∨ χ. If that's what CDCL folk call learning then that's really interesting to me because most of Inductive Logic Programming is an effort to use Resolution for inductive inference i.e. machine learning, but in logic. I guess I should check the article's bibliography. They reference s a textbook that might be useful ("Handbook of Satisfiability". Though one of the authors is an author of the article so that may not bode well for the textbook).

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 ago
  If 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.
js8 3y ago
The resolution is actually also what 2SAT algorithm is doing.
- YeGoblynQueenne 3y ago
  I like how the Wikipedia page on 2SAT explains the use of Resolution: >> Resolution, a method for combining pairs of constraints to make additional valid constraints, also leads to a polynomial time solution. "Constraints" being a slightly odd-sounding way to put it, to me anyway, but I guess that's because I don't have the relevant background to think of clauses that way.

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 ago
If 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.

js8 3y ago

The resolution is actually also what 2SAT algorithm is doing.

YeGoblynQueenne 3y ago
I like how the Wikipedia page on 2SAT explains the use of Resolution: >> Resolution, a method for combining pairs of constraints to make additional valid constraints, also leads to a polynomial time solution. "Constraints" being a slightly odd-sounding way to put it, to me anyway, but I guess that's because I don't have the relevant background to think of clauses that way.