[tombert]

Solvers are something that still kind of feel like magic to me. I have done a fair amount of Isabelle, and the "sledgehammer" tool in there (which uses solvers to see if an existing proof can be made to work to solve your subgoal) is something that impresses me every single time I use it.

[nextaccountic]

On same level of abstraction I think it's useful to view those tools as some form of constraint solving. Think how you can solve sudoku with pen and paper by writing out each possibility, then fill squares either because it has only one possibility or by making guesses. After you fill a square, you can then update your possible states (propagate constraints), and repeat until you solve it or hit an impossible solve (in which case you need to backtrack on some earlier guess).

The algorithms differ mainly in how they keep track of all possibilities and how they update them

I think this answer is pretty good https://cstheory.stackexchange.com/a/29428 (take note at the end "sat is csp on boolean domains")