+612 9045 4394
Decision Procedures : An Algorithmic Point of View - Daniel Kroening

Decision Procedures

An Algorithmic Point of View


Published: 23rd May 2008
Ships: 15 business days
15 business days
RRP $128.99
or 4 easy payments of $24.85 with Learn more

Other Available Formats (Hide)

  • Paperback View Product Available: 10th February 2019
    Pre-Order Today. Ships in 1-2 business days after release

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.

From the reviews: "This book has two topics as main points: 'decision procedures' and 'algorithms to be applied for these decisions'. ... Such an approach is very useful for graduate students or students in year four or five ... . Each chapter introduces and explains a lot of different concepts and presents good examples, some problems and exercises with algorithm-based solutions, and a glossary at its end, which makes the book very applicable and readable. ... The book is very well written and interesting to read." (Christian Posthoff, Zentralblatt MATH, Vol. 1149, 2008) "There are a number of things that I like about the book. Although the material is often complex, the exposition is extremely clear, precise and meticulous. A definition is almost always followed by a clarifying example. As noted above, Kroening and Strichman go to great efforts to explain the notations used. In fact, I'd be hard pressed to think of another text on an advanced subject that does so much to make the material accessible to the reader." (K. Harrow, ACM Computing Reviews, September 2008) "This book is a developed version of classroom notes for a course on decision procedures, intended for undergraduate and graduate students ... . The developments are intended for programmers who need to know about the algorithms that solve their particular problems, as well as for students and researchers who need to know how to define such algorithms in the framework of appropriate logics. ... Overall, the book is well structured ... ." (Siva Anantharaman, Mathematical Reviews, Issue 2009 m)

