Daniel Kroening是牛津大学计算机科学系的教授，他的兴趣包括自动验证、软件工程和编程语言。

Ofer Strichman是以色列理工学院工业工程与管理学院的教授，他的研究兴趣包括软件和硬件的形式化验证，以及一阶逻辑片段的决策程序。

适读人群 ：本书适合软件工程师、计算机专业的学生以及对逻辑推理感兴趣的读者阅读

·填补空白：作为约束求解领域稀缺教材，适配学术研究与工程实践双重需求

·主创团队：牛津 / 以色列理工学院两位领域先驱合著，蔡少伟研究员倾力翻译，译文严谨贴合原著精髓

·案例实操：通过大量工业级案例演示复杂问题向逻辑模型的转化过程，助力理论落地应用

·内容多维：系统覆盖可判定一阶理论、SAT/SMT 求解核心算法与建模语言，兼顾理论深度与工程细节

·名家力荐：7 位国际国内院士、学会主席等联名推荐，认可其参考价值

第 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章量化公式196

91引言196

911例子：量化布尔公式198

912例子：量化析取线性算术199

92量词消去200

921前束范式200

922量词消去算法202

923量化布尔公式的量词消去203

924量化析取线性算术的量词消去206

93基于搜索的QBF算法207

94有效命题化逻辑210

95一般量化212

96习题219

961热身练习219

962QBF220

963EPR222

964一般量化222

97文献注释222

98词汇表224

第 10章判定理论组合公式225

101引言225

102预备知识225

103Nelson–Oppen过程227

1031凸理论的组合227

1032非凸理论的组合231

1033Nelson–Oppen过程的正确性证明233

104习题237

105文献注释238

106词汇表240

第 11章命题逻辑编码241

111惰性编码vs积极编码241

112从未解释函数到等式逻辑241

1121Ackermann归约242

1122Bryant归约245

113等式图249

114化简公式252

115基于图的命题逻辑归约255

116等式和小值域实例化258

1161一些简单的界259

1162基于图的域分配261

1163域分配算法262

1164可靠性证明265

1165总结268

117Ackermann归约vsBryant归约268

118习题270

1181归约271

1182域分配272

119文献注释273

1110词汇表275

第 12章判定过程在软件工程和计算生物上的应用277

121引言277

122有界程序分析279

1221检查单一路径的可行性279

1222检查有界程序中所有路径的可行性283

123无界程序分析285

1231使用非确定赋值的过近似285

1232过估计可能太粗糙287

1233循环不变式290

1234利用循环不变式对抽象进行细化292

124SMT方法在生物学中的应用294

1241DNA计算294

1242基因调控网络296

125习题298

1251热身练习298

1252有界符号模拟298

1253程序的过近似300

126文献注释301

ASMT-LIB：简介304

A1SMT库与标准304

A2SMT-LIB文件接口305

A21命题逻辑306

A22算术307

A23位向量算术308

A24数组309

A25等式理论和未解释函数309

B判定过程的C++库311

B1简介311

B2图和树312

B3解析314

B31一阶逻辑语法314

B32问题的文件格式316

B33存储标识符的类317

B34解析树317

B4CNF和SAT319

B41产生CNF319

B42解析命题骨架320

B5一个惰性判定过程模板321

参考文献323