| Introduction and Basic Concepts | p. 1 |
| Two Approaches to Formal Reasoning | p. 3 |
| Proof by Deduction | p. 3 |
| Proof by Enumeration | p. 4 |
| Deduction and Enumeration | p. 5 |
| Basic Definitions | p. 5 |
| Normal Forms and Some of Their Properties | p. 8 |
| The Theoretical Point of View | p. 14 |
| The Problem We Solve | p. 17 |
| Our Presentation of Theories | p. 17 |
| Expressiveness vs. Decidability | p. 18 |
| Boolean Structure in Decision Problems | p. 19 |
| Problems | p. 21 |
| Glossary | p. 23 |
| Decision Procedures for Propositional Logic | p. 25 |
| Propositional Logic | p. 25 |
| Motivation | p. 25 |
| SAT Solvers | p. 27 |
| The Progress of SAT Solving | p. 27 |
| The DPLL Framework | p. 28 |
| BCP and the Implication Graph | p. 30 |
| Conflict Clauses and Resolution | p. 35 |
| Decision Heuristics | p. 39 |
| The Resolution Graph and the Unsatisfiable Core | p. 41 |
| SAT Solvers: Summary | p. 42 |
| Binary Decision Diagrams | p. 43 |
| From Binary Decision Trees to ROBDDs | p. 43 |
| Building BDDs from Formulas | p. 46 |
| Problems | p. 50 |
| Warm-up Exercises | p. 50 |
| Modeling | p. 50 |
| Complexity | p. 51 |
| DPLL SAT Solving | p. 52 |
| Related Problems | p. 52 |
| Binary Decision Diagrams | p. 53 |
| Bibliographic Notes | p. 54 |
| Glossary | p. 57 |
| Equality Logic and Uninterpreted Functions | p. 59 |
| Introduction | p. 59 |
| Complexity and Expressiveness | p. 59 |
| Boolean Variables | p. 60 |
| Removing the Constants: A Simplification | p. 60 |
| Uninterpreted Functions | p. 60 |
| How Uninterpreted Functions Are Used | p. 61 |
| An Example: Proving Equivalence of Programs | p. 63 |
| From Uninterpreted Functions to Equality Logic | p. 64 |
| Ackermann's Reduction | p. 66 |
| Bryant's Reduction | p. 69 |
| Functional Consistency Is Not Enough | p. 72 |
| Two Examples of the Use of Uninterpreted Functions | p. 74 |
| Proving Equivalence of Circuits | p. 75 |
| Verifying a Compilation Process with Translation Validation | p. 77 |
| Problems | p. 78 |
| Warm-up Exercises | p. 78 |
| Problems | p. 78 |
| Glossary | p. 79 |
| Decision Procedures for Equality Logic and Uninterpreted Functions | p. 81 |
| Congruence Closure | p. 81 |
| Basic Concepts | p. 83 |
| Simplifications of the Formula | p. 85 |
| A Graph-Based Reduction to Propositional Logic | p. 88 |
| Equalities and Small-Domain Instantiations | p. 92 |
| Some Simple Bounds | p. 93 |
| Graph-Based Domain Allocation | p. 94 |
| The Domain Allocation Algorithm | p. 96 |
| A Proof of Soundness | p. 98 |
| Summary | p. 101 |
| Ackermann's vs. Bryant's Reduction: Where Does It Matter? | p. 101 |
| Problems | p. 103 |
| Conjunctions of Equalities and Uninterpreted Functions | p. 103 |
| Reductions | p. 104 |
| Complexity | p. 105 |
| Domain Allocation | p. 106 |
| Bibliographic Notes | p. 106 |
| Glossary | p. 108 |
| Linear Arithmetic | p. 111 |
| Introduction | p. 111 |
| Solvers for Linear Arithmetic | p. 112 |
| The Simplex Algorithm | p. 113 |
| Decision Problems and Linear Programs | p. 113 |
| Basics of the Simplex Algorithm | p. 114 |
| Simplex with Upper and Lower Bounds | p. 116 |
| Incremental Problems | p. 120 |
| The Branch and Bound Method | p. 120 |
| Cutting-Planes | p. 122 |
| Fourier-Motzkin Variable Elimination | p. 126 |
| Equality Constraints | p. 126 |
| Variable Elimination | p. 126 |
| Complexity | p. 129 |
| The Omega Test | p. 129 |
| Problem Description | p. 129 |
| Equality Constraints | p. 130 |
| Inequality Constraints | p. 132 |
| Preprocessing | p. 138 |
| Preprocessing of Linear Systems | p. 138 |
| Preprocessing of Integer Linear Systems | p. 139 |
| Difference Logic | p. 140 |
| Introduction | p. 140 |
| A Decision Procedure for Difference Logic | p. 142 |
| Problems | p. 142 |
| Warm-up Exercises | p. 142 |
| The Simplex Method | p. 143 |
| Integer Linear Systems | p. 143 |
| Omega Test | p. 144 |
| Difference Logic | p. 145 |
| Bibliographic Notes | p. 145 |
| Glossary | p. 146 |
| Bit Vectors | p. 149 |
| Bit-Vector Arithmetic | p. 149 |
| Syntax | p. 149 |
| Notation | p. 151 |
| Semantics | p. 152 |
| Deciding Bit-Vector Arithmetic with Flattening | p. 156 |
| Converting the Skeleton | p. 156 |
| Arithmetic Operators | p. 157 |
| Incremental Bit Flattening | p. 160 |
| Some Operators Are Hard | p. 160 |
| Enforcing Functional Consistency | p. 162 |
| Using Solvers for Linear Arithmetic | p. 163 |
| Motivation | p. 163 |
| Integer Linear Arithmetic for Bit Vectors | p. 163 |
| Fixed-Point Arithmetic | p. 165 |
| Semantics | p. 165 |
| Flattening | p. 167 |
| Problems | p. 167 |
| Semantics | p. 167 |
| Bit-Level Encodings of Bit-Vector Arithmetic | p. 168 |
| Using Solvers for Linear Arithmetic | p. 169 |
| Bibliographic Notes | p. 169 |
| Glossary | p. 170 |
| Arrays | p. 171 |
| Introduction | p. 171 |
| Arrays as Uninterpreted Functions | p. 172 |
| A Reduction Algorithm for Array Logic | p. 175 |
| Array Properties | p. 175 |
| A Reduction Algorithm | p. 176 |
| Problems | p. 178 |
| Bibliographic Notes | p. 178 |
| Glossary | p. 179 |
| Pointer Logic | p. 181 |
| Introduction | p. 181 |
| Pointers and Their Applications | p. 181 |
| Dynamic Memory Allocation | p. 182 |
| Analysis of Programs with Pointers | p. 184 |
| A Simple Pointer Logic | p. 185 |
| Syntax | p. 185 |
| Semantics | p. 187 |
| Axiomatization of the Memory Model | p. 188 |
| Adding Structure Types | p. 189 |
| Modeling Heap-Allocated Data Structures | p. 190 |
| Lists | p. 190 |
| Trees | p. 191 |
| A Decision Procedure | p. 193 |
| Applying the Semantic Translation | p. 193 |
| Pure Variables | p. 195 |
| Partitioning the Memory | p. 196 |
| Rule-Based Decision Procedures | p. 197 |
| A Reachability Predicate for Linked Structures | p. 198 |
| Deciding Reachability Predicate Formulas | p. 199 |
| Problems | p. 202 |
| Pointer Formulas | p. 202 |
| Reachability Predicates | p. 203 |
| Bibliographic Notes | p. 204 |
| Glossary | p. 206 |
| Quantified Formulas | p. 207 |
| Introduction | p. 207 |
| Example: Quantified Boolean Formulas | p. 209 |
| Example: Quantified Disjunctive Linear Arithmetic | p. 211 |
| Quantifier Elimination | p. 211 |
| Prenex Normal Form | p. 211 |
| Quantifier Elimination Algorithms | p. 213 |
| Quantifier Elimination for Quantified Boolean Formulas | p. 214 |
| Quantifier Elimination for Quantified Disjunctive Linear Arithmetic | p. 217 |
| Search-Based Algorithms for QBF | p. 218 |
| Problems | p. 220 |
| Warm-up Exercises | p. 220 |
| QBF | p. 220 |
| Bibliographic Notes | p. 223 |
| Glossary | p. 224 |
| Deciding a Combination of Theories | p. 225 |
| Introduction | p. 225 |
| Preliminaries | p. 225 |
| The Nelson-Oppen Combination Procedure | p. 227 |
| Combining Convex Theories | p. 227 |
| Combining Nonconvex Theories | p. 230 |
| Proof of Correctness of the Nelson-Oppen Procedure | p. 233 |
| Problems | p. 236 |
| Bibliographic Notes | p. 236 |
| Glossary | p. 239 |
| Propositional Encodings | p. 241 |
| Overview | p. 241 |
| Lazy Encodings | p. 244 |
| Definitions and Notations | p. 244 |
| Building Propositional Encodings | p. 245 |
| Integration into DPLL | p. 246 |
| Theory Propagation and the DPLL(T) Framework | p. 246 |
| Some Implementation Details of DPLL(T) | p. 250 |
| Propositional Encodings with Proofs (Advanced) | p. 253 |
| Encoding Proofs | p. 254 |
| Complete Proofs | p. 255 |
| Eager Encodings | p. 257 |
| Criteria for Complete Proofs | p. 258 |
| Algorithms for Generating Complete Proofs | p. 259 |
| Problems | p. 263 |
| Bibliographic Notes | p. 264 |
| Glossary | p. 267 |
| The SMT-LIB Initiative | p. 269 |
| A C++ Library for Developing Decision Procedures | p. 271 |
| Introduction | p. 271 |
| Graphs and Trees | p. 272 |
| Adding "Payload" | p. 274 |
| Parsing | p. 274 |
| A Grammar for First-Order Logic | p. 274 |
| The Problem File Format | p. 276 |
| A Class for Storing Identifiers | p. 277 |
| The Parse Tree | p. 277 |
| CNF and SAT | p. 278 |
| Generating CNF | p. 278 |
| Converting the Propositional Skeleton | p. 281 |
| A Template for a Lazy Decision Procedure | p. 281 |
| References | p. 285 |
| Index | p. 299 |
| Table of Contents provided by Ingram. All Rights Reserved. |