I like that he has examples that show CNF formulations next to SMT formulations. SMT is really easy to write, but it seems like magic. CNF draws back the curtain a bit.
It’s worth learning the basic use of some constraint solver, since they are now so fast and powerful. Z3 is free software and is very, very good, and you’d be surprised how many problems it can tackle (see: hundreds of examples in this book) that might actually come up in your work or life. In particular, you can attack scheduling problems with Z3 and people will think you are a wizard.
Those are small examples but you can scale them up and Z3 can still handle it.
I have no meaningful experience in OR, don’t know how SAT solvers work or how Z3 reduces things to SAT. Yet I was able to use it to attack a really gnarly scheduling problem with hundreds of variables, weird constraints, preferences, etc.
In addition to finding feasible solutions Z3 has an “Optimize” class that can handle soft constraints and objective functions. This is really useful. (I suspect CPLEX/Gurobi would be better at this but Z3 still works well.)
I'm slightly annoyed that this only describes the implementation. It would be very helpful for those beginning to study this area to see the formulations of these problems in mathematical notation. (Yes, some of them are trivially identified. Others, however, not so much.) Seeing the translation from S{M|A}T into the implemented formulation (on, in my case, the reverse) was helpful in my understanding of how this whole sub-field works. Otherwise, though, this is a remarkable resource for understanding problems and how to translate them into S{M|A}T
