I keep asking this question and not getting satisfying answers so I'll try again: I'm sure I encounter problems every month that reduce to SAT (or SMT) and I could save a lot of time and energy (for both me and my computer) if I would just ask a SAT solver to find the answer instead of writing custom code each time.

However, that thought never strikes me because I haven't gotten used to thinking about problems as SAT reducible. But since the thought never strikes me, I also don't get many opportunities to get used to that!

How does one get started with incorporating SAT (or SMT) solving as a natural part of going about one's day?