# Decision Procedures: An Algorithmic Point of View

Springer Science & Business Media, May 23, 2008 - Computers - 306 pages

A decision procedure is an algorithm that, given a decision problem, terminates with a correct yes/no answer. Here, the authors focus on theories that are expressive enough to model real problems, but are still decidable. Specifically, the book concentrates on decision procedures for first-order theories that are commonly used in automated verification and reasoning, theorem-proving, compiler optimization and operations research. The techniques described in the book draw from fields such as graph theory and logic, and are routinely used in industry.

The authors introduce the basic terminology of satisfiability modulo theories and then, in separate chapters, study decision procedures for each of the following theories: propositional logic; equalities and uninterpreted functions; linear arithmetic; bit vectors; arrays; pointer logic; and quantified formulas. They also study the problem of deciding combined theories and dedicate a chapter to modern techniques based on an interplay between a SAT solver and a decision procedure for the investigated theory.

This textbook has been used to teach undergraduate and graduate courses at ETH Zurich, at the Technion, Haifa, and at the University of Oxford. Each chapter includes a detailed bibliography and exercises. Lecturers' slides and a C++ library for rapid prototyping of decision procedures are available from the authors' website.

### What people are saying -Write a review

We haven't found any reviews in the usual places.

### Contents

 Introduction and Basic Concepts 1 11 Two Approaches to Formal Reasoning 3 112 Proof by Enumeration 4 113 Deduction and Enumeration 5 13 Normal Forms and Some of Their Properties 8 14 The Theoretical Point of View 14 141 The Problem We Solve 17 15 Expressiveness vs Decidability 18
 62 Deciding BitVector Arithmetic with Flattening 156 622 Arithmetic Operators 157 63 Incremental Bit Flattening 160 632 Enforcing Functional Consistency 162 64 Using Solvers for Linear Arithmetic 163 65 FixedPoint Arithmetic 165 652 Flattening 167 662 BitLevel Encodings of BitVector Arithmetic 168

 16 Boolean Structure in Decision Problems 19 17 Problems 21 18 Glossary 23 Decision Procedures for Propositional Logic 24 22 SAT Solvers 27 222 The DPLL Framework 28 223 BCP and the Implication Graph 30 224 Conflict Clauses and Resolution 35 225 Decision Heuristics 39 226 The Resolution Graph and the Unsatisfiable Core 41 Summary 42 23 Binary Decision Diagrams 43 232 Building BDDs from Formulas 46 24 Problems 50 243 Complexity 51 244 DPLL SAT Solving 52 246 Binary Decision Diagrams 53 25 Bibliographic Notes SAT 54 26 Glossary 57 Equality Logic and Uninterpreted Functions 59 312 Boolean Variables 60 321 How Uninterpreted Functions Are Used 61 Proving Equivalence of Programs 63 33 From Uninterpreted Functions to Equality Logic 64 331 Ackermanns Reduction 66 332 Bryants Reduction 69 34 Functional Consistency Is Not Enough 72 35 Two Examples of the Use of Uninterpreted Functions 74 351 Proving Equivalence of Circuits 75 352 Verifying a Compilation Process with Translation Validation 77 36 Problems 78 37 Glossary 79 Decision Procedures for Equality Logic and Uninterpreted Functions 81 42 Basic Concepts 83 43 Simplifications of the Formula 85 44 A GraphBased Reduction to Propositional Logic 88 45 Equalities and SmallDomain Instantiations 92 451 Some Simple Bounds 93 452 GraphBased Domain Allocation 94 453 The Domain Allocation Algorithm 96 454 A Proof of Soundness 98 455 Summary 101 47 Problems 103 472 Reductions 104 473 Complexity 105 474 Domain Allocation 106 49 Glossary 108 Linear Arithmetic 111 511 Solvers for Linear Arithmetic 112 52 The Simplex Algorithm 113 522 Basics of the Simplex Algorithm 114 523 Simplex with Upper and Lower Bounds 116 524 Incremental Problems 120 531 CuttingPlanes 122 54 FourierMotzkin Variable Elimination 126 543 Complexity 129 552 Equality Constraints 130 553 Inequality Constraints 132 56 Preprocessing 138 562 Preprocessing of Integer Linear Systems 139 57 Difference Logic 140 572 A Decision Procedure for Difference Logic 142 582 The Simplex Method 143 584 Omega Test 144 585 Difference Logic 145 510 Glossary 146 Bit Vectors 148 612 Notation 151 613 Semantics 152
 663 Using Solvers for Linear Arithmetic 169 68 Glossary 170 Arrays 171 72 Arrays as Uninterpreted Functions 172 73 A Reduction Algorithm for Array Logic 175 732 A Reduction Algorithm 176 74 Problems 178 76 Glossary 179 Pointer Logic 181 812 Dynamic Memory Allocation 182 813 Analysis of Programs with Pointers 184 82 A Simple Pointer Logic 185 822 Semantics 187 823 Axiomatization of the Memory Model 188 824 Adding Structure Types 189 83 Modeling HeapAllocated Data Structures 190 832 Trees 191 84 A Decision Procedure 193 842 Pure Variables 195 843 Partitioning the Memory 196 85 RuleBased Decision Procedures 197 851 A Reachability Predicate for Linked Structures 198 852 Deciding Reachability Predicate Formulas 199 86 Problems 202 862 Reachability Predicates 203 87 Bibliographic Notes 204 88 Glossary 206 Quantified Formulas 207 Quantified Boolean Formulas 209 Quantified Disjunctive Linear Arithmetic 211 922 Quantifier Elimination Algorithms 213 923 Quantifier Elimination for Quantified Boolean Formulas 214 924 Quantifier Elimination for Quantified Disjunctive Linear Arithmetic 217 93 SearchBased Algorithms for Quantified Boolean Formulas 218 94 Problems 220 95 Bibliographic Notes 223 96 Glossary 224 Deciding a Combination of Theories 225 103 The NelsonOppen Combination Procedure 227 1032 Combining Nonconvex Theories 230 1033 Proof of Correctness of the NelsonOppen Procedure 233 104 Problems 236 106 Glossary 239 Propositional Encodings 240 112 Lazy Encodings 244 1122 A Lazy Procedure for Building Propositional Encodings 245 1123 Integration into DPLL 246 1125 Some Implementation Details of DPLLT 250 113 Propositional Encodings with Proofs Advanced 253 1131 Encoding Proofs 254 1132 Complete Proofs 255 1133 Eager Encodings 257 1134 Criteria for Complete Proofs 258 1135 Algorithms for Generating Complete Proofs 259 114 Problems 263 115 Bibliographic Notes 264 116 Glossary 267 The SatisfiabilityModuloTheory Library and Standard SMTLIB 269 A C++ Library for Developing Decision Procedures 271 B2 Graphs and Trees 272 B21 Adding Payload 274 B32 The Problem File Format 276 B33 A Class for Storing Identifiers 277 B4 CNF and SAT 278 B42 Converting the Propositional Skeleton 281 References 284 Index 299 Copyright

### Popular passages

Page 288 - P. Cheeseman, B. Kanefsky, and WM Taylor. Where the really hard problems are.
Page 284 - C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality.
Page 284 - A. Armando and E. Giunchiglia. Embedding complex decision procedures inside an interactive theorem prover. Annals of Mathematics and Artificial Intelligence, 8(3-4):475-502, 1993.