Decision Procedures
An Algorithmic Point of View
Foreword to the first edition
刚开始阅读的时候没注意，第二遍阅读的时候发现foreword是Randal E. Bryant写的，就觉得这个名字很熟悉，好像是CS:APP的作者。上网一搜果然是CS:APP作者之一。Google Scholar显示他的研究方向是：Formal verification 和 binary decision diagrams。
Foreword to the second edition
Preface
A decision procedure is an algorithm that, given a decision problem, terminates with a correct yes.no answer.
Satisfiability Modulo Theories(SMT)
SMT solver: software that solves SMT formulas.
Which Theories? Which Algorithms?
The Structure and Nature of This Book
1 Introduction and Basic Concepts
The list includes the theories of bit vectors, arrays, and pointer logic, which are necessary components in the field of software formal verification.
1.1 Two Approaches to Formal Reasoning
The primary problem: the validity (or satisfiability) of a given formula.
Two fundamental strategies:
- The proof-theoretic approach is to use a duductive mechanism of reasoning, based on axioms and inference rules, which together are called an inference system.
- The model-theoretic approach is to enumerate possible solutions from a finite number of candidates.
Two directions: deduction and enumeration
1.1.1 Proof by Deduction
the system is called:
- sound: whether everything that can be proven with a given inference system is indeed valid
- complete: whether there exists a proof of validity using the inference system for every valid formula
1.1.2 Proof by Enumeration
1.1.3 Deduction and Enumeration
In practice, many decisiion procedures are not based on explicit use of either enumeration or deduction.
1.2 Basic Definitions
Definition 1.1 (assignment)
Definition 1.2 (satisfiability, validity, and contradiction).
-
A formula is satisfiable
if there exists an assignment of its variables under which the formula evluates to TRUE.
-
A formula is a contradiction if it is not satisfiable.
A formula is valid (also called a tautology) if it evaluates to TRUE under all assignments.