[aseipp]

It's unfortunately a very rapidly evolving field and is difficult to "break into" as far as understanding internals. Though just understanding DLPP is a good start, but ultimately you need a lot of practice and experimenting on your own to get a good intuition for it.

For the record these are problems many "solver-aided" communities struggle with; I'd say the #1 problem that people have with this class of tools is prospective, interested users struggle with the issue of "how can I encode my problem into a SAT instance with reasonable efficiency." I know this because it's my #1 problem!

On the other hand, there are a lot of "straightforward" NP problems you can run into and get good solutions for with little effort though. Binpacking comes up surprisingly often and being able to just throw it at a solver and get a good, generic solution quickly is always nice (not that this is exclusive to SMT solvers, but it's an easy way to get your feet wet at least.)