追求最优，「约束求解」这一小波人的问题与实践

喜欢

来源：互联网
|
2021-09-17
|
0 条评论
|
我要分享
|
T小字　 T大字

近期「」发表了人物采访文章《解决中国“卡脖子”问题：研究求解器的少数者》，在文章中作者重点介绍了国内这一领域的坚守者和领跑者：中科院软件所蔡少伟研究员以及上海财经大学葛冬冬教授。求解器被誉为“工业软件之魂”，是继芯片与操作系统之后的国之重器。然而相较于机器学习，求解器的热度相形见绌；甚至稍显尴尬的是，国内多数真正有需求的人竟不曾耳闻「求解器」为何物。

我们由中科院计算所副所长包云岗研究员对此文章的点评可略见一斑：

给坚守的少数者点赞！

SAT求解器是EDA软件中的非常核心的基础组件，属于小众研究方向。但若做好了，则能产生很重要的影响。比如普林斯顿电子与计算机工程ECE系主任Sharad Malik教授的成名作，就是发表在2001年设计自动化会议DAC上一项加速SAT求解器的工作Chaff，被广泛应用，这篇论文迄今引用也超过了4600次。

在国内开展这些不是热门的研究确实不容易，从国家自然基金委数据库用“SAT”关键词搜索2000-2020这二十年间批准的相关项目竟然一共只有10项，总经费306万！获得资助的高校屈指可数——北京工商大学、上海交大、广西师范大学、国防科技大学、复旦、北航、黔南民族师范学院、湖南大学、中山大学、北方民族大学。这个结果有点触目惊心！（希望是我搜错了，大家如查到更精准的结果，请一定纠正）

鲜有985、211学校开展这方面研究，但这其实就属于典型的基础研究了，反而是一些地方师范大学有老师在坚守。这也许和985、211高校晋升要求论文、经费比较高有关，做这类研究在985/211不容易生存。听到一个学术界的自嘲段子：我是甘于坐冷板凳，但坐着坐着，板凳没了。

这个局面的改变，也许还是需要一些顶层规划。特别是这些特别基础的研究，应该留出一部分经费把这些学者“包养”起来。举个亲身经历的例子。2010年，我刚到普林斯顿，发现系里每周五都有免费午餐，后来才知道普林斯顿一位理论方向很牛的教授Sanjeev Arora带给全系的“福利”，因为他从美国自然基金委拿到了5年1000万美元的大项目。对于理论研究来说，这简直就是一笔巨款。而这笔经费把美国很多大学的从事理论研究的学者“包养”了至少5年，让他们可以在这期间安心钻研。

那么「求解器」到底是什么？当下进展如何？为何被誉为“工业软件之魂”？

简单来说，它类似于我们生活中使用的计算器，给定输入，求解器则计算出结果。96年的一篇综述中对求解器的本质有很好的描述， 「用户把问题描述出来，然后由计算机来解决。」

事实上，求解器在诸多领域都有广泛应用，例如船舶调度、物流仓储、交通优化、外卖配送、EDA（电子设计自动化）验证等。不同工业领域往往需要不同类型的求解器，因此做求解器需要广博的知识积累，不仅涉及模型、算法、工程实现等技术层面，也涉及底层的数学知识和领域知识。这也是为什么 「需求者众，研究者少」的重要原因。

国内当前需要用到约束求解器的企业，基本都是直接购买/使用美国的Z3、CPLEX、GUROBI、XPRESS等；一旦出现涨价、限购，甚至禁售等“卡脖子”政策，中国将面临无“求解器”可用的尴尬境地。

不过可喜的是，国内这“一小撮”坚守者在积极突破。葛冬冬等人成立了国内首家国产求解器公司「杉数科技」；华为、京东等企业也都在积极布局，组建自己的团队；阿里达摩院也是国内最早投入求解器研发的机构之一。蔡少伟等人历年中在该领域最重要的 SAT 比赛中不断取得最佳成绩，并将成果迅速转化到企业应用当中。

然后，这些依然是Z3、CPLEX、GUROBI、XPRESS等“大巫”下的“小巫”。我们如何能够在求解器应用领域破局，依然需要产学研三界共同探讨和促进。

