Anyway I'm not an expert on SAT solving. Thank you for the perspective you provide with which I was unfamiliar.
Edit: I don't think the OP meant SAT solvers when they said "symbolic learning"?
SAT solvers, however, learn from their "mistakes", at least internally, which is really interesting and I think opens some very, very interesting research questions that as far as I know don't have that much money going into.
For example, human brains can reason internally and learn in a similar manner, learning from "mistakes" of rule application in the same way (i.e. if I try to do this, then that fails, but if I do this other thing, then it works but not fully...). Just some food for thought.
Automated Theorem Proving is also a very important success of the Symbolic camp but I would argue a less interesting one, since SAT solvers can do much more than prove theorems (and ATPs that can do more than prove theorems invariably use a SAT/SMT solver internally, like Vampire does for example). SAT solvers (and extensions) are used in model checkers, software and hardware verification tools, software and hardware synthesis tools, operations research, etc.
One reason I think that theorem provers are more important than SAT solvers is that SLD-Resolution at least can be efficiently implemented.
Also, Resolution can be used for induction, from examples and a background theory. That's a relatively recent result and you won't find a very clear account of it in the literature, but for instance, see here some early work:
Meta-Interpretive Learning of Higher-Order Dyadic Datalog: Predicate Invention Revisited
https://www.ijcai.org/Proceedings/13/Papers/231.pdf
You have to unpick it from the language used but "meta-interpretive learning" means that it's based on a Prolog meta-interpreter, so an implementation of SLD(NF)-Resolution. And those "metarules" are really second-order definite clauses. The approach is really higher-order SLD-Resolution that turns out to be inductive, rather than deductive.
But what you say about learning from "mistakes" reminded me of a rival approach, "Learning from Failures":
Learning programs by learning from failures
http://andrewcropper.com/pubs/popper.pdf
Which is, incidentally, implemented by means of SAT solvers (via ASP, ultimately). I'm more of a fan of the meta-interpretive approach (I study it), but I think the Popper paper might interest you, judging from your comment.
Vampire uses a portfolio of strategies, including the application of an SMT solver (Z3). This link goes into some detail: http://smt2019.galois.com/papers/tool_paper_20.pdf
This is the most relevant bit for our conversation:
> There are only two cases where Vampire can return sat: Firstly in UF and secondly, if Vampire produces a ground problem after preprocessing it may pass this problem to Z3 and report its result (possibly sat) directly.
Essentially this refers to model building, i.e. solving existential problems. That's where SAT solvers excel. This includes producing counter-examples which are extremely useful in industry.
Commercial Mixed Integer Programming solvers can optimize massive problems to provably global optimality very very quickly, and they too have an internal learning mechanism (cutting-planes).
They excel at reasoning but they can only learn from the outcomes of the rules they are provided and how they interact, they cannot learn from data. With the advent of soft-constraints (which have an associated weight) I wonder if such systems could be adapted to learn probabilistic rules as well.
Some existing systems (like AlphaGo) already combine symbolic approaches (Monte-Carlo Tree Search) with Deep Learning, but what I'm thinking about here goes beyond that.