蔡少伟清晰地记得，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 求解同时注重符号推理与算法设计，还需要巧妙的数据结构和精致的代码实现，难度极高。
图 / 蔡少伟（左）参加 SAT 2011 时，遇到同是研究随机局部搜索的德国乌尔姆大学博士生Adrian Balint（右），讨论不过瘾，决定直接上机器 PK
2006年，蔡少伟在本科班主任王家兵的带领下首次接触 SAT 问题。当时，他正就读于华南理工大学计算机科学与技术专业，刚上大二。王家兵对 SAT 问题很感兴趣，见蔡少伟数学底子不错，就让他协助研究。为了完成这些工作，蔡少伟跑去图书馆查找资料，由此入门。
本科毕业后，蔡少伟直博北大。在确定研究方向时，蔡少伟先是摸索了一年，最后发现还是求解算法方向最有趣，就选择继续研究 SAT 求解器。
从接触 SAT 问题开始，他就知道这是一块“硬骨头”。
首先，国内研究 SAT 的学者少，知识传承不足。上世纪90年代，虽然国内也有研究 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 求解器的应用得到推广。
虽然蔡少伟与导师苏开乐的研究方向不同，他只能靠自己摸索，但在苏开乐的带领下，他有幸结识了一群研究 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 问题的求解上。
除了开辟的艰辛，李初民认为，研究 SAT 求解的难点还在于，具有实际意义的 SAT 求解技术通常很简单，主要通过大量繁重的实验来支撑，因此写出来的论文看起来并不高深，投到顶会的论文很容易被不懂行的审稿专家“枪毙”。李初民有这方面的亲身经历。2017年，他指导学生实现了一项子句精简技术，非常有效，投到 IJCAI 后，有审稿专家就说，很多人都已经实现过这个技术，因此论文没有创新。“幸好有一个行家指出我们与别人的不同，论文才逃过了被‘枪毙’的命运。”后来，凭借这项技术，他们获得了当年 SAT 竞赛的金牌，这项技术与他们的实现方式也成为了SAT求解器的标准配置。除了自己研究 SAT 求解器，李初民也乐于指导对SAT求解有兴趣的年青人。蔡少伟也许是李初民指导过的学生中，坚持研究 SAT 最久的学生。他从2009年正式开始 SAT 以及相关问题的算法研究，第一个成果是利用 SAT 求解的约束加权技术设计另一个经典NP 难问题—最小顶点覆盖问题的局部搜索算法，该算法 EWLS 在一个著名挑战实例 frb100-40 上打破了当时的世界纪录。之后，他继续深入局部搜索算法研究，尝试解决其重要缺陷，即循环问题。系统搜索与随机（局部）搜索是SAT问题中的两大方向。拿走地图举例，系统搜索是：走走剪剪，走到地图的哪一块，就将哪一块剪掉，所以这张地图会越走越小，最后走空了，就知道所有地方都走过了；而随机搜索是：你在地图上跑来跑去，但是你不记得你跑过哪些地方，没有“剪枝能力”，无法剪掉，造成循环访问的现象。如果说 SAT 问题是计算机科学世界的大门，那么相变现象则是大门的锁芯，因此相变区实例也成为 SAT 求解的热门测试集。而随机搜索是求解相变区实例的最有希望的方法，但对于大规模相变实例仍然有较大障碍。导致相变区难解的本质原因，就是随机搜索的循环现象。针对这个问题，当时已有的解决方法主要是冯·诺依曼奖获得者 Fred Glover 在1998年提出的禁忌搜索策略（tabu search）与荷兰莱顿大学教授 Holger Hoos 在2002年提出的随机扰动方法。但是，它们没有利用问题结构，无法针对问题结构做出调整，且带有参数，在使用的时候常常需要大量的调参工作。所以，蔡少伟思考如何克服随机搜索中的循环缺陷，希望设计出一种两全其美的方法，既能保留随机搜索的优势，又能克服其循环搜索的缺陷。但这并不简单，蔡少伟苦苦思索，停滞数月，毫无进展。心情自然十分郁闷。那段时间，他读了许多无关本领域的书，尤其是博弈论与社会学。其中，许多篇章谈到个体与群体的关系。带着“如何克服循环缺陷”的问题，蔡少伟虽然是阅读课外书籍，却时时忍不住将这个问题与书中的章节内容联系起来，读着读着，突然冒出一个想法：可以利用环境信息减轻循环！虽然直觉告诉蔡少伟这个思路可行，但直到不久后，他在一次交流会上听到李初民对 SAT 算法研究的演讲，才突然受到启发，一刹那看到了自己苦思冥想的方法！“世界突然安静了，只有笔尖和纸张摩擦的声音，我飞快地写着，很怕是个幻觉，会马上消失。”在个人博客中，蔡少伟记录了这一美妙的精神过程。也是在这一瞬间，他创造了博士期间的得意之作：格局检测策略（CC）。格局检测的核心是：如果变量的环境信息没有改变，则不允许改变取值，而环境信息可以是由该变量的邻居变量的取值构成，也可以由该变量的关联子句的状态构成。通过避免局部结构循环，减轻搜索的循环现象。利用问题的结构信息，不仅可以避免循环现象，还能通过设置多层评分函数克服“短视”。
图 / 格局检测策略示意图
运用这个方法，他大幅度改进了原来的算法，产生了第二篇论文，2011年发表在顶刊《人工智能期刊》（AIJ）上。蔡少伟意识到这个新方法的通用性。他花了一段时间静心思考，把它抽象成一个通用方法，应用到 SAT 问题上。起初并不见效，但他“已陷入 SAT 问题不可自拔”，决心作出名堂。通过半年的努力，他终于超过了当时 SAT 比赛的冠军算法。但好景不长，2011 年 SAT 比赛的新冠军又让他的算法黯然失色。期间几多波折，也经历了数个低谷，直到 2012 年 SAT 比赛，蔡少伟又扳回一城，获得冠军！对于这场夺冠，蔡少伟印象深刻：2011年年底，他开始着手准备，虽然算法在当时已达到国际前沿，但并没有太大的把握。过完寒假回校，他一边忙毕业的事，一边备战 SAT 比赛。有两位师弟帮忙，研究进度加快不少，“开始只是小优化，如隔靴搔痒，一直到比赛截止两个礼拜前才有了质的飞跃。”果然，比赛结果公布，三条主赛道，蔡少伟组的算法（CCSat）赢得了随机组（测试集为相变区实例）的第一名，并且遥遥领先于第二名，求解效率比是 423（70.5%）vs 321（53.5%）。
图 / 蔡少伟组的 CCSat 打败了 Kevin Leyton-Brown 等人提出的 SATzilla 求解器
这也是中国第一次在国际SAT协会举办的 SAT 比赛系列中取得冠军，蔡少伟的心情无比激动。在做算法设计时，他坚持算法大师 Dijkstra 的信条，“优雅就是简单而高效”。他的格局检测策略是一个全新的方法，经过凝练，简单而高效。一路坚持下来，没想到竟成就了自己的风格。蔡少伟的算法以明显优势夺冠，在当时的学术界也引起了较大反响。Holger Hoos 称 CCASat是代表性最前沿求解器，比赛举办方更是以CCASat的成功说明研究核心算法的重要性。2012年前后，随机搜索有逐渐被边缘化的迹象。蔡少伟提出格局检测策略后，加上当时随机搜索方向的其他学者的工作（如probSAT），随机搜索再一次吸引了国内外学者的注意，让大家觉得：哦，原来随机搜索还有很大的研究潜力。接下来几年，随机搜索吸引了更多人加入其中。现在，随机搜索已经成为和CDCL的系统搜索并驾齐驱的两大主流算法之一。2012年从北大博士毕业后，蔡少伟继续在SAT求解器上钻研。他用两年时间从澳大利亚格里菲斯大学获得应用数学博士学位，2014年回国加盟中科院软件研究所，开始挑战康奈尔大学计算机系教授 Bart Sellman 等人在1997年所提出的命题逻辑推理与搜索十大挑战之一：结合系统搜索与随机搜索设计出比这两种方法更高效的算法。 （四）与巨人同行（2）在蔡少伟深入 SAT 求解研究的同时，时任上海财经大学交叉科学研究院院长的葛冬冬开始琢磨线性规划求解器的开发。如前所述，SAT 问题有许多变元，需要判定其为0或1（真或假命题）。SAT问题也可以表现为一个线性方程组，但变元只能取0或1，又被称为“0/1规划问题”。只是，在现实生活中，问题建模可能不是线性方程，而是二次方程、三次方程、对数、指数、根号等等，x与y的取值也不仅仅是0或1，可以是任意数，包括整数、正数、实数……
图 / SAT与混合整数规划（MIP）、约束整数规划（CIP）及约束规划（CP）的关系
葛冬冬是运筹学出身。运筹学研究问题主要分两步，第一步是建模，第二步是求解：将现实中的问题通过算法建成标准的数学模型（如线性不等式）后，再对数学模型进行求解，从而解决现实问题。如果变量少，只有x与y，那么我们可以进行手算；但当数学模型涉及到几百万变量，则必须借助软件（如matlab）来自动计算。本质上，求解器就是一个专业的数学/计算软件，用于实现复杂的数学算法。当软件对线性方程组求解时，该软件可以称为“线性方程组的求解器”。计算机历史上最早的求解器，就是线性规划求解器。葛冬冬对求解器有所耳闻，要追溯到他在斯坦福读博的师门关系：1947年，“线性规划之父”、斯坦福大学教授 George Dantzig （葛冬冬的师爷）提出了第一个用于优化线性系统的算法，叫“单纯形法”（Simplex Method），第一次使大规模优化问题得到求解。单纯形法一直雄踞二十世纪最伟大的算法前五之列。30年后，随着计算机技术的发展，人们又开始尝试用计算机开发求解软件。1979年，第一个求解器软件在美国诞生，名为 LINGO。
幸运的是，他们最终在XPRESS找到了一个志同道合的中国人，本科就读于北航计算机系，毕业后去英国读博，博士期间的内容就是研发求解器。之后，他们又陆陆续续从CPLEX、XPRESS与LINGO等处挖到了多个程序员。后来，又有一些人奔着杉数创始团队都是叶荫宇学生的份上而来。叶荫宇提出的“内点法”的具体实现方法是各大商业求解器的底层架构，圈内有名，所以，在他的感召下，杉数找到了许多优秀的人才。国内的高校也开始了这方面的有意识尝试。2018年，中科院戴彧虹研究院团队推出了国内第一款整数规划求解器CMIP。又过了两年，2019年5月，杉数推出中国首个商用线性规划求解器COPT。COPT的出现，给国内大厂传递了一个重要信息：开发求解器的难度确实极高，但也不是全无可能。随着企业的数字化转型，需要进行更多量化的、精细的智能决策，借助一些数学模型来建模，求解器的用途也越来越大。因此，国内有能力的大企业（比如华为和阿里巴巴）也开始自己琢磨做求解器。 （五）求解器在中国与欧美数十年前就将求解器用于航空、铁路交通规划不同，工业求解器在中国的落地历史很短，最早可以追溯到2000年代初期，宝钢采用 ILOG CPLEX 优化生产规划系统。在COPT出现之前，商业求解器三大厂 CPLEX、GUROBI 与 XPRESS 凭借丰富的商业开发经验，以及较好的性能，在国际市场上占了超过90%的份额。三大求解器中，历史最坎坷的是1988年由美国数学家 Robert E. Bixby 所开发的 CPLEX。1997年，CPLEX 由法国企业 ILOG 收购，2009年，ILOG 又被 IBM 收购，从此 CPLEX 变成了 IBM 的求解器。当时，CPLEX功能较完善，擅长各类求解，在市场上占了统治地位。
图 / Robert E. Bixby
但没过多久，由于 IBM 的自身管理问题，以及对求解器业务不够重视，IBM求解器团队的几个最核心开发人员从 CPLEX 离职，出来创立了新的公司，叫 GUROBI。GUROBI 的唯一业务就是开发求解器，他们十分注重这一块，很快超过了CPLEX。随着 IBM 的越发衰落，CPLEX也随之慢慢衰落，美国商用求解器成了 GUROBI 的天下。与此同时，英国爱丁堡的Dash Optimization团队在1983年开发了 XPRESS，1986 年开始应用于混合整数规划求解。该团队的开发人员大约有10人，一直相对稳定。2008年，XPRESS 由美国金融信用商 FICO 收购，将求解器用于制定金融场景的大规模优化方案。收购后，FICO 不做过多干涉，XPRESS 的开发团队继续留在英国，保持了自身的竞争力，在市场上占有一定份额。这三家均是开始商用求解器，以核数定价，核数越高，价格越高。在中国还没有商用求解器之前，进口求解器的价格基本是卖方市场。杉数的 COPT 发布后，无论核数多少，均以打包价出售，倒逼国外品牌将价格下降来竞争中国的市场。近两年，华为与阿里也开始布局求解器开发。华为开发求解器，主要用于EDA设计、供应链规划等，而阿里做求解器，则主要用于阿里云的资源调度优化。阿里也是从线性规划入手，先做单纯形法，再做内点法。2020年，阿里达摩院决策智能实验室发布数学规划求解器 MindOpt。根据阿里的官方说法，在发布 MindOpt 时，他们已在内部使用了一段时间，帮阿里云节省了数亿元成本。现在，求解器在阿里云上每天被调用的次数以十亿计。过去两年，杉数、阿里与GUROBI在线性规划权威榜单 Mittlemann 测试上竞争激烈。在单纯形法测试上，阿里与杉数轮流当第一，80%的时间是杉数领先；而在内点法上，杉数一直稳居榜首。在线性规划单纯形法上，GUROBI 已经被挤到第三很久了。但是在整数规划这一最重要的求解器开发上，国内与美国还有着很大的差距。目前求解器软件，国内只有COPT具备了求解大规模整数规划问题的能力。“目前我们的800家用户，79%的问题来自整数规划。虽然在榜上排名世界第二，但是实际上我们与三大厂都还有着不小差距。整数规划能力的提升，难度是线性的几十倍，是一个漫长的旅程。我们还需要持续艰苦的努力。”葛冬冬总结。就制造业而言，求解器是最核心的软件。比方说，国家电网的调度优化、无功优化、电力市场清算等等环节，背后有上千个求解器在不停地计算。杉数的线性规划求解器 COPT 自诞生以来，已应用于能源、航空、制造、物流、零售等多个行业，合作的企业包括国网/南网、南航、华为、小米等大厂。杉数与这些大厂的其中一项合作是排产排程。对于 ICT（信息通信技术）这类大厂，设想一下，工厂数量多，数百个工厂有上千个生产车间，用到的零部件大约有10万多种。如果同时收到几百个订单，规定在未来的20周内完成，这时就需要全局优化思想，避免造成资源浪费。我们可以将这个问题建模成一个整数规划问题，即使考虑其简化形式线性规划，变量与约束也都是上亿级别，但求解器可以快速求解。谈到求解器的变迁，葛冬冬感叹，求解器的发展也很快，2009年那会，求解器算一个百万级别的线性规划很吃力，但如今，上亿级别的线性规划只需一个小时的计算量。“一开始大家觉得（上亿级变量问题）只能用 GUROBI 算，我们也没什么信心。最后发现，我们不但能算出来，而且计算速度比 GUROBI 快了大概 30% 以上。”不同领域的求解器在底层思想上有相通的地方。比如，现在华为就开始将SAT求解器中通行的冲突分析思想应用在整数规划求解器中。相对来说，线性规划求解器在国内外的发展更成熟，而 SAT 求解器在国内做的人寥寥无几，近些年来，只有蔡少伟团队在做自己道路的 SAT 求解器。他们曾与华为合作，将 SAT 求解器用于华为芯片中的电路等价验证，将miter电路转为SAT问题，求解规模高达5000万变量、1亿5千万子句，但只用了1小时。
图 / 用 SAT 求解器做电路等价验证
工业 SAT 求解的挑战主要是变量依赖与超大规模，前者需要系统搜索，后者需要随机搜索。换言之，用于工业的SAT求解器，需要将系统搜索与随机搜索相结合。这也是 Bart Sellman 命题逻辑推理与搜索十大挑战中的第七个挑战。蔡少伟从2014年开始研究混合搜索求解器。此前，这方面的求解器有 ANC、WalkSatz 等等，但它们都是侧重系统搜索与局部搜索在求解能力上的互补，黑盒调用，在工业实例上的表现无法超越单一的系统搜索方法。他深入探索了系统搜索和随机搜索的算法行为以及在合作中的作用，经过近几年的研究，放弃了走求解能力互补的道路，提出了以随机局部搜索采样，以系统搜索求解，进行基于信息交互的深度合作。实验结果显示，与 2011 年到 2019 年 SAT 比赛的工业组冠军与主赛道冠军算法相比，蔡少伟所设计的混合搜索求解器比单搜索求解器平均比每个benchmark多解约30个算例，且能求出许多系统搜索与局部搜索均求不出来的实例（平均占求解实例的12%）。
图 / 混合搜索求解器 RelaxedNewTech 框架示意图
这也是距 Bart Selman 在1997年提出十大挑战以来，首次有人解决了第七大挑战。蔡少伟团队提出的松弛子句冲突学习方法也在2020年SAT比赛中获得主赛道的冠军；相关论文（“Deep Cooperation of CDCL and Local Search for SAT”）获得 SAT 2021 最佳论文奖，这也是SAT会议自1997年设立以来，第一篇来自中国的工作获得该奖。在解决 EDA 等中国“卡脖子”问题中，SAT 求解的地位无异于人的命门。同时，一个不容忽略的现实是：无论是 SAT 求解器，还是数学规划求解器（包括线性规划），中国人才始终占极少数。不过，李初民很乐观。他认为，中国研究SAT求解器的人一定会越来越多。今年，他和德国形式化专家Armin Biere，西班牙人工智能专家Felip Manya等人发起、他的早年学生黄冲和华中科技大学吕志鹏参与组织 EDA 国际算法竞赛 EDA Challenge (www.eda-ai.org)，收到的求解器约有一半来自中国。（六）适千里者，三月聚粮路漫漫其修远兮。如今，除了SAT求解，蔡少伟也开始研究SMT（可满足性模理论问题），SMT公式可以看作是SAT与数学规划等背景理论的结合，SMT求解是更具挑战的方向，国内更是无人问津；同样地，葛冬冬与杉数的研究重心也从线性规划求解转到了整数规划和非线性规划求解。无论是从SAT到SMT，还是从线性规划到整数规划，蔡少伟与葛冬冬所传达的讯号是一致的：用求解器加速中国的工业发展。从广义上看，求解器的意义不仅仅在于工业的发展。叶荫宇一直认为，国内应该形成一个将数学与代码相结合的研究生态，而开发求解器是一个很好的结合点。通过研究求解器，我们可以培养一大批既精通数学、又擅长编程的人才。葛冬冬谈道：“导师的想法是要鼓励大家去研究求解器。所以后来，其他大厂或者高校做求解器，有时候遇到棘手的问题，跑来问我们。只要不涉及到核心机密，我们一般都会给他们义务解答。”而李初民则提到，SAT求解讲究从冲突中学习变元之间的精确逻辑关系，机器学习是从大数据中学习数据的统计性质，两者可以相互促进、相互补充，从而人工智能更好地发展。机器学习中的一些问题（比如决策树），也可以表述为SAT问题。从这些优秀学者的经历来看，我们不难发现，求解器是一项大工程：李初民从1994年开始研究，专注三年才开发出 Satz 求解器；蔡少伟从2014年挑战系统搜索与局部搜索相结合，直到2020年才算“拿下”这个问题；葛冬冬等人从2015年开始研究，只做求解器，用了4年才开发了他们的王牌solver — COPT。蔡少伟感叹，求解器适合马拉松型选手，“很巧的是，我以前读书时参加百米短跑，总是压着及格线过关。但如果是跑5000米，我往往就能跑得比较好。”相比机器学习，求解器的热度相形见绌。生于深度学习时代，无论是蔡少伟，还是葛冬冬，他们都没有被外界的浪潮卷动，始终坚持自己最初的追求，以内因战外因，做没有深度学习的 AI 研究。十年过去，他们成为了中国少数研究求解器的青年砥柱。如果没有他们的坚持，我国求解器的研究也许仍是空白状态。热潮自有大众追捧，但对人才本就稀缺的领域来说，一个人的坚持，很可能就决定了全局的命运。致敬！作者注：人物/采访、交流、爆料、抬杠，欢迎添加微信（302703941）。
