内容简介
本书系统介绍了各种可判定的一阶理论及其在自动软件和硬件验证、定理证明与编译器优化等场景中的具体应用，涵盖了可满足性（SAT）求解器和可满足性模理论（SMT）求解器的核心技术，以及命题逻辑、线性算术和位向量等多种建模语言。作者通过大量实际案例展示了如何将复杂的计算问题转化为形式化的逻辑问题，并借助高效的判定过程进行求解。本书不仅为研究人员提供了丰富的理论知识，还为高级软件工程师和开发者提供了实用的参考指南。
本书适合软件工程师、计算机专业的学生以及对逻辑推理感兴趣的读者阅读。
目录
第 1版序
第 2版序
前言
第 1章简介和基本概念1
11形式推理的两种方法2
111基于推演的证明3
112基于枚举的证明4
113推演与枚举5
12基本定义5
13范式及其属性7
14理论视角14
141我们求解的问题17
142如何介绍理论18
15表达能力vs可判定性18
16逻辑公式的布尔结构20
17逻辑作为建模语言21
18习题23
19词汇表24
第 2章命题逻辑的判定过程25
21命题逻辑25
22SAT求解器27
221SAT求解的历史27
222CDCL框架29
223布尔约束传播和蕴含图30
224学习子句与归结法36
225决策启发式39
226归结图和不可满足核42
227增量式可满足性问题43
228从SAT到CSP44
229SAT求解器：总结46
23习题47
231预热练习47
232命题逻辑48
233建模48
234复杂度49
235CDCLSAT求解50
236相关问题51
24文献注释51
25词汇表55
第3章从命题逻辑到无量词理论56
31引言56
32DPLL(T)概述58
33形式化表达60
34理论传播和DPLL(T)框架64
341理论传播蕴含64
342性能，性……66
343返回蕴含赋值而非子句67
344生成强引理68
345即刻传播68
35习题69
36文献注释70
37词汇表72
第4章带未解释函数的等式逻辑73
41引言73
411复杂度和表达能力73412布尔变量74
413消除常数：一个化简技术74
42未解释函数74
421未解释函数的使用75
422一个例子：证明程序的等价性76
43通过等价闭包判定等式和未解释函数的合取公式80
44函数一致性不足以完成证明82
45未解释函数的两个应用例子84
451证明电路的等价性84
452通过翻译验证来验证编译过程86
46习题87
47文献注释89
48词汇表90
第5章线性算术91
51引言91
52单纯形法93
521范式93
522单纯形法基础94
523带上下界的单纯形法96
524增量式问题99
53分支限界方法100
54Fourier–Motzkin消元106
541等式约束106
542变量消除106
543复杂度109
55Omega测试109
551问题描述109
552等式约束110
553不等式约束113
56预处理118
561线性系统的预处理118
562整数线性系统的预处理119
57差分逻辑120
571引言120
572一个差分逻辑判定过程122
58习题123
581热身练习123
582单纯形法123
583整数线性系统124
584Omega测试124
585差分逻辑125
59文献注释126
510词汇表127
第6章位向量128
61位向量算术128
611语法128
612符号130
613语义131
62位向量算术的平展判定方法136
621转换骨架136
622算术运算137
63增量位平展140
631有些运算是难的140
632基于未解释函数进行抽象142
64定点算术142
641语义142
642平展144
65习题145
651语义145
652位向量算术的位级别变量145
653使用线性算术求解器146
66文献注释148
67词汇表149
第7章数组151
71引言151
711语法152
712语义153
72消除数组项154
73数组理论片段的归约算法155
731数组属性155
732归约算法157
74惰性编码过程159
741基于DPLL(T)的增量编码159
742读覆写公理的惰性实例化159
743外延规则的惰性实例化162
75习题164
76文献注释165
77词汇表166
第8章指针逻辑167
81引言167
811指针及其应用167
812动态内存分配169
813带指针程序分析169
82一个简单的指针逻辑171
821语法171
822语义173
823内存模型的公理化174
824增加结构类型175
83堆分配的数据结构建模176
831链表176
832树178
84一个判定过程180
841应用语义转换180
842纯变量182
843内存划分183
85基于规则的判定过程185
851链接型数据结构的可达性谓词185
852判定可达性谓词公式187
86习题190
861指针公式190
862可达性谓词191
87文献注释192
88词汇表194
第9章量化公式19
