Muutke küpsiste eelistusi

Decision Procedures: An Algorithmic Point of View 2nd ed. 2016 [Kõva köide]

4.09/5 (11 hinnangut Goodreads-ist)
,
  • Formaat: Hardback, 356 pages, kõrgus x laius: 235x155 mm, kaal: 6919 g, 5 Illustrations, color; 59 Illustrations, black and white; XXI, 356 p. 64 illus., 5 illus. in color., 1 Hardback
  • Sari: Texts in Theoretical Computer Science. An EATCS Series
  • Ilmumisaeg: 27-Jan-2017
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • ISBN-10: 3662504960
  • ISBN-13: 9783662504963
Teised raamatud teemal:
  • Kõva köide
  • Hind: 71,86 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Tavahind: 84,54 €
  • Säästad 15%
  • Raamatu kohalejõudmiseks kirjastusest kulub orienteeruvalt 2-4 nädalat
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Tellimisaeg 2-4 nädalat
  • Lisa soovinimekirja
Decision Procedures: An Algorithmic Point of View 2nd ed. 2016Suurem pilt
  • Formaat: Hardback, 356 pages, kõrgus x laius: 235x155 mm, kaal: 6919 g, 5 Illustrations, color; 59 Illustrations, black and white; XXI, 356 p. 64 illus., 5 illus. in color., 1 Hardback
  • Sari: Texts in Theoretical Computer Science. An EATCS Series
  • Ilmumisaeg: 27-Jan-2017
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • ISBN-10: 3662504960
  • ISBN-13: 9783662504963
Teised raamatud teemal:
Püsilink: https://www.kriso.ee/db/9783662504963.html
Märksõnad:
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.

Arvustused

This is an excellent book, which I am delighted to have the chance to review. The text and the supporting material have been invaluable, stepping the reader through decision procedures and their combinations. I highly recommend the book to those interested in understanding and contributing to the world of SAT and SMT solving ... . (Rosemary Monahan, Formal Aspects of Computing, Vol. 30 (06), November, 2018)