Introduction and Basic Conceptsp. 1
Two Approaches to Formal Reasoningp. 3
Proof by Deductionp. 3
Proof by Enumerationp. 4
Deduction and Enumerationp. 5
Basic Definitionsp. 5
Normal Forms and Some of Their Propertiesp. 8
The Theoretical Point of Viewp. 14
The Problem We Solvep. 17
Our Presentation of Theoriesp. 17
Expressiveness vs. Decidabilityp. 18
Boolean Structure in Decision Problemsp. 19
Problemsp. 21
Glossaryp. 23
Decision Procedures for Propositional Logicp. 25
Propositional Logicp. 25
Motivationp. 25
SAT Solversp. 27
The Progress of SAT Solvingp. 27
The DPLL Frameworkp. 28
BCP and the Implication Graphp. 30
Conflict Clauses and Resolutionp. 35
Decision Heuristicsp. 39
The Resolution Graph and the Unsatisfiable Corep. 41
SAT Solvers: Summaryp. 42
Binary Decision Diagramsp. 43
From Binary Decision Trees to ROBDDsp. 43
Building BDDs from Formulasp. 46
Problemsp. 50
Warm-up Exercisesp. 50
Modelingp. 50
Complexityp. 51
DPLL SAT Solvingp. 52
Related Problemsp. 52
Binary Decision Diagramsp. 53
Bibliographic Notesp. 54
Glossaryp. 57
Equality Logic and Uninterpreted Functionsp. 59
Introductionp. 59
Complexity and Expressivenessp. 59
Boolean Variablesp. 60
Removing the Constants: A Simplificationp. 60
Uninterpreted Functionsp. 60
How Uninterpreted Functions Are Usedp. 61
An Example: Proving Equivalence of Programsp. 63
From Uninterpreted Functions to Equality Logicp. 64
Ackermann's Reductionp. 66
Bryant's Reductionp. 69
Functional Consistency Is Not Enoughp. 72
Two Examples of the Use of Uninterpreted Functionsp. 74
Proving Equivalence of Circuitsp. 75
Verifying a Compilation Process with Translation Validationp. 77
Problemsp. 78
Warm-up Exercisesp. 78
Problemsp. 78
Glossaryp. 79
Decision Procedures for Equality Logic and Uninterpreted Functionsp. 81
Congruence Closurep. 81
Basic Conceptsp. 83
Simplifications of the Formulap. 85
A Graph-Based Reduction to Propositional Logicp. 88
Equalities and Small-Domain Instantiationsp. 92
Some Simple Boundsp. 93
Graph-Based Domain Allocationp. 94
The Domain Allocation Algorithmp. 96
A Proof of Soundnessp. 98
Summaryp. 101
Ackermann's vs. Bryant's Reduction: Where Does It Matter?p. 101
Problemsp. 103
Conjunctions of Equalities and Uninterpreted Functionsp. 103
Reductionsp. 104
Complexityp. 105
Domain Allocationp. 106
Bibliographic Notesp. 106
Glossaryp. 108
Linear Arithmeticp. 111
Introductionp. 111
Solvers for Linear Arithmeticp. 112
The Simplex Algorithmp. 113
Decision Problems and Linear Programsp. 113
Basics of the Simplex Algorithmp. 114
Simplex with Upper and Lower Boundsp. 116
Incremental Problemsp. 120
The Branch and Bound Methodp. 120
Cutting-Planesp. 122
Fourier-Motzkin Variable Eliminationp. 126
Equality Constraintsp. 126
Variable Eliminationp. 126
Complexityp. 129
The Omega Testp. 129
Problem Descriptionp. 129
Equality Constraintsp. 130
Inequality Constraintsp. 132
Preprocessingp. 138
Preprocessing of Linear Systemsp. 138
Preprocessing of Integer Linear Systemsp. 139
Difference Logicp. 140
Introductionp. 140
A Decision Procedure for Difference Logicp. 142
Problemsp. 142
Warm-up Exercisesp. 142
The Simplex Methodp. 143
Integer Linear Systemsp. 143
Omega Testp. 144
Difference Logicp. 145
Bibliographic Notesp. 145
Glossaryp. 146
Bit Vectorsp. 149
Bit-Vector Arithmeticp. 149
Syntaxp. 149
Notationp. 151
Semanticsp. 152
Deciding Bit-Vector Arithmetic with Flatteningp. 156
Converting the Skeletonp. 156
Arithmetic Operatorsp. 157
Incremental Bit Flatteningp. 160
Some Operators Are Hardp. 160
Enforcing Functional Consistencyp. 162
Using Solvers for Linear Arithmeticp. 163
Motivationp. 163
Integer Linear Arithmetic for Bit Vectorsp. 163
Fixed-Point Arithmeticp. 165
Semanticsp. 165
Flatteningp. 167
Problemsp. 167
Semanticsp. 167
Bit-Level Encodings of Bit-Vector Arithmeticp. 168
Using Solvers for Linear Arithmeticp. 169
Bibliographic Notesp. 169
Glossaryp. 170
Arraysp. 171
Introductionp. 171
Arrays as Uninterpreted Functionsp. 172
A Reduction Algorithm for Array Logicp. 175
Array Propertiesp. 175
A Reduction Algorithmp. 176
Problemsp. 178
Bibliographic Notesp. 178
Glossaryp. 179
Pointer Logicp. 181
Introductionp. 181
Pointers and Their Applicationsp. 181
Dynamic Memory Allocationp. 182
Analysis of Programs with Pointersp. 184
A Simple Pointer Logicp. 185
Syntaxp. 185
Semanticsp. 187
Axiomatization of the Memory Modelp. 188
Adding Structure Typesp. 189
Modeling Heap-Allocated Data Structuresp. 190
Listsp. 190
Treesp. 191
A Decision Procedurep. 193
Applying the Semantic Translationp. 193
Pure Variablesp. 195
Partitioning the Memoryp. 196
Rule-Based Decision Proceduresp. 197
A Reachability Predicate for Linked Structuresp. 198
Deciding Reachability Predicate Formulasp. 199
Problemsp. 202
Pointer Formulasp. 202
Reachability Predicatesp. 203
Bibliographic Notesp. 204
Glossaryp. 206
Quantified Formulasp. 207
Introductionp. 207
Example: Quantified Boolean Formulasp. 209
Example: Quantified Disjunctive Linear Arithmeticp. 211
Quantifier Eliminationp. 211
Prenex Normal Formp. 211
Quantifier Elimination Algorithmsp. 213
Quantifier Elimination for Quantified Boolean Formulasp. 214
Quantifier Elimination for Quantified Disjunctive Linear Arithmeticp. 217
Search-Based Algorithms for QBFp. 218
Problemsp. 220
Warm-up Exercisesp. 220
QBFp. 220
Bibliographic Notesp. 223
Glossaryp. 224
Deciding a Combination of Theoriesp. 225
Introductionp. 225
Preliminariesp. 225
The Nelson-Oppen Combination Procedurep. 227
Combining Convex Theoriesp. 227
Combining Nonconvex Theoriesp. 230
Proof of Correctness of the Nelson-Oppen Procedurep. 233
Problemsp. 236
Bibliographic Notesp. 236
Glossaryp. 239
Propositional Encodingsp. 241
Overviewp. 241
Lazy Encodingsp. 244
Definitions and Notationsp. 244
Building Propositional Encodingsp. 245
Integration into DPLLp. 246
Theory Propagation and the DPLL(T) Frameworkp. 246
Some Implementation Details of DPLL(T)p. 250
Propositional Encodings with Proofs (Advanced)p. 253
Encoding Proofsp. 254
Complete Proofsp. 255
Eager Encodingsp. 257
Criteria for Complete Proofsp. 258
Algorithms for Generating Complete Proofsp. 259
Problemsp. 263
Bibliographic Notesp. 264
Glossaryp. 267
The SMT-LIB Initiativep. 269
A C++ Library for Developing Decision Proceduresp. 271
Introductionp. 271
Graphs and Treesp. 272
Adding "Payload"p. 274
Parsingp. 274
A Grammar for First-Order Logicp. 274
The Problem File Formatp. 276
A Class for Storing Identifiersp. 277
The Parse Treep. 277
CNF and SATp. 278
Generating CNFp. 278
Converting the Propositional Skeletonp. 281
A Template for a Lazy Decision Procedurep. 281
Referencesp. 285
Indexp. 299
Table of Contents provided by Ingram. All Rights Reserved.

ISBN: 9783540741046
ISBN-10: 3540741046
Series: Texts in Theoretical Computer Science. An EATCS Series
Audience: Professional
Format: Hardcover
Language: English
Number Of Pages: 306
Published: 23rd May 2008
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.5 x 15.5  x 2.29
Weight (kg): 0.68