Daniel Kroening and Ofer Strichman: Decision Procedures – An Algorithmic Point of View
Springer, 2016, 356 pages, ISBN 978-3-662-57065-4
https://www.springer.com/gp/book/9783662504963
Summary
This book, entitled Decision Procedures – An Algorithmic Point of View, successfully describes and explains algorithmic solutions to decision problems. It is well-suited for use as a textbook and as a developer reference. The book precisely describes a series of algorithms used by decision procedures and also includes many worked out examples accompanied by a library that includes implementations of the algorithms.
This review is written by Stefan Hallerstede for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community.
Decision Procedures – An Algorithmic Point of View
by
Daniel Kroening and Ofer Strichman.
Review
A decision procedure takes a problem as input and yields as output an answer of either yes or no. A theoretical difficulty is that many interesting problems have high complexity that is exponential or worse. In practice, this means that the run-time of a decision procedure may be excessively long and the answer arrive too late to be useful. To address this difficulty, the book discusses specific problems for which efficient algorithms are known, heuristics to increase efficiency, clever encodings for problems that permit applying efficient decision procedures, and practical implementation techniques. A complete explanation of the theory underlying decision procedures, while missing in this book, is available in other standard textbooks, such as [KS01].
Decision Procedures is designed primarily for teaching the theory and practice of decision procedures to graduate and advanced undergraduate students. The presentation of the material in the book is highly appropriate for this target audience. The book is also suitable for advanced developers as suggested in the book’s foreword. For this audience, in particular, the detailed worked out examples should be very helpful.
To understand the book, a background in computer science and some mathematical maturity is useful. Basic knowledge of complexity theory should also prove helpful in some places, but the book does not rely heavily on such knowledge. As is appropriate, the book’s focus is on the practical aspects and implementation of selected algorithms and methods.
A 2013 review of the first edition of the book [Bar13] provides a good summary of the material covered and its relevance. The second edition of Decision Procedures has been updated to describe new developments and shifts in the field. Moreover, a chapter has been added which describes advanced industrial applications, e.g., in computational biology. A 2018 review [Mon18] discusses the use of the book in teaching. It also provides an excellent overview of the topics covered in the book’s second edition.
Chapters 1-3 of the second edition of Decision Procedures provide an easy to read introduction to decision procedures and the basic SAT and SMT algorithms supporting them. Chapter 11 supplements this by describing current approaches using lazy and eager encodings. Chapters 4-10 are more technical in nature, dealing with encodings and decision procedures for equality, uninter- preted functions, linear arithmetic, bit vectors, arrays, pointers and quantifiers. The inclusion of many supporting examples facilitates the reader’s understanding of more technical but also essen- tial details. Finally, Chapter 12 discusses applications in software engineering and computational biology. This provides important motivation for students. The two appendices on SMT-LIB and a C++ library for programming decision procedures support practical application and experimen- tation. The supporting web page [KS22] contains additional material, including a library whose contents are available for download. In addition, the web site offers supporting teaching materials and suggested projects. Unfortunately, the current web page refers to the first edition. This web page should be updated to be compatible with the book’s second edition.
Two other books describing decision procedures have been published, namely, The Handbook of Satisfiability by Biere et al. and The Handbook of Practical Logic and Automated Reasoning by Harrison [Har09]. The Handbook of Satisfiability discusses SAT in detail and SMT briefly but lacks the depth and wide coverage of this book. Moreover, it is not designed for university teach- ing. The second book, The Handbook of Practical Logic and Automated Reasoning, discusses the implementation of decisions procedures and other approaches to automated reasoning in Ocaml. The material covered focuses on theorem proving support and does not cover SMT. In contrast to these two books, Decision Procedures, as mentioned above, is suitable not only for students but for advanced developers as well.
In summary, both the first and the second editions of the book Decision Procedures are valuable both as teaching resources and also as references.
References
[Bar13] Clark W. Barrett. ”Decision Procedures: An Algorithmic Point of View, ” by Daniel Kroening and Ofer Strichman, springer-verlag, 2008. J. Autom. Reason, 51(4):453–456, 2013.
[Har09] John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
[KS01] Efim Kinber and Carl Smith. Theory of Computing. A Gentle Introduction. Prentice Hall, 2001.
[KS22] Daniel Kroening and Ofer Strichman. http://www.decision-procedures.org/, Retrieved 8 June 2022.
[Mon18] Rosemary Monahan. Daniel Kroening and Ofer Strichman: Decision procedures Springer Verlag, 2016, xxi, +356 isbn 978-3-662-50496-3 (Hardback, e69, 67), http://www.decision-procedures.org/. Formal Aspects Comput, 30(6):759, 2018.