蔡少伟清晰地记得，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。
在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年所提出的命题逻辑推理与搜索十大挑战之一：结合系统搜索与随机搜索设计出比这两种方法更高效的算法。
图 / 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的出现，给国内大厂传递了一个重要信息：开发求解器的难度确实极高，但也不是全无可能。随着企业的数字化转型，需要进行更多量化的、精细的智能决策，借助一些数学模型来建模，求解器的用途也越来越大。因此，国内有能力的大企业（比如华为和阿里巴巴）也开始自己琢磨做求解器。
图 / 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 框架示意图
相关阅读
雷锋网雷锋网雷锋网
雷峰网原创文章，未经授权禁止转载。详情见转载须知。
