zlacker

> Symbolic AI like SAT solvers and planners is not trying to learn from data and there's no context in which it has to "scale with huge data".

Actually, they do. Conflict-Driven Clause Learning (CDCL) learns from conflicts encountered during working on the data. The space of inputs they are dealing with oftentimes is in the order of the number of atoms in Universe and that is huge.

>>thesz+(OP)
"Learning" in CDCL is a misnomer: the learning process is Resolution and it's deductive (reasoning) not inductive (learning).

>>YeGobl+BE
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".

>>joe_th+N41
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 :)

>>YeGobl+kn2
I'd love a diatribe if you're still following this post.

>>YeGobl+BE
You invented a new kind of learning that somewhat contradicts usual definition [1] [2].

  [1] https://www.britannica.com/dictionary/learning
  [2] https://en.wikipedia.org/wiki/Learning

"Learning" in CDCL is perfectly in line of "gaining knowledge."

>>YeGobl+kn2
Take a look at Satisfaction-Driven Clause Learning [1].

[1] https://www.cs.cmu.edu/~mheule/publications/prencode.pdf

>>joe_th+zb7
As would I.

You know, this seems like yet another reason to allow HN users to direct message each other, or at least receive reply notifications. Dang, why can't we have nice things?

>>EarlKi+Is8
Oh, hi guys. Sorry just saw this.

Oh gosh I gotta do some work today, so no time to write what I wanted. Maybe watch this space? I'll try to make some time later today.