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

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 问题的社群目前有多大呢？