Comment by YeGoblynQueenne
10 months ago
"Learning" in CDCL is a misnomer: the learning process is Resolution and it's deductive (reasoning) not inductive (learning).
10 months ago
"Learning" in CDCL is a misnomer: the learning process is Resolution and it's deductive (reasoning) not inductive (learning).
You invented a new kind of learning that somewhat contradicts usual definition [1] [2].
"Learning" in CDCL is perfectly in line of "gaining knowledge."
I'm pretty sure most "industrial scale" SAT solvers involve both deduction and heuristics to decide which deductions to make and which to keep. At a certain scale, the heuristics have to be adaptive and then you have "induction".
I don't agree. The derivation of new clauses by Resolution is well understood as deductive and the choice of what clauses to keep doesn't change that.
Resolution can be used inductively, and also for abduction, but that's going into the weeds a bit- it's the subject of my PhD thesis. Let me know if you're in the mood for a proper diatribe :)
Take a look at Satisfaction-Driven Clause Learning [1].
[1] https://www.cs.cmu.edu/~mheule/publications/prencode.pdf
I'd love a diatribe if you're still following this post.
2 replies →