判定过程 SAT与SMT求解算法 第2版

·填补空白：作为约束求解领域稀缺教材，适配学术研究与工程实践双重需求
·主创团队：牛津 / 以色列理工学院两位领域先驱合著，蔡少伟研究员倾力翻译，译文严谨贴合原著精髓
·案例实操：通过大量工业级案例演示复杂问题向逻辑模型的转化过程，助力理论落地应用
·内容多维：系统覆盖可判定一阶理论、SAT/SMT 求解核心算法与建模语言，兼顾理论深度与工程细节
·名家力荐：7 位国际国内院士、学会主席等联名推荐，认可其参考价值

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

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

丹尼尔·克勒宁（Daniel Kroening），AWS高级首席科学家，生成式AI初创公司 Diffblue 的联合创始人，曾任牛津大学计算机科学系教授，研究兴趣包括自动验证、软件工程和编程语言。

奥弗·施特里希曼（Ofer Strichman），以色列理工学院数据与决策科学系教授，现任该校计算方向副主任，主要研究形式化验证、SAT/SMT求解器、程序等价性验证等，曾获2021年CAV奖。

蔡少伟，中国科学院软件研究所研究员，国内约束求解领域领军人物。多次夺得国际 SAT与SMT比赛冠军，在 CAV、CP、SAT等顶级会议获得最佳论文与杰出论文奖，担任相关国际顶级会议程序委员会主席。其研发的求解器应用于芯片验证、操作系统验证及工业调度。

第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 求解器

……