But deep learning neural network are also said to be used when there's no good solution known.
It's the first time I see the symmetry. When should I use a SAT vs an ANN?
Other than SAT and ANN, are there other kind or technology that automatically solve/approximate solutions?
A good guide (in my experience) -- with SAT while the answer is hard to find it's easy to check (like a Sudoku, or building a timetable with no clashes), while ANN give answers where verifying the answer isn't easy to perform computstionally (if I give you a translation of a text into Latin, verifying it is about as hard as just making a new one from scratch)
How could a SAT/SMT help me in this task? I know it's already used for math theorem checking.
E.g All men are mortal. Socrates is a man. Therefore Socrate is mortal. I have currently two way to solve syllogisms
One hard-coded Disjonction of cases (but not flexible enough for non canonical forms of syllogisms)
And a flexible one that generate a graph of transitivity.
Both are 100% accurate.
Could SAT/SMT give me a third way of determining if the conclusion is logically valid? (not non sequitur)
SMT is some extra stuff on top of SAT. There are a few frameworks which extend SAT. I'd look at minizinc, it is a fairly easy to use language which can produce SAT (and SMT, and others) as output. Often encoding things in SAT directly gets arkward.
System description: Transition system like automata or a guarded command language which induces a graph.
System Property: Stated in some logic, CTL/LTL
Output: Satisfied, or Unsatisfied with a counter example (usually a path in the graph which is false).
If your problem can fit into such a framework, have a look at model checkers: https://en.wikipedia.org/wiki/List_of_model_checking_tools
SAT solvers work out if it is possible to satisfy a logical model (hence the name).
In theory a neural network could approximate a function that solves SAT. In practice it is a much better idea to use a SAT solver. Neural networks aren't that powerful at solving logic puzzles.
One is heuristic vs algorithm. If SAT solver finds a solution, it's correct. If ANN finds a solution, it might be correct.
ANN is suitable for pattern recognition, statistical learning and representation learning. Learning continuous functions for example. SAT solvers work best for discrete problems.