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

蔡少伟：这个没有去认真统计过，也很难统计，只能从相关会议的人数和文献的数量去估计，但有不少做这方面研究的人可能很久发一篇论文。目前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问题，我就开始喜欢这个问题，一直做到现在。现在我带着一个博士生做这个方向，我也提醒他，这个方向的前期需要积累比较长的时间，会比较辛苦，不要羡慕其他同学发论文，我们做的事比发论文更有意义。