(click to enlarge)
Introduction and Basic Concepts
1.1 Two Approaches to Formal Reasoning
1.2 Basic Definitions
1.3 Normal Forms and Some of Their Properties
1.4 The Theoretical Point of View
1.5 Expressiveness vs. Decidability
1.6 Boolean Structure in Decision Problems
1.7 Logic as a Modeling Language
1.8 Problems
1.9 Glossary
Decision Procedures for Propositional Logic
2.1 Propositional Logic
2.2 SAT Solvers
2.3 Problems
2.4 Bibliographic Notes
2.5 Glossary
From Propositional to Quantifier-Free Theories
3.1 Introduction
3.2 An Overview of DPLL(T)
3.3 Formalization
3.4 Theory Propagation and the DPLL(T) Framework
3.5 Problems
3.6 Bibliographic Notes
3.7 Glossary
Equalities and Uninterpreted Functions
4.1 Introduction
4.2 Uninterpreted Functions
4.3 Congruence Closure
4.4 Functional Consistency Is Not Enough
4.5 Two Examples of the Use of Uninterpreted Functions
4.6 Problems
4.7 Bibliographic Notes
4.8 Glossary
Linear Arithmetic
5.1 Introduction
5.2 The Simplex Algorithm
5.3 The Branch and Bound Method
5.4 Fourier--Motzkin Variable Elimination
5.5 The Omega Test
5.6 Preprocessing
5.7 Difference Logic
5.8 Problems
5.9 Bibliographic Notes
5.10 Glossary
Bit Vectors
6.1 Bit-Vector Arithmetic
6.2 Deciding Bit-Vector Arithmetic with Flattening
6.3 Incremental Bit Flattening
6.4 Fixed-Point Arithmetic
6.5 Problems
6.6 Bibliographic Notes
6.7 Glossary
Arrays
7.1 Introduction
7.2 Eliminating the Array Terms
7.3 A Reduction Algorithm for a Fragment of the Array Theory
7.4 A Lazy Encoding Procedure
7.5 Problems
7.6 Bibliographic Notes
7.7 Glossary
Pointer Logic
8.1 Introduction
8.2 A Simple Pointer Logic
8.3 Modeling Heap-Allocated Data Structures
8.4 A Decision Procedure
8.5 Rule-Based Decision Procedures
8.6 Problems
8.7 Bibliographic Notes
8.8 Glossary
Quantified Formulas
9.1 Introduction
9.2 Quantifier Elimination
9.3 Search-Based Algorithms for QBF
9.4 Effectively Propositional Logic
9.5 General Quantification
9.6 Problems
9.7 Bibliographic Notes
9.8 Glossary
Deciding a Combination of Theories
10.1 Introduction
10.2 Preliminaries
10.3 The Nelson--Oppen Combination Procedure
10.4 Problems
10.5 Bibliographic Notes
10.6 Glossary
Propositional Encodings
11.1 Lazy vs. Eager Encodings
11.2 From Uninterpreted Functions to Equality Logic
11.3 The Equality Graph
11.4 Simplifications of the Formula
11.5 A Graph-Based Reduction to Propositional Logic
11.6 Equalities and Small-Domain Instantiations
11.7 Ackermann's vs. Bryant's Reduction: Where Does It Matter?
11.8 Problems
11.9 Bibliographic Notes
11.10 Glossary
Applications in Software Engineering and Computational Biology
12.1 Introduction
12.2 Bounded Program Analysis
12.3 Unbounded Program Analysis
12.4 SMT-Based Methods in Biology
12.5 Problems
12.6 Bibliographic Notes
SMT-LIB: a Brief Tutorial
A.1 The SMT-LIB Initiative
A.2 The SMT-LIB File Interface
A C++ Library for Developing Decision Procedures
B.1 Introduction
B.2 Graphs and Trees
B.3 Parsing
B.4 CNF and SAT
B.5 A Template for a Lazy Decision Procedure