Decision Procedures: An Algorithmic Point of View

Front Cover
Springer Science & Business Media, May 23, 2008 - Computers - 306 pages
0 Reviews

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

Other editions - View all

Common terms and phrases

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.

Bibliographic information