作者：智源社区 贾伟
AI 这个词被偷走了。
图灵奖得主Alan Kay在智源大会上曾经这样说：因为在深度学习带来人工智能的一波热潮下，很多人被误导，认为人工智能就等于机器学习。而事实上，机器学习只是整个智能研究中的子领域。
因此，我们始终要意识到，尽管机器学习在近十年取得了令人瞩目的成就，但在此之外，仍有大量值得深度探究的其他人工智能研究。
例如：布尔可满足性问题（Boolean satisfiability problem，SAT）。
SAT ，即确定是否存在满足给定布尔公式的解的问题。举例来说，针对公式“a AND NOT b”，询问是否存在一个 a 和 b 的解，能够使公式为真，如果存在，则说这个公式可满足；反之，则称不满足。例如“a AND NOT a”便是不满足的，因为不存在一个 a 的解使公式为真。
SAT 研究的重要性，不言而喻。首先，SAT是人工智能领域自动推理中的一个经典问题，也是历史上第一个被证明为 NP 完全的问题。其次，在工业领域（尤其是软硬件验证中），SAT求解器具有广泛的应用，例如Intel芯片和Windows操作系统验证中都用到了SAT求解器。
在深度学习所遇挑战愈发艰难之际，事实上，我们需要回过头来，去看看人工智能的其他领域的研究，特别是包含着人类知识的研究方向，将这些研究与以深度学习为代表的机器学习方法进行结合，从而创造出下一代具有知识的人工智能算法。同时也只有从一个全面的角度，才能认清人工智能的全貌，而不被深度学习这“一叶”而障了目。
智源针对SAT的研究及发展，与中科院软件所研究员蔡少伟进行了一次深度对话，从中或可一窥 SAT 研究的进展及社群现状。
蔡少伟，是国内少有的几位对 SAT 有较深入研究的学者之一。他在近日与其博士生张昕荻共同开发的SAT 求解器在SAT Competition 2020比赛中获得了Main Track SAT冠军。此外，蔡少伟团队也曾获得SAT Competition 2014、2016亚军和2012、2018冠军的奖项，以及2018年联合逻辑奥林匹克金牌。他所提出的约束求解技术和研制的SAT求解器被分别应用于微软Azure云平台的虚拟机预配置和异常检测、腾讯地图优化以及美联邦通信委员会的频谱分配等项目中。
Q1：恭喜你再次获得SAT国际比赛冠军。就布尔可满足性问题（SAT）而言，目前大家似乎还比较陌生。你能不能先介绍一下？
蔡少伟：SAT也称为命题逻辑公式可满足性问题，就是要判断一个命题逻辑公式是否可满足，也即是否存在对该公式变量的一组赋值，使得公式为真。因为命题逻辑公式的变量都是布尔变量，所以常常称为布尔可满足性问题。
Q2：判定一个命题是否可满足很有意思，但从问题研究本身以及工业应用来说，它有什么意义呢？
蔡少伟：要谈SAT的意义，得先认识到 SAT不仅仅是一个具体问题，它是个元问题，代表一种解决问题的思路。
SAT是用布尔逻辑表达的，是非常底层的表达，这使得它在理论和实践上都有很广泛的意义。当时SAT被证明为NP完全问题，就是从图灵机的角度去证明的。这是第一个被证明为NP完全的问题，是NP完全性理论的种子问题。很多漂亮的复杂性理论结果都和SAT有关系，随机SAT和统计物理也有密切关系。
另一方面，SAT是有广泛应用的，比如软硬件验证，数学定理的自动证明，密码学，资源配置，生物计算，等等。SAT是软硬件验证的基础引擎，像NASA，Intel，微软这些巨头都用到了SAT求解器去做相关的事情。
Q3：能不能从历史角度，介绍一下SAT研究经历过哪些阶段？每个阶段代表性方法及特点是什么？
蔡少伟：SAT研究涵盖面比较大，我就从SAT算法相关的研究历史讲吧，比较粗糙的分可以分为三个阶段。
早期阶段（1960-1990）: 一般认为SAT算法可以追溯到1960年Davis和Putnam提出的DP过程以及后来的DPLL。这也是机器定理证明历史上的一个重要工作。1971年，SAT被证明为NP完全问题，这是另一个重要的事情，在这之后有很多复杂性方面的工作。这个时期的研究比较集中在归结原理和复杂度研究，也包括易解子类比如2SAT和Horn SAT的研究。
快速发展阶段（1990-2010）：这个阶段SAT求解的研究有了巨大的进展，目前常用的SAT方法包括冲突分析子句学习（简称CDCL）方法和局部搜索方法都是在90年代提出的。
1992年，Seman和Gu几乎同时开启了SAT的局部搜索算法研究，GSAT算法在几个典型的问题包括N皇后和图着色等问题上比DPLL算法取得了更好的效果，也引起了AI领域启发式搜索社群的兴趣，之后出现了各种SAT局部搜索算法，华裔法国教授Chumin Li老师在这方面做了一些有影响的工作。
CDCL方法是在90年代中期提出的，主要特点是非时序回溯和子句学习，之后从算法和数据结构都有一些改进的工作。在这方面有一个典型的求解器MiniSAT，2003年研发的，后来有持续改进，基本实现了CDCL的主要技术。
另一个典型求解器就是Glucose，提出了文字区块距离，从学习子句的管理方面对CDCL做了进一步改进。这期间，SAT求解器的应用也得到广泛推广。
此外，研究人员对一类特殊的SAT问题有较高的兴趣，就是随机k-SAT问题，尤其是对相变现象的研究以及对相变区随机k-SAT的算法研究，从理论上和求解算法上都有不少工作，有一个基于统计物理的Survey Propagation方法在求解相变区的随机3-SAT问题有很好的效果。
现代阶段（2010至今）：2010年前后，曾经一度SAT求解的进展近乎停滞，不少人也觉得这个方向发展了那么多年了，应该很难突破了。确实，经过快速发展的20年之后，SAT求解要进一步改进的难度更大了。
或许是停滞的期间激发了新的探索，2012年至2015年这几年期间，出现了一批新的局部搜索SAT算法，因为采用的技术和之前的有较大不同且性能上有大幅度提升，在文献中常常被称为现代局部搜索求解器，主要包括格局检测方法和概率分布方法，对应的代表性算法分别是CCASat（这也是我拿到SAT比赛第一个冠军的算法）和ProbSAT。
在CDCL方面，对于学习子句的管理更加精致了，并且开始有研究利用机器学习方法来改进算法的启发式，代表工作是Maple算法用MAB多臂赌博机方法来改进分支启发式。
另外，局部搜索和CDCL的结合引起了越来越多的兴趣，尤其是最近3年，这方面的研究越来越深入，今年的SAT比赛中Main track的前三名都结合了这两种方法。这个方向还不是很成熟，但已经显出其潜力，我相信在接下来几年是SAT求解的一个主要方向。
除了这两个主要方法的发展，SAT并行处理也有了较大进展，主要是Cube-and-Conquer方法。算法选择器和自动算法配置也被引入来提高SAT求解，它们是对已有的SAT算法通过机器学习方法进行算法或策略的自动选择，更多的是从工程的角度去研究，SAT社群一般把它们和核心算法区分开。此外，SAT社群对SAT应用的重视达到了新的高度，这也可以从最近几年发表的论文看出来，从数学定理，经济学定理的自动证明，到频谱分配等和软件验证等实际项目，可以越来越多地看到SAT求解的应用，论文中的实验也更加侧重于现实数据。
Q4：你刚才提到“SAT社群”。现在以深度学习为代表的机器学习社群已经达到几百万的规模。那么，研究 SAT 问题的社群目前有多大呢？
蔡少伟：这个没有去认真统计过，也很难统计，只能从相关会议的人数和文献的数量去估计，但有不少做这方面研究的人可能很久发一篇论文。目前SAT会议每年大概100多人，另外SAT研究的论文也主要出现在CP（约束求解领域的会议，今年录用55篇论文）和IJCAI，AAAI等会议的相应session。总的来说，和目前比较热的机器学习方向相比，SAT社群要小很多。
从分布上看，最主要是欧洲，包括德国，法国，奥地利，英国，芬兰，西班牙等，欧洲向来有逻辑和形式化的传统，在这方面一直保持的挺好，紧接着是北美（美国和加拿大），然后，亚太地区包括中国，日本，澳大利亚，新加坡等也做，但是规模小一些。
中国在这方面的社群应该说没有形成，做的人太少了，比较零散，学生们大都不愿意做这种偏逻辑和传统算法的方向，可能是受到发论文和找工作的压力的影响，不过最近几年还是慢慢有一些人加入进来做，我觉得有个好的趋势。
Q5：SAT比赛应该是研究SAT问题的研究者一个主要集散地了，从2002年至今，国际 SAT 学会已经举办了13届SAT比赛。这个比赛对SAT社区产生了哪些有价值的影响？
蔡少伟：举办SAT比赛，一个是为了促进SAT求解的进展，一个也是促进SAT应用，每届比赛都会鼓励大家提交从现实应用编码过来的SAT问题提交作为比赛的测试集。
我觉得SAT比赛带来的价值是多方面的。首先是促进SAT算法的研究，不仅是促进大家去改进算法，而且参加比赛的代码大部分时候是要求开源的，这也促进大家互相学习（互相竞争），往往前一届比赛的冠军到了下一届都难以保持前三名。这对学生是个很好的事情，有充分的资源可以学习。
当然，也提高了SAT社群的凝聚力和知名度，并且向工业界随时反馈最新进展，SAT会议上也有不少来自工业界的人员去参与，去听取最新进展，也促进了SAT求解器在工业界的应用。
Q6：这很有意思。SAT 比赛的评比过程怎样？
蔡少伟：每届比赛一般是在4，5月份截至求解器的提交，没有限定你的研发时间，只要在截至时间之前提交到比赛指定的平台即可，同时也会征集比赛的测试集，举办方也会自己生成测试集并从提交的测试集里面挑选一些作为比赛测试集。
比赛测试集只有在赛后才会公布，每届比赛的测试集是不一样的。测试集来自数学问题和工业问题编码过来的SAT问题。
当比赛提交的截至日期到了之后，组织方就会进行实验，对提交的求解器进行评估，评估的标准主要是以给定的时间限制（比如5000秒）求解的问题个数为主，也参考求解时间。比赛结果会在当年的SAT会议上公布。
Q7：我们注意到，从2012年起，你几乎每届都获得过冠/亚军。在每年比赛中，所使用的方法有哪些变化？而且我们也比较好奇，你每届都能获奖的秘诀是什么？
蔡少伟：其实也没有每届都获得过冠/亚军，比如我在2013年SAT比赛就没得奖。SAT Competition有时候是一年办一次，有时候是两年办一次，中间一年可能是一个称为SAT Race的活动。不过比较好的一件事是，从2012年起每一届SAT比赛都有获奖求解器是用到我的方法开发的。
在比较早的几届，也就是从2012到2016那几年，我的SAT求解器主要是局部搜索求解器；从2018年开始，我主要研究对CDCL求解器的改进，这几年主要的方法是我在2018年提出来的松弛CDCL方法，2018和2020我获得冠军的求解器都是基于该方法研发的。
说实话，我没发现什么获奖的秘诀。每一届比赛的结果公布之前，我都不知道自己会不会得奖，所以每次到了公布结果的时候仍然会激动。我唯一肯定的就是，我在这个方向付出了持续不断的努力。从我本科二年级2006年第一次接触SAT问题，我就开始喜欢这个问题，一直做到现在。现在我带着一个博士生做这个方向，我也提醒他，这个方向的前期需要积累比较长的时间，会比较辛苦，不要羡慕其他同学发论文，我们做的事比发论文更有意义。
Q8：你在 SAT 上的研究有哪些实际应用？以及你比较关心的实际应用是哪些？
蔡少伟：我们的SAT求解器被实际项目直接调用的，我知道的有美联邦通讯委员会的频谱分配项目，意大利银行ARC系统优化，以及MIT的新型材料研究项目，如果说到相关方法的应用，还包括腾讯地图优化和微软Azure云平台里虚拟机预配置用到的约束求解算法等。
目前我更加关心SAT求解在芯片验证上的应用，实际上最近我们正在跟国内这方面的主要企业讨论这方面的事情，也做了一些初步的实验，希望有机会能为我国的芯片事业贡献微薄的力量。
Q9：我看到你之前提到，你在人工智能和算法设计有着比较广泛的兴趣。那么在这些方面，你研究思路是什么呢？
蔡少伟：人工智能是很大的领域，不同方法擅长求解不同类型的问题。不过现在可能很多人觉得人工智能和机器学习是同义词，他们可能不知道人工智能还有约束求解和自动推理这些方向。我自己会坚持做约束求解和自动推理这些偏向于符号主义的方向。我感觉机器学习更适合于感知任务，而基于逻辑和约束的方法在认知层次会更合适一些。当然，不同的方法其实可以互相借鉴，相互融合，我相信机器学习方法可以用来提高约束求解方法。但我倾向于相信在这方面比较好的途径是，将人类经验知识（比如成功的算法框架/方法）和机器学习进行结合。
此外，做求解器就是做工具，总是要找到实际问题去发挥它的价值，很多智能应用的底层都涉及到复杂的约束问题，我们做的研究处于人工智能比较底层的研究。
在算法设计方面，我一直比较关心的一个事情就是，如何缩小理论算法/复杂度理论和实验算法之间的距离。从现状上，这个距离可以称得上是鸿沟了。理论算法有漂亮的理论结果，但是实际应用的时候却很少有效解决问题，而实验算法比如SAT求解器可以很好解决实际问题，但是缺乏理论上的理解。这需要两个方向的人互相交流合作，然而这正是目前比较缺乏的。我和几个朋友组织了一个研讨会，是关于难解问题的理论、算法和应用，也是想促进这个事情。我和北航的许可老师就这个问题讨论过很多次，谈到目前对算法的分析方法也许需要做出调整，比如理论上认为比较难的最大团问题，在实际中一些几千万点的大图上却可以在几秒钟精确求解，因为具体问题的难度不仅和规模有关，也和问题的结构有关，直观上是很容易理解的事情，但是如何做就不知道了。理论算法和实验算法在思路上有时候也是可以互相启发的，比如我在SAT方面有一个关于“关键子句”方面的想法，就是受到一个SAT理论算法PPSZ的启发。上次陆品燕老师跟我讨论时也提到他在考虑如何将近似算法的方法用于启发式算法，我觉得很高兴，越多人重视这个问题，那么就越早有进展。
Q10：很棒，最后问一个比较宽泛的问题。你觉得做学术研究，最重要的品质是什么？
蔡少伟：我觉得自己还是学术界的学生，现在还不适合来回答这个问题。我只知道，做学术研究，心里得有学术，“要保守你的心，胜过保守一切。”
