解决中国“卡脖子”问题：研究求解器的少数者
来源:Amadeus发布时间:2021-09-071249浏览
询问 AI（一）少数者
蔡少伟清晰地记得，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 = NP-Complete 谈起
探讨 SAT 求解器之前，我们首先要了解 SAT 问题的研究历史。
说来牛叉，SAT 问题是计算机历史上第一个被证明为 NP-Complete 的问题，其主要贡献者就是计算复杂理论研究方向的大神、现任多伦多大学计算机系与数学系的教授Stephen A. Cook。
图 / 1982 年图灵奖获得者 Stephen 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秒
除了开辟的艰辛，李初民认为，研究 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。
图 / George Dantzig，电影《心灵捕手》男主人公的原型
1980年代，美国又有多位学者提出了内点法（Interior-Point algorithm）。此前，线性系统优化一直是单纯形法的天下，直到内点法出现。内点法在某些问题上比单纯形法的求解速度更快，可以处理许多非线性规划问题，从而成为新的潮流，并也被用于商用求解器的开发。George Dantzig 的得意门生叶荫宇（葛冬冬的导师）也是公认的内点法奠基者之一，因此获得了运筹学的最高奖——冯·诺依曼理论奖。
图 / 位于德国柏林的ZIB研究所
从2013年加入上海财经大学后，葛冬冬便开始有意识地招收一些擅长做优化算法的年青人。那时，他有些犹豫：“求解器这事究竟能不能做？”心里没底，跑去咨询导师，叶老师很支持，说：“中国总得要自己的求解器，不要老觉得做不成，总得有人挑头。”于是，2015年，葛冬冬联合海内外的同门师兄弟罗小渠、王子卓与王曦，创立了杉数科技，开始倒腾求解器。杉数刚成立，叶荫宇弟子、斯坦福博士等称号，就为他们拿到了大约200万美元的天使轮投资。最初，他们是从上海财大的交叉科学院调配人手，加上杉数科技的创始团队，从零开始探索做一个开源求解器。葛冬冬与创始团队自学、找专家、找导师，花了很多力气琢磨求解器开发，比如单纯形法与内点法如何在软件开发上走通全流程，弄清楚求解器开发的核心部件，矩阵数据简化等等。期间，叶荫宇给了许多指导，甚至亲自下场帮他们写开源代码。经过两年的摸索，他们在2017年发布了中国第一个开源优化求解器 LEAVES，但性能并不突出。这使他们意识到，开发求解器是一个很大的系统工程，光靠学校的力量、投入小的成本是做不成的。所以，杉数开始在国际上秘密寻求有经验的人，组建团队。“说白了，真正懂求解器开发的就是三大厂（XPRESS、GUROBI与CPLEX）的开发人员，每家的核心开发都不到10人，所以全世界真正精通求解器的不过20多人。”葛冬冬介绍，“加上德国柏林ZIB研究所的人，叶老师一位开发第三方商业求解器 MOSEK 的丹麦博士生和他的团队。以及很少的一些成熟开源求解器的高手，也就是说，全世界的核心求解器开发人才，就这30多个人。”
图 / 葛冬冬在杉数科技担任首席科学官
幸运的是，他们最终在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 框架示意图
（六）适千里者，三月聚粮路漫漫其修远兮。如今，除了SAT求解，蔡少伟也开始研究SMT（可满足性模理论问题），SMT公式可以看作是SAT与数学规划等背景理论的结合，SMT求解是更具挑战的方向，国内更是无人问津；同样地，葛冬冬与杉数的研究重心也从线性规划求解转到了整数规划和非线性规划求解。无论是从SAT到SMT，还是从线性规划到整数规划，蔡少伟与葛冬冬所传达的讯号是一致的：用求解器加速中国的工业发展。从广义上看，求解器的意义不仅仅在于工业的发展。叶荫宇一直认为，国内应该形成一个将数学与代码相结合的研究生态，而开发求解器是一个很好的结合点。通过研究求解器，我们可以培养一大批既精通数学、又擅长编程的人才。葛冬冬谈道：“导师的想法是要鼓励大家去研究求解器。所以后来，其他大厂或者高校做求解器，有时候遇到棘手的问题，跑来问我们。只要不涉及到核心机密，我们一般都会给他们义务解答。”而李初民则提到，SAT求解讲究从冲突中学习变元之间的精确逻辑关系，机器学习是从大数据中学习数据的统计性质，两者可以相互促进、相互补充，从而人工智能更好地发展。机器学习中的一些问题（比如决策树），也可以表述为SAT问题。从这些优秀学者的经历来看，我们不难发现，求解器是一项大工程：李初民从1994年开始研究，专注三年才开发出 Satz求解器；蔡少伟从2014年挑战系统搜索与局部搜索相结合，直到2020年才算“拿下”这个问题；葛冬冬等人从2015年开始研究，只做求解器，用了4年才开发了他们的王牌solver —COPT。蔡少伟感叹，求解器适合马拉松型选手，“很巧的是，我以前读书时参加百米短跑，总是压着及格线过关。但如果是跑5000米，我往往就能跑得比较好。”相比机器学习，求解器的热度相形见绌。生于深度学习时代，无论是蔡少伟，还是葛冬冬，他们都没有被外界的浪潮卷动，始终坚持自己最初的追求，以内因战外因，做没有深度学习的 AI 研究。十年过去，他们成为了中国少数研究求解器的青年砥柱。如果没有他们的坚持，我国求解器的研究也许仍是空白状态。热潮自有大众追捧，但对人才本就稀缺的领域来说，一个人的坚持，很可能就决定了全局的命运。致敬！
作者 | 陈彩娴
整理 | 李扬霞编辑 | 王晔新闻来源：中科院半导体所，文中所述为作者独立观点，不代表icspec立场。更多精彩资讯请下载icspec App。如对本稿件有异议，请联系微信客服specltkj。
