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?
Keep your eyes open for problems where you have to do some form of brute-force search. Those that doesn't have a clear solution other than trying all the possibilities.
Another thing is that the best kind of problem for SAT solvers are problems that ask a yes/no question. Is there a way to satisfy all the constraints, and if so what are the variable assignments that do so? It's also possible to use SAT solvers for other kinds of problems (e.g. find the solution with the best score) but it's more advanced.
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?