[throwaway81523]

The basic algorithm is DPLL and the other stuff is mostly clever hacks added on. There is a critical-systems analogy for SAT that supposedly really does go pretty far. SAT problems are like water: below a certain temperature, water is frozen and understandable. By analogy, SAT problems with too many clauses per variable are generally unsatisfiable and it's not too hard to figure that out. Above that temperature, water is liquid and understandable: the corresponding SAT problems tend to be satisfiable. It's only right around the critical temperature that stuff is chaotic and unpredictable, and that's where the hard SAT instances are. When I say that the analogy goes pretty far, I mean that the phenomenon really does get studied using tools of statistical physics. But I don't know anything more about that at the moment.

https://yurichev.com/writings/SAT_SMT_by_example.pdf is a very good tutorial about using SAT solvers, though it doesn't say much about the theory.

The so-far-released portions of Knuth TAOCP vol 4 do discuss SAT solver theory.

[freemint]

What you just stated about the critical temperature is true for some classes of random instances. Early results on larger classes of random instances from this line of research do not survive scaling experiments. I don't have a reference one that but I recall that being said in one of the discussion rounds of the Beyond Satisfiability online seminary at the Simons Institute.