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云平台的虚拟机预配置和异常检测、腾讯地图优化以及美联邦通信委员会的频谱分配等项目中。