Yurichev's SAT/SMT by Example [0] is a great (free!) resource for learning how to model problems to SAT/SMT

[0] - https://smt.st/