[wjholden]

I agree, the theory isn't nearly as difficult as the reductions. Dennis Yurichev's "SAT/SMT by Example" (https://smt.st/) is a great resource on this topic, although pretty intimidating.