内容提要 本书系统介绍了各种可判定的一阶理论及其在自动软硬件验证、定理证明与编译器优化等场景中的具体应用，涵盖了布尔可满足性（SAT）求解器和可满足性模理论（SMT）求解器的核心技术，以及命题逻辑、线性算术和位向量等多种建模语言。作者通过大量实际案例展示了如何将复杂的计算问题转化为形式化的逻辑问题，并借助高效的判定过程进行求解。本书不仅为研究人员提供了丰富的理论知识，还为高级软件工程师和开发者提供了实用的参考指南。 本书适合软件工程师、计算机专业的学生以及对逻辑推理感兴趣的读者阅读。

第1章 简介和基本概念
1.1 形式推理的两种方法
1.1.1 基于推演的证明
1.1.2 基于枚举的证明
1.1.3 推演与枚举
1.2 基本定义
1.3 范式及其属性
1.4 理论视角
1.4.1 我们求解的问题
1.4.2 如何介绍理论
1.5 表达能力与可判定性
1.6 逻辑公式的布尔结构
1.7 逻辑作为建模语言
1.8 习题
1.9 符号表
第2章 命题逻辑的判定过程
2.1 命题逻辑
2.2 SAT求解器
2.2.1 SAT求解器的历史
2.2.2 CDCL框架
2.2.3 布尔约束传播和蕴含图
2.2.4 学习子句与归结法
2.2.5 决策启发式
2.2.6 归结图和不可满足核
2.2.7 增量式可满足性问题
2.2.8 从SAT到CSP
2.2.9 SAT求解器：总结
2.3 习题
2.3.1 热身练习
2.3.2 命题逻辑
2.3.3 建模
2.3.4 复杂度
2.3.5 CDCL SAT求解
2.3.6 相关问题
2.4 文献注释
2.5 符号表
第3章 从命题逻辑到无量词理论
3.1 引言
3.2 DPLL（T）概述
3.3 形式化表达
3.4 理论传播和DPLL（T）框架
3.4.1 理论传播蕴含
3.4.2 性能，性能
3.4.3 返回蕴含赋值而非子句
3.4.4 生成强引理
3.4.5 即刻传播
3.5 习题
3.6 文献注释
3.7 符号表
第4章 带未解释函数的等式逻辑
4.1 引言
4.1.1 复杂度和表达能力
4.1.2 布尔变量
4.1.3 消除常数：一项化简技术
4.2 未解释函数
4.2.1 未解释函数的使用
4.2.2 一个例子：证明程序的等价性
……
第3章 从命题逻辑到无量词理论
第4章 带未解释函数的等式逻辑
第5章 线性算术
第6章 位向量
第7章 数组
第8章 指针逻辑
第9章 量化公式
第10章 判定理论组合公式
第11章 命题逻辑编码
第12章 判定过程在软件工程和计算生物学中的应用
附录A SMT-LIB：简介
附录B 判定过程的C++库
参考文献
工具索引
算法索引
索引