Comment by YorkshireSeason

Unfortunately, Harrison's book, despite its many other merits, doesn't really treat CDCL (= conflict-driven clause learning), which is really what makes SAT solvers fly.