Decision Procedures: An Algorithmic Point of View / Edition 2

by Daniel Kroening, Ofer Strichman

Overview

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 SAT, Satisfiability Modulo Theories (SMT) and the DPLL(T) framework. Then, in separate chapters, they study decision procedures for 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 based on the Nelson-Oppen procedure.

Thefirst edition of this book was adopted as a textbook in courses worldwide. It was published in 2008 and the field now called SMT was then in its infancy, without the standard terminology and canonic algorithms it has now; this second edition reflects these changes. It brings forward the DPLL(T) framework. It also expands the SAT chapter with modern SAT heuristics, and includes a new section about incremental satisfiability, and the related Constraints Satisfaction Problem (CSP). The chapter about quantifiers was expanded with a new section about general quantification using E-matching and a section about Effectively Propositional Reasoning (EPR). The book also includes a new chapter on the application of SMT in industrial software engineering and in computational biology, coauthored by Nikolaj Bjørner and Leonardo de Moura, and Hillel Kugler, respectively.

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.

Product Details

ISBN-13:	9783662504963
Publisher:	Springer Berlin Heidelberg
Publication date:	11/23/2016
Series:	Texts in Theoretical Computer Science. An EATCS Series
Edition description:	2nd ed. 2016
Pages:	356
Product dimensions:	6.10(w) x 9.25(h) x (d)

About the Author

Daniel Kroening is a professor in the Dept. of Computer Science at the University of Oxford; his interests include automated verification, software engineering, and programming languages. Ofer Strichman is a professor in the faculty of industrial engineering and management at the Technion; his research interests include formal verification of software and hardware, and decision procedures for fragments of first-order logic.

Table of Contents

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

Editorial Reviews

From the reviews:

“The topic of this book is decision procedures for first-order theories … . it is one of the first to capture the essential concepts of SMT in a book. … relevant to those wishing to understand the area today. … the book more accessible to those without a strong background in mathematical logic.” (Clark Barrett, Journal of Automated Reasoning, Vol. 51, 2013)

"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)

"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 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." (ChristianPosthoff, Zentralblatt MATH, Vol. 1149, 2008)

From the Publisher