蔡少伟清晰地记得，2011年夏天他去美国密歇根大学安娜堡分校参加 SAT 会议时，一眼望去，全场只有他一个中国人。

参会人员一半来自欧洲，四分之一来自北美（尤其是美国），另外四分之一则来自亚太地区。他将自己的“单刀赴会”列为 SAT 2011一行的两大记忆点之一，另一点是那年大会主席的论文被 SAT 评委“枪毙”了。

这是蔡少伟第一次参加 SAT。这个被 CCF 列为 B 类的会议全称为“International Conference on Theory and Applications of Satisfiability Testing”（可满足性判定的理论与应用国际会议），始设于1997年，主要面向研究可满足性问题，尤其是布尔可满足性（Boolean Satisfiability Problem，简称“SAT”）问题的科研人员，向来少为中国学者问津。

不过，蔡少伟似乎对这份“孤军作战”的寂寞也早已见惯不惯。当时，他在北京大学计算机系的理论实验室攻读博士，师从苏开乐，是当时组里唯一一位研究 SAT 求解算法的人。作为数理逻辑基础问题又是NP完全问题，SAT 求解同时注重符号推理与算法设计，还需要巧妙的数据结构和精致的代码实现，难度极高。

同样经历过“四下无人”的少数者，还有 2009 年从斯坦福毕业回国的葛冬冬。那一年，他从斯坦福大学管理科学与工程系（MS&E）取得运筹学博士学位，拿到了上海交通大学的教职 offer，准备回国任教。

读博期间，他师从运筹学泰斗、冯·诺依曼理论奖的唯一华人获奖者叶荫宇，主要研究大规模优化理论与算法，并不直接研究求解器，只是在研究某些整数规划的问题时经常需要调用。但回国后，他却发现，国内居然没有人开发商用求解器。凡是需要用到求解器的企业，都是直接购买美国的 CPLEX、GUROBI 与 XPRESS。

“求解器分为专业版、个人版与商用版，不同版本有不同的价格，5万到40万人民币不等。”葛冬冬谈道，“中国没有求解器，要从国外买，人家不可能给你降低价格。如果买几千台的话，几个亿的外汇就这样出去了。”

看到国内在求解器研究上的空白，葛冬冬感到很奇怪：为什么没有人做？但那时，他刚步入教职不久，身兼数职，也没有条件去作更多的研究。直到2013年，他从交大转到上海财经大学、担任交叉科学研究院院长，有机会组建自己的团队，才开始带队探索。

十年过去，再回头看，从无人区走出来的蔡少伟与葛冬冬，都已成为国内研究求解器的青年先驱人物。但是，谈起求解器的研究现状，他们的结论仍与十年前无异，“就一小撮人”。

事实上，在深度学习兴起之前，人工智能十分注重逻辑推理（reasoning），当时偏符号主义的 SAT 问题比深度学习还流行。

从“解题”的角度看，一切人工智能系统都可以归结为“问题求解”（Problem Solving）系统，即为了实现给定目标而展开的动作序列的过程。而解决特定问题的算法，被称为“求解器”（solver）。无论是 SAT 求解器，还是整数规划求解器，都是经典的离散约束算法问题。

求解器在工业发展中的意义非凡。例如，中国战略布局上亟待解决的“卡脖子”难题 EDA （电子设计自动化）需要用到 SAT 求解器进行快速验证，而制造、物流与供应链优化等则需要用到整数规划求解器（尤其是线性规划求解器）。因此，近两年，华为与阿里也开始布局求解器研究。

江湖传闻，华为内部对求解器研究十分重视，多个海内外团队同时推进，任总直接听取汇报。由于人才供给紧缺，蔡少伟所培养的博士毕业生入职华为后，待遇直接对标“华为天才少年”，年薪近百万。

探讨 SAT 求解器之前，我们首先要了解 SAT 问题的研究历史。

说来牛叉，SAT 问题是计算机历史上第一个被证明为 NP-Complete 的问题，其主要贡献者就是计算复杂理论研究方向的大神、现任多伦多大学计算机系与数学系的教授 Stephen A. Cook。

在1971年的论文“The Complexity of Theorem Proving Procedures”中，Stephen Cook 提出了著名的库克定理（Cook Theorem），从图灵机的角度证明所有 NP 问题都可以快速转化为 SAT 问题。

在库克定理里，图灵机的计算过程可以用 SAT 表达出来，转化成一条条独立的语句，十分简单，但又极高效。库克定理指出，如果 SAT 问题可以快速求解，那么所有 NP 问题都可以快速求解。Cook 本人也因此获得 1982 年图灵奖。

