Decision Procedures

More about the book

A decision procedure is an algorithm that provides a correct yes/no answer for a given decision problem. This work focuses on expressive yet decidable first-order theories relevant to automated verification, reasoning, theorem-proving, compiler optimization, and operations research. It employs techniques from graph theory and logic, widely used in industry. The authors introduce terminology related to SAT, Satisfiability Modulo Theories (SMT), and the DPLL(T) framework. The book examines decision procedures for propositional logic, equalities, uninterpreted functions, linear arithmetic, bit vectors, arrays, pointer logic, and quantified formulas. It also addresses the Nelson-Oppen procedure for deciding combined theories. The first edition, published in 2008, was adopted as a textbook globally, at a time when SMT was nascent. This second edition updates the DPLL(T) framework, expands the SAT chapter with modern heuristics, and adds a section on incremental satisfiability and the Constraints Satisfaction Problem (CSP). The chapter on quantifiers includes new sections on E-matching and Effectively Propositional Reasoning (EPR). Additionally, a new chapter discusses SMT applications in industrial software engineering and computational biology, coauthored by experts in the field. Each chapter features a detailed bibliography and exercises, with supplementary resources available on the authors’ website.