为了促进求解器领域的应用发展， 智源研究院举办了第一期的约束求解应用封闭研讨「约束求解应用交流会」，汇聚了当前国内这一领域最核心的一波人，包括中国科学院软件研究所研究员、智源学者蔡少伟、阿里达摩院决策智能实验室王孟昌、杉数科技求解器研发总负责人皇甫琦、阿卡思CEO袁军、微软亚洲研究院(MSRA)首席研究员林庆维、华为理论实验室副主任邓益平、华为欧拉实验室形式化验证工程师李屹、京东算法研发部负责人戚永志、北京化工大学经济管理学院马红光等，对当前求解器领域的最新进展和应用进行碰撞。

会议的下半场，与会的各位专家就约束求解的产研结合进行了深入沟通，除了会议的各位报告人，北京大学教授夏壁灿、阿里达摩院决策智能实验室负责人印卧涛、货拉拉李锐、杉数科技首席科学家葛冬冬等也做了发言。

智源社区将研讨核心内容整理如下，本文仅摘录第一部分。

整理：李梦佳、李佳伦、李中梁

1、蔡少伟-约束求解简介与近期进展

首先，中国科学院软件研究所研究员、智源学者蔡少伟对约束求解做了简介并分享了若干进展。其中，四种常见的约束表达方式包括逻辑约束、数值约束、多类型约束和逻辑+数值约束。同时他分享了团队近年来的主要进展：混合求解方法。最后，他提出约束求解为大规模组合优化问题提供了新的思路。

AI有三大主义：符号主义、联结主义、行为主义。其中，约束求解就是符号主义的一个典型方法。解决问题的思路是，将问题描述出来，计算机来解决问题。

96年一篇综述中提到， 「约束求解的圣杯：用户把这个问题简单地描述出来，由计算机来解决。」

人类和计算机之间的鸿沟，是语言，人类用自然语言，计算机用编程语言。所以需要一些专家把自然语言建模为数学语言，然后从数学语言变为计算机可以处理的问题。

首先拿到一个问题，要进行约束建模，变成数学语句，该语句交由约束求解器来处理。这是一条比较机械化的路径。

常见的约束表达有几种方式，

1）布尔代数表达（SAT问题）：侧重于变量之间的逻辑关系；

2）数学规划（MP）：侧重数值约束

3）变量关系（CSP）：各种类型的约束

4）谓词逻辑（SMT）：逻辑+背景理论（包括数学理论和数据结构）

这几种方式当中，SAT是最核心也是最小的，可以看成0-1整数规划，可以看成是CSP的最简单的版本，也可以看成是SMT除掉理论，只剩逻辑框架的一个版本，它是最核心的。

他们有不同的适用场景。SMT可以看成是SAT和数学规划的一个结合体，有时也会和数据结构有关。相比于SAT和数学规划，SMT有时也会包含数组。使用时需要考虑到底这个场景属于什么场景，比如如果布尔变量很多，会倾向于考虑SAT。如果数值约束很强，逻辑约束比较稀疏，那么数学规划更适用。如果涉及的问题逻辑关系很多，背景理论也很强，那么就必须用到谓词逻辑——SMT。此外，表达能力和计算能力之间存在trade-off，比如SMT的表达能力比较强，但计算能力会相对弱。

约束求解可以简单划分为：

1）精确算法（完备算法）：算法结束时确保问题最优解，往往难以解决大规模问题；

2）启发式算法（不完备算法/近似求解方法）：不保证最优解，争取在短时间内返回解（近似解）。

几类约束求解问题介绍

SAT问题（布尔可满足性问题），给定一个命题逻辑公式，判定是否存在一组使其为真的赋值，满足所有的字句。

SAT是第一个被证明为NP完全问题的种子问题。之后衍生出大量的NP完全问题。适用的场景有大量布尔变量的问题，比如EDA领域，AI planning领域，资源分配问题等。

库克定理指出，如果SAT问题可以快速求解，那么所有NP问题都可以快速求解。SAT问题的本质，是探求布尔变量间的逻辑推理关系是否成立。

主要的推理方法有两类：

一类是基于子句学习的系统搜索，采取穷举和回溯的思想，从理论上能保证判定给定命题公式的可满足性，在实例无解的情况下可以给出完备证明。

另外一类是侧重于搜索的启发式搜索，主要基于局部搜索的思想，在解空间随机搜索，但并非单纯随机地搜索，而是在目标函数的引导下逐步逼近最终解。

可满足性模理论：SMT问题

SMT问题可以看成是SAT框架+理论，理论的部分可以是线性规划/非线性规划，位向量/数组理论，甚至字符串等等。不同理论的SMT，求解方法差别会很大，和该理论的领域知识相挂钩。