广义上，可满足性（Satisfiability）问题是指对给定逻辑公式判定是否可满足的问题。SAT问题特指“布尔可满足性问题”，又称“命题逻辑可满足性问题”。命题逻辑是形式逻辑最基本的类别，基本元素是布尔变元。每个布尔变元代表一个基本命题。SAT 问题的本质，是探求一大堆布尔变元之间的逻辑推理关系是否成立。

听起来很高深，但描述十分简单。举个例子：

甲乙丙想参会，甲说：乙参会我就参会，乙说：丙参会我就参会，而丙说：甲参会我就不参会，那么能不能同时满足甲乙丙的参会需求？

这就是一个 SAT 问题，而求解的答案是：他们的需求是不可（同时）满足的。如果命题简单，那么人脑可以很快判定逻辑推理关系是否成立。但随着布尔变元和约束的条件越来越多，SAT 的求解就会越来越难，需要借助算法来进行推理与计算。

比方说，在进行机场飞机调度时，研究人员要考虑的状态非常多，包括待起飞的飞机数量，飞机分布的跑道数量与位置，飞机的运行方向，风向等等。一个布尔变元表示单一时空下的一种状态。由此可见，布尔变元所表达的信息非常小，只有 0 与 1 。如果要表达完全部有用信息，那么涉及到的变元数量可能是成千上万亿。

这种“描述起来十分简单、却可以延伸出深入研究”的问题个性十分吸引蔡少伟。

2006年，蔡少伟在本科班主任王家兵的带领下首次接触 SAT 问题。当时，他正就读于华南理工大学计算机科学与技术专业，刚上大二。王家兵对 SAT 问题很感兴趣，见蔡少伟数学底子不错，就让他协助研究。为了完成这些工作，蔡少伟跑去图书馆查找资料，由此入门。

本科毕业后，蔡少伟直博北大。在确定研究方向时，蔡少伟先是摸索了一年，最后发现还是求解算法方向最有趣，就选择继续研究 SAT 求解器。

从接触 SAT 问题开始，他就知道这是一块“硬骨头”。

首先，国内研究 SAT 的学者少，知识传承不足。上世纪90年代，虽然国内也有研究 SAT 问题的学者，比如北航的李未院士，华中科技大学的黄文奇教授，还有中科院软件研究所的张健研究员。蔡少伟入门 SAT 所读的第一本著作，就是张健的《逻辑公式的可满足性判定——方法、工具及应用》。但是，这些研究都没有形成一个派系。

其次，研究 SAT求解器需要扎实的数学基础，且对算法设计和工程实现的能力要求极高，往往需要投入数年努力才有论文产出，对研究人员的心智与耐力都是一种考验。蔡少伟自问，虽然自己热爱数学与算法，但并不擅长，也无天赋。

导师苏开乐擅长的是逻辑系统，却支持他选择自己喜欢的求解算法研究。他是当时实验室里唯一做求解器的学生。在这种先天条件不足、后天支持有限的情况下，蔡少伟独自探索，过程的艰难可想而知。

他回忆，当时研究 SAT，最大的困难是没有足够的机器。研究求解器要做大量实验，而他只有一个非常普通的笔记本。由于没日没夜地跑实验，这个笔记本后来还被烧坏了。无奈之下，他只有求助室友，借对方实验室的服务器来跑实验。“不过，这对现在的学生来说已经不是难题，因为现在的计算资源比当时先进多了。”蔡少伟谈道。

早在上世纪60年代，SAT问题就有了第一个求解算法，叫“Davis-Putnam algorithm”（又称“DP算法”），由 Martin Davis 与 Hilary Putnam 提出。后来，DP算法又迭代为“DPLL（Davis–Putnam–Logemann–Loveland）算法”，之后的系统搜索算法主要是基于 DPLL 算法的框架，是解决约束满足性最常用的算法（即回溯搜索法）。

到了90年代，冲突分析子句学习（CDCL）方法与局部搜索方法出现。其中，CDCL在系统搜索算法中加入了冲突分析等关键技术，而局部搜索算法作为主要的启发式算法为人所知。1992年，Bart Selman 提出的局部搜索算法 GSAT 在 N 皇后与图着色等多个经典问题上取得了比 DPLL 算法更好的效果，引起了人工智能领域启发式搜索社群的兴趣，期间出现各类局部搜索算法。而 CDCL 方法极大提高了 DPLL 算法的性能，使得 SAT 求解器的应用得到推广。

此外，研究人员开始对随机 k-SAT 问题产生兴趣，在相变现象研究与相变区随机 k-SAT 的算法研究上取得了许多成果，包括 Alfredo Braunstein 等人在2002年提出的基于统计物理的调查传播（Survey Propagation）方法。在中国，北航的许可教授是深入研究相变现象的研究者之一。但 2010 年前后，SAT 求解的进展近乎停滞。

