Yes, it is a very well written summary of what has been going on with SAT solvers in the last decades. I personally think most of this (r)evolution can be attributed to miniSAT. A relatively easy to read (at least compared to other theorem provers), free software implementation of a SAT solver, with instantiations if I remember correctly. Since variables only have two possible valuations (true/false) in boolean logic, they can be instantiated and the problem can be split up, and sometimes greatly simplified in doing so. I.e. we can replace each occurrence of variable 'a' with 'true' to make a new smaller problem, and then replace each occurrence variable 'a' with 'false' to make another smaller problem. I.e. split 1 problem into 2 simpler problems, and solve them in parallel etc.
I don't have a background in SAT solving but the "clause learning" in CDCL looks a lot like what we call a Resolution-derivation in Resolution theorem-proving. In short, given a conjunction of two (propositional or first order) clauses (¬φ ∨ ψ) ∧ (φ ∨ χ) Resolution eliminates the contradiction in the "complementary pair" (¬φ, φ) and derives the new clause ψ ∨ χ. If that's what CDCL folk call learning then that's really interesting to me because most of Inductive Logic Programming is an effort to use Resolution for inductive inference i.e. machine learning, but in logic. I guess I should check the article's bibliography. They reference s a textbook that might be useful ("Handbook of Satisfiability". Though one of the authors is an author of the article so that may not bode well for the textbook).