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.
I'll be happy to circle back to more modern methods once the core parts of the field are addressed. The point of the library is not really to deliver a competitive solver (yet).