蔡少伟研究员倾力翻译国际经典《判定过程：SAT与SMT求解算法（第2版）》中文版，填补中文教材空白，为国内形式化验证与约束求解领域发展注入新动力。权威教材，不容错过！
原文标题：约束求解领域大佬蔡少伟倾力翻译，这本全球经典教材终于有了中文版！
原文作者：图灵编辑部
冷月清谈：
该书核心介绍布尔可满足性（SAT）问题和可满足性模理论（SMT）问题的求解算法，这两者是计算机科学的核心问题，也是符号主义AI的代表性技术，在现代计算机系统可靠性与安全性中扮演着重要角色。蔡少伟研究员强调，特别是2000年后SMT求解算法获得了长足发展，而本书系统覆盖了不同背景理论的SMT求解算法及SAT主要算法，填补了国内技术教材的空白，这正是选择翻译此书而非另行编著的重要原因。
《判定过程：SAT与SMT求解算法（第2版）》汇集了牛津大学和以色列理工学院两位领域先驱的智慧，并经过蔡少伟研究员的严谨翻译与校阅团队的精益求精，确保了译文的专业性与准确性。它不仅记录了该领域的发展脉络，更系统地深入探讨了判定过程背后的思想、工程方法，以及理论、工程与工具如何紧密结合以实现高性能。该教材不仅适配学术研究需求，也通过大量工业级案例演示了复杂问题向逻辑模型的转化过程，助力理论落地应用，因此获得了多位国际国内院士与专家的联名推荐，被公认为形式化方法领域不可或缺的参考读物。
怜星夜思：
2、文章里提到了SAT/SMT在芯片验证、操作系统验证等工业领域有很多应用，还说是符号主义AI的代表技术。现在AI这么火，大家觉得SAT/SMT未来还能在哪些新兴领域发挥作用？有没有可能跟现在的生成式AI结合起来，解决一些‘幻觉’问题？
3、书里强调高性能不只依赖好算法，更取决于理论、工程与工具的紧密结合。对于SAT/SMT这类技术来说，大家觉得理论研究、工程实践和工具开发三者之间，哪一个环节最考验人？或者说，哪个部分更能体现研究者的综合能力？
原文内容
在形式化验证、逻辑推理、SAT/SMT 求解这些听起来有点硬核的领域里，有一位始终站在前沿的中国学者——蔡少伟，他是中国科学院软件研究所研究员，国内约束求解领域领军人物。多年来，他带领团队多次在国际 SAT 与 SMT 比赛中获奖，并将其研发的求解器应用于芯片验证、操作系统验证及工业调度等关键工程实践。
这一次，他决定做一件特别的事，将这本由国际顶尖学者合著的、被全球学界公认为约束求解领域权威教材的Decision Procedures: An Algorithmic Point of View，Second Edition 带给中文读者。他希望通过这次翻译，让更多对约束求解感兴趣的读者，能有机会系统地了解这一领域的理论与方法。
正如他在序中所写：“希望能为这一方向在中国的发展做一点微小的贡献。”
下文是蔡少伟研究员为中文版特别撰写的序言。希望他的思考与经验，能让你在阅读本书时获得更多启发。
在计算机的数学基础中，数理逻辑可以说是基础中的基础，主要包含命题逻辑和一阶逻辑。可满足性问题是数理逻辑的核心问题，其目标是判定是否存在一组变量赋值，使得给定公式的结果为真，简单地说，就是判断一个逻辑公式是否包含矛盾。很多问题其实都属于这类问题，比如计算机硬件或软件有没有漏洞，某个规划任务有没有可行方案。这本书介绍了布尔可满足性 (SAT) 问题和可满足性模理论 (SMT) 问题的求解算法，分别对应命题逻辑和给定背景理论的一阶逻辑公式的可满足性问题。
可满足性问题是计算机科学的核心问题之一。同时，可满足性判定作为自动推理的主要方法，也是符号主义 AI 的代表性技术。从芯片设计到操作系统，从基础软件到工业软件，从密码分析到航空航天，SAT/SMT 求解器在很多重要领域发挥着重要作用。
2022 年和 2023 年，为了普及相关方向，我和吴志林研究员组织了两次“约束求解”公开课，报名的学员来自 100 多个单位，包括各大高校和著名企业。其中，2023 年线上听课人数超过 1000 人，引起了很好的反响。
在此过程中，我经常被问到一个问题：“这个领域有没有相关的中文教材？”这时我也意识到了一本中文教材的重要意义。我自己在本科期间刚接触这个领域的时候，读了中国科学院软件研究所张健研究员的《逻辑公式的可满足性判定一方法、工具及应用》一书( 2000 年出版)，受益匪浅。
这些年来，这个领域取得了长足的发展，特别是大部分 SMT 求解算法是在 2000 年之后发展起来的。然而，目前仍缺乏系统介绍这些算法技术的中文教材。我也想过自己编写一本介绍 SAT/SMT 算法的教材，但受限于能力和精力，恐怕短期内难以完成这一任务。再者，国际上已经有很好的教材，其中我认为最好的一本是Decision Procedures: An Algorithmic Point of View, Second Edition ,它覆盖了不同背景理论的 SMT 求解算法，也介绍了 SAT 最主要的算法。于是我决定将这本教材翻译成中文，希望能为此方向在中国的发展做一点微小的贡献。
在本书的翻译过程中，我有幸得到了多位朋友的帮助。感谢贺飞、马菲菲、吴志林、李博涵、韩瑞、吕昆航、师朗辰、贾富琦、董弈伯、张枨宇、何德源、郝政伟、刘柯蓝、杨子腾、赵启元、吴熙炜、戴佳妮等人对本书进行了校阅。
感谢原书作者 Ofer Strichman 对译者序细节的严格要求，这极大地帮助我们进一步提升了质量。感谢编辑王军花的耐心和各种帮助。在翻译过程中，我根据原书的勘误做了更正，对某些明显的不当之处也做了更正，并且得到了作者的认可。限于译者水平，翻译不妥之处在所难免，敬请读者谅解和指正。
蔡少伟
2025年夏于北京市中关村
判定过程的研究仍在飞速发展，每年都有新工具和新算法问世。但正如书中强调的，真正的高性能并不只依赖某个好算法，而是取决于理论、工程与工具的紧密结合。
这正是本书的价值所在，它不仅记录了一个领域的发展脉络，更让你理解判定过程背后的思想与工程方法。
如果你想了解自动推理如何支撑现代计算机系统的可靠性与安全性，或者需要一本系统、全面、权威的教材来学习判定过程，那么这本书无疑是最值得选择的经典。
系统覆盖可判定一阶理论、SAT/SMT 求解核心算法与建模语言，兼顾理论深度与工程细节。通过大量工业级案例演示复杂问题向逻辑模型的转化过程，助力理论落地应用，7 位国际国内院士、学会主席等联名推荐，认可其参考价值。
逻辑推理的判定过程，是自动推理技术革命的核心。这场革命已在工业领域展现出广泛应用，从硬件与软件验证，到云服务正确性的保障，乃至更多关键领域。有人认为，这些技术将在解决生成式机器学习模型的“幻觉”问题上发挥关键作用。本书是该领域最有价值的入门读物。两位作者作为自动推理领域的先驱和知名专家，不仅对最重要的方法提供了算法细节，还深入探讨了其背后的逻辑与计算基础，最后介绍了这些技术的应用场景。对于任何想了解这一前沿方向的读者而言，本书都是不可或缺的读物。如今，其中文版得以问世，我深感欣喜。
——Armin Biere，德国弗赖堡大学计算机体系结构讲席教授、国际SAT学会前任主席
这本经典著作是最早也是至今唯一的系统阐述可满足性模理论（SMT）核心概念的教材。更重要的是，其内容至今仍对想要了解该领域的读者具有极高的参考价值。书中几乎涵盖了现代 SMT 求解相关的所有重要主题，尤其侧重算法解析与实例演示，这一特点使得不同背景的读者都能轻松理解书中内容。
——Clark Barrett，斯坦福大学计算机系教授、著名自动推理专家、ACM会士
在过去的 25 年里，SMT 已成为自动推理领域的领先技术。由该领域两位前沿研究人员丹尼尔·克勒宁和奥弗·施特里希曼所著的《判定过程：SAT 与 SMT 求解算法（第2版）》是这一重要领域的权威教科书。我很高兴看到蔡少伟研究员将此书翻译成中文，让中国的本科生和研究生能够接触到这部重要著作。
——Moshe Vardi，美国莱斯大学计算工程系杰出教授、著名形式化方法专家、美国国家科学院/美国国家工程院/美国艺术与科学院院士
在我的大脑中，经常会出现两个声音：一个推崇科学之美，另一个推崇极致工程。在我的认知中，可判定的一阶理论以及 SAT 与 SMT 求解器，正是计算机领域中一座连接科学与工程的桥梁。蔡少伟研究员是约束求解方向的顶尖学者，其倾力翻译的《判定过程：SAT与SMT求解算法（第2版）》这本经典著作，系统地介绍了这个方向的基础理论、重要算法、核心技术以及具体应用，必将会促进该方向在国内的发展，意义深远。值得一提的是，书中每一章最后专门讲述了相关知识的演进脉络与幕后故事，其中蕴藏着科学技术发展的内在规律，极富启发性。
——包云岗，中国科学院计算技术研究所副所长、中国科学院大学计算机学院副院长
本书系统介绍了可判定一阶理论及其应用，是该领域不可多得的优秀教材。我国约束求解专家蔡少伟研究员将该书倾力翻译为中文，具有深远意义。强烈推荐所有形式化方法领域的研究者、技术开发者以及相关工程应用人员学习和参考。
——王戟，国防科技大学研究员、CCF 形式化方法专业委员会前任主任
本书由国际知名学者丹尼尔·克勒宁与奥弗·施特里希曼合著，是计算机科学领域的一本经典教材。该书从算法视角系统地介绍了一阶理论的可判定性问题，聚焦 SAT 与 SMT 求解器的核心技术，通过大量实际场景甚至工业级的案例展现了算法和求解器在应用中的威力。无论是对于计算机专业学生、算法工程师，还是对形式化验证感兴趣的研究人员来说，该书都是一本关于 SAT与 SMT 求解的涵盖理论、算法和工程落地的重要参考书。蔡少伟研究员以深厚的学术功底和对 SAT 与 SMT 求解的深刻洞见，把握原著精髓，译文严谨流畅，为国内读者提供了一个快捷进入该领域前沿的途径。
——夏壁灿，北京大学数学科学学院教授
SAT 是计算机科学和人工智能领域的重要基础问题之一。自 20 世纪末以来，SAT 求解算法取得了巨大进步。SMT 是其扩展，能接受更加丰富的约束形式。SAT 和 SMT 求解算法及工具推动了软件分析、测试和验证的发展。本书是较早介绍 SAT 和 SMT 求解技术的专著，在国际上有重要影响，虽然不是尽善尽美，但有助于读者深入了解该领域。我相信，该书中文版的出版，将吸引更多的国内学者加入这一领域，或使用该领域的成果。
——张健，中国科学院软件研究所研究员、CCF 会士