1 Introduction and Basic Concepts
1(26)
1.1 Two Approaches to Formal Reasoning
3(2)
1.1.1 Proof by Deduction
3(1)
1.1.2 Proof by Enumeration
4(1)
1.1.3 Deduction and Enumeration
5(1)
1.2 Basic Definitions
5(3)
1.3 Normal Forms and Some of Their Properties
8(6)
1.4 The Theoretical Point of View
14(4)
1.4.1 The Problem We Solve
17(1)
1.4.2 Our Presentation of Theories
18(1)
1.5 Expressiveness vs. Decidability
18(2)
1.6 Boolean Structure in Decision Problems
20(2)
1.7 Logic as a Modeling Language
22(1)
1.8 Problems
23(1)
1.9 Glossary
24(3)
2 Decision Procedures for Propositional Logic
27(32)
2.1 Propositional Logic
27(2)
2.1.1 Motivation
27(2)
2.2 SAT Solvers
29(21)
2.2.1 The Progress of SAT Solving
29(2)
2.2.2 The CDCL Framework
31(1)
2.2.3 BCP and the Implication Graph
32(6)
2.2.4 Conflict Clauses and Resolution
38(4)
2.2.5 Decision Heuristics
42(3)
2.2.6 The Resolution Graph and the Unsatisfiable Core
45(1)
2.2.7 Incremental Satisfiability
46(2)
2.2.8 From SAT to the Constraint Satisfaction Problem
48(1)
2.2.9 SAT Solvers: Summary
49(1)
2.3 Problems
50(4)
2.3.1 Warm-up Exercises
50(1)
2.3.2 Propositional Logic
51(1)
2.3.3 Modeling
51(1)
2.3.4 Complexity
52(1)
2.3.5 CDCL SAT Solving
53(1)
2.3.6 Related Problems
54(1)
2.4 Bibliographic Notes
54(4)
2.5 Glossary
58(1)
3 From Propositional to Quantifier-Free Theories
59(18)
3.1 Introduction
59(2)
3.2 An Overview of DPLL(T)
61(3)
3.3 Formalization
64(2)
3.4 Theory Propagation and the DPLL(T) Framework
66(6)
3.4.1 Propagating Theory Implications
66(3)
3.4.2 Performance, Performance
69(1)
3.4.3 Returning Implied Assignments Instead of Clauses
70(1)
3.4.4 Generating Strong Lemmas
71(1)
3.4.5 Immediate Propagation
72(1)
3.5 Problems
72(1)
3.6 Bibliographic Notes
73(2)
3.7 Glossary
75(2)
4 Equalities and Uninterpreted Functions
77(20)
4.1 Introduction
77(2)
4.1.1 Complexity and Expressiveness
77(1)
4.1.2 Boolean Variables
78(1)
4.1.3 Removing the Constants: a Simplification
78(1)
4.2 Uninterpreted Functions
79(6)
4.2.1 How Uninterpreted Functions Are Used
80(1)
4.2.2 An Example: Proving Equivalence of Programs
81(4)
4.3 Congruence Closure
85(1)
4.4 Functional Consistency Is Not Enough
86(1)
4.5 Two Examples of the Use of Uninterpreted Functions
87(5)
4.5.1 Proving Equivalence of Circuits
89(2)
4.5.2 Verifying a Compilation Process with Translation Validation
91(1)
4.6 Problems
92(1)
4.7 Bibliographic Notes
93(2)
4.8 Glossary
95(2)
5 Linear Arithmetic
97(38)
5.1 Introduction
97(2)
5.1.1 Solvers for Linear Arithmetic
98(1)
5.2 The Simplex Algorithm
99(7)
5.2.1 A Normal Form
99(1)
5.2.2 Basics of the Simplex Algorithm
100(2)
5.2.3 Simplex with Upper and Lower Bounds
102(4)
5.3 The Branch and Bound Method
106(6)
5.3.1 Cutting Planes
108(4)
5.4 Fourier--Motzkin Variable Elimination
112(3)
5.4.1 Equality Constraints
112(1)
5.4.2 Variable Elimination
112(3)
5.4.3 Complexity
115(1)
5.5 The Omega Test
115(9)
5.5.1 Problem Description
115(1)
5.5.2 Equality Constraints
116(3)
5.5.3 Inequality Constraints
119(5)
5.6 Preprocessing
124(2)
5.6.1 Preprocessing of Linear Systems
124(1)
5.6.2 Preprocessing of Integer Linear Systems
125(1)
5.7 Difference Logic
126(3)
5.7.1 Introduction
126(2)
5.7.2 A Decision Procedure for Difference Logic
128(1)
5.8 Problems
129(2)
5.8.1 Warm-up Exercises
129(1)
5.8.2 The Simplex Method
129(1)
5.8.3 Integer Linear Systems
130(1)
5.8.4 Omega Test
130(1)
5.8.5 Difference Logic
131(1)
5.9 Bibliographic Notes
131(2)
5.10 Glossary
133(2)
6 Bit Vectors
135(22)
6.1 Bit-Vector Arithmetic
135(7)
6.1.1 Syntax
135(2)
6.1.2 Notation
137(1)
6.1.3 Semantics
138(4)
6.2 Deciding Bit-Vector Arithmetic with Flattening
142(4)
6.2.1 Converting the Skeleton
142(2)
6.2.2 Arithmetic Operators
144(2)
6.3 Incremental Bit Flattening
146(3)
6.3.1 Some Operators Are Hard
146(2)
6.3.2 Abstraction with Uninterpreted Functions
148(1)
6.4 Fixed-Point Arithmetic
149(2)
6.4.1 Semantics
149(1)
6.4.2 Flattening
150(1)
6.5 Problems
151(3)
6.5.1 Semantics
151(1)
6.5.2 Bit-Level Encodings of Bit-Vector Arithmetic
152(1)
6.5.3 Using Solvers for Linear Arithmetic
152(2)
6.6 Bibliographic Notes
154(2)
6.7 Glossary
156(1)
7 Arrays
157(16)
7.1 Introduction
157(2)
7.1.1 Syntax
158(1)
7.1.2 Semantics
159(1)
7.2 Eliminating the Array Terms
159(3)
7.3 A Reduction Algorithm for a Fragment of the Array Theory
162(3)
7.3.1 Array Properties
162(1)
7.3.2 The Reduction Algorithm
163(2)
7.4 A Lazy Encoding Procedure
165(4)
7.4.1 Incremental Encoding with DPLL(T)
165(1)
7.4.2 Lazy Instantiation of the Read-Over-Write Axiom
165(2)
7.4.3 Lazy Instantiation of the Extensionality Rule
167(2)
7.5 Problems
169(1)
7.6 Bibliographic Notes
170(1)
7.7 Glossary
171(2)
8 Pointer Logic
173(26)
8.1 Introduction
173(4)
8.1.1 Pointers and Their Applications
173(1)
8.1.2 Dynamic Memory Allocation
174(2)
8.1.3 Analysis of Programs with Pointers
176(1)
8.2 A Simple Pointer Logic
177(5)
8.2.1 Syntax
177(2)
8.2.2 Semantics
179(1)
8.2.3 Axiomatization of the Memory Model
180(1)
8.2.4 Adding Structure Types
181(1)
8.3 Modeling Heap-Allocated Data Structures
182(3)
8.3.1 Lists
182(1)
8.3.2 Trees
183(2)
8.4 A Decision Procedure
185(4)
8.4.1 Applying the Semantic Translation
185(2)
8.4.2 Pure Variables
187(1)
8.4.3 Partitioning the Memory
188(1)
8.5 Rule-Based Decision Procedures
189(5)
8.5.1 A Reachability Predicate for Linked Structures
190(1)
8.5.2 Deciding Reachability Predicate Formulas
191(3)
8.6 Problems
194(2)
8.6.1 Pointer Formulas
194(1)
8.6.2 Reachability Predicates
195(1)
8.7 Bibliographic Notes
196(2)
8.8 Glossary
198(1)
9 Quantified Formulas
199(30)
9.1 Introduction
199(4)
9.1.1 Example: Quantified Boolean Formulas
201(2)
9.1.2 Example: Quantified Disjunctive Linear Arithmetic
203(1)
9.2 Quantifier Elimination
203(7)
9.2.1 Prenex Normal Form
203(2)
9.2.2 Quantifier Elimination Algorithms
205(1)
9.2.3 Quantifier Elimination for Quantified Boolean Formulas
206(3)
9.2.4 Quantifier Elimination for Quantified Disjunctive Linear Arithmetic
209(1)
9.3 Search-Based Algorithms for QBF
210(2)
9.4 Effectively Propositional Logic
212(3)
9.5 General Quantification
215(7)
9.6 Problems
222(3)
9.6.1 Warm-up Exercises
222(1)
9.6.2 QBF
223(1)
9.6.3 EPR
224(1)
9.6.4 General Quantification
224(1)
9.7 Bibliographic Notes
225(2)
9.8 Glossary
227(2)
10 Deciding a Combination of Theories
229(16)
10.1 Introduction
229(1)
10.2 Preliminaries
229(2)
10.3 The Nelson--Oppen Combination Procedure
231(9)
10.3.1 Combining Convex Theories
231(3)
10.3.2 Combining Nonconvex Theories
234(3)
10.3.3 Proof of Correctness of the Nelson--Oppen Procedure
237(3)
10.4 Problems
240(1)
10.5 Bibliographic Notes
240(4)
10.6 Glossary
244(1)
11 Propositional Encodings
245(36)
11.1 Lazy vs. Eager Encodings
245(1)
11.2 From Uninterpreted Functions to Equality Logic
245(8)
11.2.1 Ackermann's Reduction
246(3)
11.2.2 Bryant's Reduction
249(4)
11.3 The Equality Graph
253(2)
11.4 Simplifications of the Formula
255(4)
11.5 A Graph-Based Reduction to Propositional Logic
259(3)
11.6 Equalities and Small-Domain Instantiations
262(10)
11.6.1 Some Simple Bounds
263(2)
11.6.2 Graph-Based Domain Allocation
265(1)
11.6.3 The Domain Allocation Algorithm
266(3)
11.6.4 A Proof of Soundness
269(2)
11.6.5 Summary
271(1)
11.7 Ackermann's vs. Bryant's Reduction: Where Does It Matter?
272(1)
11.8 Problems
273(3)
11.8.1 Reductions
274(2)
11.8.2 Domain Allocation
276(1)
11.9 Bibliographic Notes
276(3)
11.10 Glossary
279(2)
12 Applications in Software Engineering and Computational Biology
281(28)
12.1 Introduction
281(2)
12.2 Bounded Program Analysis
283(6)
12.2.1 Checking Feasibility of a Single Path
283(4)
12.2.2 Checking Feasibility of All Paths in a Bounded Program
287(2)
12.3 Unbounded Program Analysis
289(8)
12.3.1 Overapproximation with Nondeterministic Assignments
289(2)
12.3.2 The Overapproximation Can Be Too Coarse
291(3)
12.3.3 Loop Invariants
294(1)
12.3.4 Refining the Abstraction with Loop Invariants
295(2)
12.4 SMT-Based Methods in Biology
297(5)
12.4.1 DNA Computing
298(2)
12.4.2 Uncovering Gene Regulatory Networks
300(2)
12.5 Problems
302(2)
12.5.1 Warm-up Exercises
302(1)
12.5.2 Bounded Symbolic Simulation
302(1)
12.5.3 Overapproximating Programs
303(1)
12.6 Bibliographic Notes
304(5)
A SMT-LIB: a Brief Tutorial
309(6)
A.1 The SMT-LIB Initiative
309(1)
A.2 The SMT-LIB File Interface
310(5)
A.2.1 Propositional Logic
311(1)
A.2.2 Arithmetic
312(1)
A.2.3 Bit-Vector Arithmetic
313(1)
A.2.4 Arrays
313(1)
A.2.5 Equalities and Uninterpreted Functions
314(1)
B A C++ Library for Developing Decision Procedures
315(14)
B.1 Introduction
315(1)
B.2 Graphs and Trees
316(2)
B.2.1 Adding "Payload"
318(1)
B.3 Parsing
318(4)
B.3.1 A Grammar for First-Order Logic
318(2)
B.3.2 The Problem File Format
320(1)
B.3.3 A Class for Storing Identifiers
321(1)
B.3.4 The Parse Tree
321(1)
B.4 CNF and SAT
322(3)
B.4.1 Generating CNF
322(3)
B.4.2 Converting the Propositional Skeleton
325(1)
B.5 A Template for a Lazy Decision Procedure
325(4)
References 329(18)
Tools Index 347(2)
Algorithms Index 349(2)
Index 351
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.