Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant (Q2473386)

This book has two topics as main points: ``decision procedures'' and ``algorithms to be applied for these decisions''. This is a very interesting approach because in real life (i.e. in the application area) a given problem is what comes first, and then solutions have to be found, and mostly there is a broad range of possibilities for the solutions. Since real problems tend to be very large and complex, the creation of appropriate solutions by means of algorithms and software is the final target. Such an approach is very useful for graduate students or students in year four or five, since their knowledge is already broad enough to study several topics covered by the book. As can be seen by the sequence of topics, the knowledge covered is very extensive and gives an impressive example what could or should be done in education to prepare for real-life problems. The theoretical background is based on first-order theories, but in many different ways. It starts with methods and technologies that are based on propositional logics, such as SAT solvers and binary decision diagrams, followed by equality logic and uninterpreted functions. The next chapters deal with linear arithmetic, bit vectors, arrays, pointer logic, quantified formulas, deciding combinations of theories and propositional encodings. Some hints to a C++ library for the development of decision procedures close the book. Each chapter introduces and explains a lot of different concepts and presents good examples, some problems and exercises with algorithm-based solutions, and a glossary at its end, which makes the book very applicable and readable. The book is very well written and interesting to read. As a textbook for students it will require hard work to fully understand it and go through it. It might also be useful to use it in parts.