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.
This is a kick ass book.<p>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.
Well worth reading. This was one of the major sources that helped me learn SMT, and I now have some projects in the area (yet another superoptimizer).<p>Z3 has been very good as an 'external brain' for all sorts of problems.
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