在人工智能时代，他们不做深度学习。
文章来源：AI科技评论
ID：aitechtalk
作者：陈彩娴
少数者
蔡少伟清晰地记得，年夏天他去美国密歇根大学安娜堡分校参加SAT会议时，一眼望去，全场只有他一个中国人。
参会人员一半来自欧洲，四分之一来自北美（尤其是美国），另外四分之一则来自亚太地区。他将自己的“单刀赴会”列为SAT一行的两大记忆点之一，另一点是那年大会主席的论文被SAT评委“枪毙”了。
这是蔡少伟第一次参加SAT。这个被CCF列为B类的会议全称为“InternationalConferenceonTheoryandApplicationsofSatisfiabilityTesting”（可满足性判定的理论与应用国际会议），始设于年，主要面向研究可满足性问题，尤其是布尔可满足性（BooleanSatisfiabilityProblem，简称“SAT”）问题的科研人员，向来少为中国学者问津。
不过，蔡少伟似乎对这份“孤军作战”的寂寞也早已见惯不惯。当时，他在北京大学计算机系的理论实验室攻读博士，师从苏开乐，是当时组里唯一一位研究SAT求解算法的人。作为数理逻辑基础问题又是NP完全问题，SAT求解同时注重符号推理与算法设计，还需要巧妙的数据结构和精致的代码实现，难度极高。
蔡少伟（左）参加SAT时，遇到同是研究随机局部搜索的德国乌尔姆大学博士生AdrianBalint（右），讨论不过瘾，决定直接上机器PK
同样经历过“四下无人”的少数者，还有年从斯坦福毕业回国的葛冬冬。那一年，他从斯坦福大学管理科学与工程系（MSE）取得运筹学博士学位，拿到了上海交通大学的教职offer，准备回国任教。
读博期间，他师从运筹学泰斗、冯·诺依曼理论奖的唯一华人获奖者叶荫宇，主要研究大规模优化理论与算法，并不直接研究求解器，只是在研究某些整数规划的问题时经常需要调用。但回国后，他却发现，国内居然没有人开发商用求解器。凡是需要用到求解器的企业，都是直接购买美国的CPLEX、GUROBI与XPRESS。
“求解器分为专业版、个人版与商用版，不同版本有不同的价格，5万到40万人民币不等。”葛冬冬谈道，“中国没有求解器，要从国外买，人家不可能给你降低价格。如果买几千台的话，几个亿的外汇就这样出去了。”
看到国内在求解器研究上的空白，葛冬冬感到很奇怪：为什么没有人做？但那时，他刚步入教职不久，身兼数职，也没有条件去作更多的研究。直到年，他从交大转到上海财经大学、担任交叉科学研究院院长，有机会组建自己的团队，才开始带队探索。
刚步入教职的葛冬冬
十年过去，再回头看，从无人区走出来的蔡少伟与葛冬冬，都已成为国内研究求解器的青年先驱人物。但是，谈起求解器的研究现状，他们的结论仍与十年前无异，“就一小撮人”。
事实上，在深度学习兴起之前，人工智能十分注重逻辑推理（reasoning），当时偏符号主义的SAT问题比深度学习还流行。
从“解题”的角度看，一切人工智能系统都可以归结为“问题求解”（ProblemSolving）系统，即为了实现给定目标而展开的动作序列的过程。而解决特定问题的算法，被称为“求解器”（solver）。无论是SAT求解器，还是整数规划求解器，都是经典的离散约束算法问题。
求解器在工业发展中的意义非凡。例如，中国战略布局上亟待解决的“卡脖子”难题EDA（电子设计自动化）需要用到SAT求解器进行快速验证，而制造、物流与供应链优化等则需要用到整数规划求解器（尤其是线性规划求解器）。因此，近两年，华为与阿里也开始布局求解器研究。
江湖传闻，华为内部对求解器研究十分重视，多个海内外团队同时推进，任总直接听取汇报。由于人才供给紧缺，蔡少伟所培养的博士毕业生入职华为后，待遇直接对标“华为天才少年”，年薪近百万。
从SAT=NP-Complete谈起
探讨SAT求解器之前，我们首先要了解SAT问题的研究历史。
说来厉害，SAT问题是计算机历史上第一个被证明为NP-Complete的问题，其主要贡献者就是计算复杂理论研究方向的大神、现任多伦多大学计算机系与数学系的教授StephenA.Cook。
年图灵奖获得者StephenCook
在年的论文“TheComplexityofTheoremProvingProcedures”中，StephenCook提出了著名的库克定理（CookTheorem），从图灵机的角度证明所有NP问题都可以快速转化为SAT问题。
在库克定理里，图灵机的计算过程可以用SAT表达出来，转化成一条条独立的语句，十分简单，但又极高效。库克定理指出，如果SAT问题可以快速求解，那么所有NP问题都可以快速求解。Cook本人也因此获得年图灵奖。
广义上，可满足性（Satisfiability）问题是指对给定逻辑公式判定是否可满足的问题。SAT问题特指“布尔可满足性问题”，又称“命题逻辑可满足性问题”。命题逻辑是形式逻辑最基本的类别，基本元素是布尔变元。每个布尔变元代表一个基本命题。SAT问题的本质，是探求一大堆布尔变元之间的逻辑推理关系是否成立。
听起来很高深，但描述十分简单。举个例子：
甲乙丙想参会，甲说：乙参会我就参会，乙说：丙参会我就参会，而丙说：甲参会我就不参会，那么能不能同时满足甲乙丙的参会需求？
这就是一个SAT问题，而求解的答案是：他们的需求是不可（同时）满足的。如果命题简单，那么人脑可以很快判定逻辑推理关系是否成立。但随着布尔变元和约束的条件越来越多，SAT的求解就会越来越难，需要借助算法来进行推理与计算。
比方说，在进行机场飞机调度时，研究人员要考虑的状态非常多，包括待起飞的飞机数量，飞机分布的跑道数量与位置，飞机的运行方向，风向等等。一个布尔变元表示单一时空下的一种状态。由此可见，布尔变元所表达的信息非常小，只有0与1。如果要表达全部有用信息，那么涉及到的变元数量可能是成千上万亿。
这种“描述起来十分简单、却可以延伸出深入研究”的问题个性十分吸引蔡少伟。
年，蔡少伟在本科班主任王家兵的带领下首次接触SAT问题。当时，他正就读于华南理工大学计算机科学与技术专业，刚上大二。王家兵对SAT问题很感兴趣，见蔡少伟数学底子不错，就让他协助研究。为了完成这些工作，蔡少伟跑去图书馆查找资料，由此入门。
本科毕业后，蔡少伟直博北大。在确定研究方向时，蔡少伟先是摸索了一年，最后发现还是求解算法方向最有趣，就选择继续研究SAT求解器。
从接触SAT问题开始，他就知道这是一块“硬骨头”。
首先，国内研究SAT的学者少，知识传承不足。上世纪90年代，虽然国内也有研究SAT问题的学者，比如北航的李未院士，华中科技大学的黄文奇教授，还有中科院软件研究所的张健研究员。蔡少伟入门SAT所读的第一本著作，就是张健的《逻辑公式的可满足性判定——方法、工具及应用》。但是，这些研究都没有形成一个派系。
其次，研究SAT求解器需要扎实的数学基础，且对算法设计和工程实现的能力要求极高，往往需要投入数年努力才有论文产出，对研究人员的心智与耐力都是一种考验。蔡少伟自问，虽然自己热爱数学与算法，但并不擅长，也无天赋。
导师苏开乐擅长的是逻辑系统，却支持他选择自己喜欢的求解算法研究。他是当时实验室里唯一做求解器的学生。在这种先天条件不足、后天支持有限的情况下，蔡少伟独自探索，过程的艰难可想而知。
蔡少伟
他回忆，当时研究SAT，最大的困难是没有足够的机器。研究求解器要做大量实验，而他只有一个非常普通的笔记本。由于没日没夜地跑实验，这个笔记本后来还被烧坏了。无奈之下，他只有求助室友，借对方实验室的服务器来跑实验。“不过，这对现在的学生来说已经不是难题，因为现在的计算资源比当时先进多了。”蔡少伟谈道。
早在上世纪60年代，SAT问题就有了第一个求解算法，叫“Davis-Putnamalgorithm”（又称“DP算法”），由MartinDavis与HilaryPutnam提出。后来，DP算法又迭代为“DPLL（Davis–Putnam–Logemann–Loveland）算法”，之后的系统搜索算法主要是基于DPLL算法的框架，是解决约束满足性最常用的算法（即回溯搜索法）。
到了90年代，冲突分析子句学习（CDCL）方法与局部搜索方法出现。其中，CDCL在系统搜索算法中加入了冲突分析等关键技术，而局部搜索算法作为主要的启发式算法为人所知。年，BartSelman提出的局部搜索算法GSAT在N皇后与图着色等多个经典问题上取得了比DPLL算法更好的效果，引起了人工智能领域启发式搜索社群的兴趣，期间出现各类局部搜索算法。而CDCL方法极大提高了DPLL算法的性能，使得SAT求解器的应用得到推广。
此外，研究人员开始对随机k-SAT问题产生兴趣，在相变现象研究与相变区随机k-SAT的算法研究上取得了许多成果，包括AlfredoBraunstein等人在年提出的基于统计物理的调查传播（SurveyPropagation）方法。在中国，北航的许可教授是深入研究相变现象的研究者之一。但年前后，SAT求解的进展近乎停滞。
在蔡少伟读博时，许多人都认为，SAT问题经过多年的快速发展，已经很难取得进一步的突破。比如，当时他想解决的问题是局部搜索算法求解大规模SAT实例。但是，在他入场时，局部搜索已经不被大多数人看好，处于被边缘化的地位。
明知山有虎，偏向虎山行。还是一座付出与回报不成正比的土头山。问蔡少伟，当时研究的课题遇上关卡、停滞几个月时，是否想过换方向，拣一个比较容易的题做。他说，那时候自己就是“执迷不悟”，不愿意跟在别人的屁股后做研究，觉得没意思。
蔡少伟的口头禅是，“做研究就是要有自己的label（标签）。”
与巨人同行（1）
所谓开辟，往往离不开前人铺就的奠基石。
虽然蔡少伟与导师苏开乐的研究方向不同，他只能靠自己摸索，但在苏开乐的带领下，他有幸结识了一群研究SAT问题的前辈，比如法国儒尔-凡尔纳大学（UniversityofPicardieJulesVerne）计算机系的华人教授李初民。
李初民从年开始研究SAT问题，是最早研究SAT问题的华人学者之一。他是华中工学院（现华中科技大学）计算机软件专业的第一届毕业生，年取得学士学位，后赴法国留学，分别于年和年在贡比涅大学（UniversityofTechnologyofCompiegne）计算机系取得了硕士与博士学位。
李初民
博士毕业后，李初民留在法国任教。他入门SAT，是因为在上《可计算性》这门课时，需要用图灵机进行计算，上课过程中，他发现SAT求解器就像一把万能的钥匙，只要解决SAT问题，其他许多问题也可以快速求解，于是开始研究SAT。
有句话说，“始于外貌，陷于才华，忠于人品。”这很符合SAT研究者的心路历程。李初民也一样，他被SAT问题吸引的原因与蔡少伟相似，“（SAT）看起来很简单，非常容易上手，却有着极强大的表达能力，可以很方便地用它来表达其他问题，比如图染色问题。”
如李初民介绍，SAT的本质是形式逻辑，表面看上去很简单，但丰富的信息量都隐藏在一条条语句中。既纯粹，又神秘。所以，从入门SAT后，李初民就一心扑在了SAT问题的求解上。
在上世纪90年代所涌现的一大批算法中，李初民与Anbulag在年所提出的SATZ求解器（发表在IJCAI）受到了极大