你所不知的角落，有人在做没有深度学习的AI

本文插图
作者：智源社区贾伟
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求解器去做相关的事情。