Decision Procedures

Viac o knihe

A decision procedure is an algorithm that provides a correct yes/no answer for decision problems. This book focuses on expressive yet decidable first-order theories relevant to automated verification, reasoning, theorem-proving, compiler optimization, and operations research. The authors draw on graph theory and logic, applying techniques widely used in industry. They introduce key concepts such as SAT, Satisfiability Modulo Theories (SMT), and the DPLL(T) framework. Separate chapters delve into decision procedures for propositional logic, equalities and uninterpreted functions, linear arithmetic, bit vectors, arrays, pointer logic, and quantified formulas, as well as combined theories via the Nelson-Oppen procedure. The second edition updates the first, which was published in 2008 when SMT was still developing. It enhances the DPLL(T) framework and expands the SAT chapter with modern heuristics and a new section on incremental satisfiability and Constraints Satisfaction Problem (CSP). The chapter on quantifiers now includes sections on general quantification using E-matching and Effectively Propositional Reasoning (EPR). A new chapter discusses SMT applications in industrial software engineering and computational biology. Each chapter features a detailed bibliography and exercises, with additional resources available on the authors’ website.