在蔡少伟读博时，许多人都认为，SAT 问题经过多年的快速发展，已经很难取得进一步的突破。比如，当时他想解决的问题是局部搜索算法求解大规模SAT实例。但是，在他入场时，局部搜索已经不被大多数人看好，处于被边缘化的地位。

明知山有虎，偏向虎山行。还是一座付出与回报不成正比的土头山。问蔡少伟，当时研究的课题遇上关卡、停滞几个月时，是否想过换方向，拣一个比较容易的题做。他说，那时候自己就是“执迷不悟”，不愿意跟在别人的屁股后做研究，觉得没意思。

蔡少伟的口头禅是，“做研究就是要有自己的 label（标签）。”

所谓开辟，往往离不开前人铺就的奠基石。

虽然蔡少伟与导师苏开乐的研究方向不同，他只能靠自己摸索，但在苏开乐的带领下，他有幸结识了一群研究 SAT 问题的前辈，比如法国儒尔-凡尔纳大学（University of Picardie Jules Verne）计算机系的华人教授李初民。

李初民从 1994 年开始研究 SAT 问题，是最早研究 SAT 问题的华人学者之一。他是华中工学院（现华中科技大学）计算机软件专业的第一届毕业生，1983年取得学士学位，后赴法国留学，分别于1985年和1990年在贡比涅大学（University of Technology of Compiegne）计算机系取得了硕士与博士学位。

 图 / 李初民 

博士毕业后，李初民留在法国任教。他入门 SAT，是因为在上《可计算性》这门课时，需要用图灵机进行计算，上课过程中，他发现 SAT 求解器就像一把万能的钥匙，只要解决 SAT 问题，其他许多问题也可以快速求解，于是开始研究 SAT。

有句话说，“始于外貌，陷于才华，忠于人品。”这很符合 SAT 研究者的心路历程。李初民也一样，他被 SAT 问题吸引的原因与蔡少伟相似，“（SAT）看起来很简单，非常容易上手，却有着极强大的表达能力，可以很方便地用它来表达其他问题，比如图染色问题。”

如李初民介绍，SAT的本质是形式逻辑，表面看上去很简单，但丰富的信息量都隐藏在一条条语句中。既纯粹，又神秘。所以，从入门 SAT 后，李初民就一心扑在了 SAT 问题的求解上。

在上世纪90年代所涌现的一大批算法中，李初民与 Anbulag 在1997年所提出的 SATZ 求解器（发表在 IJCAI 1997）受到了极大关注，相关论文被引用了超过 500 次。直到今天，SATZ 也是求解随机 SAT 问题最好的求解器之一。

李初民教授在 SAT 求解器的研究上坚持了二十多年，在这个领域并不常见。许多人都曾为 SAT 问题着迷，但最终能坚持下来的人却很少，主要的原因就在于：要在 SAT 问题上取得新的成果很难。

从上世纪 60 年代至今，SAT 问题的研究已经持续了大半个世纪，传统的、简单的算法都已经有许多外国学者试过。在这种相对成熟的领域去做研究，就是前人已经搭了万丈高楼，你首先要花很长时间搭一条足够长的梯子，了解前人已经研究过的知识，然后伸长手臂，站在高高的梯子上，用力往万丈高楼上丢一颗小小的石子。

“就像今年奥运会的苏炳添，在百米赛跑中两次跑进 10 秒。虽然没有拿金牌，但我们都知道他非常了不起，因为他每进步百分之一秒，都是难上加难。”李初民形容，“SAT问题的后继研究者也是一样。”

 图 / 苏炳添在2021年东京奥运会中跑进10秒 

 图 / 格局检测策略示意图 

 图 / 蔡少伟组的 CCSat 打败了 Kevin Leyton-Brown 等人提出的 SATzilla 求解器 

 图 / SAT与混合整数规划（MIP）、约束整数规划（CIP）及约束规划（CP）的关系 

 图 / George Dantzig，电影《心灵捕手》男主人公的原型 

 图 / 位于德国柏林的ZIB研究所 

 图 / 葛冬冬在杉数科技担任首席科学官 

 图 / Robert E. Bixby 

 图 / 用 SAT 求解器做电路等价验证 

 图 / 混合搜索求解器 RelaxedNewTech 框架示意图 

‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍

‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍

由于微信公众号试行乱序推送，您可能不再能准时收到AI科技评论的推送。为了第一时间收到AI科技评论的报道， 请将“AI科技评论”设为星标账号，以及常点文末右下角的“在看”。