Kissat在2020年SAT大赛的主赛道上获得第一名，在不满意的情况下获得第一名。
为了表明SAT求解在最近几年有了很大的进步，特别是2020年的Kissat，我们收集了2002到2020年的SAT竞赛的获胜者，并对他们进行了固定和移植，使其与现代编译器兼容。
然后，我们在2011年、2019年和2020年的竞赛实例集群上运行了这些历届冠军，更准确地说，是在2011年SAT竞赛申请路径的300个实例、2019年SAT竞赛的400个实例和SAT竞赛2020主路径的400个实例上运行的。
下面的曲线图显示了在一定时间内解决的实例数，因此本质上是运行时累积分布函数(越高越好)。
请注意，SATConame2011应用程序跟踪只有300个实例，而2019年和2020年的另外两个基准测试集分别由400个明显更难的实例组成。
我们的群集具有两个Intel(R)Xeon(R)CPU E5-2620 [email protected]和每个节点上128 GB的主内存，因此略低一些，但与竞争中使用的StarExec群集相当。作为时间限制，我们使用了5000秒，因为它现在在比赛中很常见。2011和2019年的主内存限制为8 GB，以最大限度地利用我们的集群。对于2020年，我们将内存限制提高到32 GB，这使得所有的解算器都可以保持在内存限制以下(组织者宣布了24 GB的内存限制，但实际使用的内存是128 GB)。
以下提交给SAT大赛2020的源代码获得了主赛道第一名和主赛道不能满足的实例第一名：
阿明·比尔，卡塔林·法泽卡斯，马蒂亚斯·弗洛里，马克西米利安·海辛格。CaDiCal、Kissat、Paraco oba、Plingling和Treengling将参加2020年SAT大赛。将出现在2020年SAT竞赛论文集-解算器和基准描述中。[纸张|bibtex|kissat|cadical|paraco oba|plingling|treengering]。
阿明·比尔和马蒂亚斯·弗洛里。追踪目标阶段第11期SAT(POS&39；20)网络空间语用学研讨会，2020年7月3日。[幻灯片[视频|实验]