Decision Procedures

by Kroening, Daniel; Strichman, Ofer; Bryant, Randal E.

• ISBN13: 9783540741046
• ISBN10: 3540741046
• Format: Hardcover
• Copyright: 2008-07-04
• Publisher: Springer-Nature New York Inc

Summary

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.

Table of Contents

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.