Description:
This textbook on decision procedure has been used to teach undergraduate and graduate courses at ETH Zurich and at the Technion, Haifa. The authors focus on theories that are expressive enough to model real problems, but are still decidable.
Review Quotes: "This is an excellent book, which I am delighted to have the chance to review. ... The text and the supporting material have been invaluable, stepping the reader through decision procedures and their combinations. ... I highly recommend the book to those interested in understanding and contributing to the world of SAT and SMT solving ... ." (Rosemary Monahan, Formal Aspects of Computing, Vol. 30 (06), November, 2018)