The Effect of Scrambling CNFs
The Effect of Scrambling CNFs
复制标题
加扰 CNF 的效果
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Marijn J. H. Heule
中科院分区：
文献类型：
--
作者：
Armin Biere;Marijn J. H. Heule
关于SAT求解器和一般不同或新算法如何在比赛中以及在论文中更重要的是，这是一场持续数十年的辩论。通常对现有基准进行评估。很少使用交叉验证和其他避免过度拟合的方法。在本文中，我们重新审视了在早期比赛中还使用基准的旧观念。争夺的目标是使此类评估的结果更加强大。我们提出了一种新方法，用于扰乱CNF，从保持炒cnf接近原始CNF的效果逐渐增加，到完成变量，条款和文字阶段的随机置换。我们使用这种方法来争夺最后两个SAT比赛的基准测试，并用最佳求解器解决了上一次SAT比赛的主要轨道。正如预期的那样，我们的实验结果表明，争夺对单个求解器的性能具有重大影响，但令人惊讶的是，对求解器的排名几乎没有影响。因此，我们认为，只有使用我们的争夺方法不足以提高竞争和总体评估的鲁棒性。
It has been an ongoing, decades-long debate about how SAT solvers and in general different or new algorithms should be evaluated and compared both in competitions and more importantly in papers. Evaluations are usually performed on existing benchmarks. Cross-validation and other means to avoid over-fitting are rarely used. In this paper we revisit the old idea of scrambling benchmarks also used in early competitions. Scrambling has the goal to make results of such evaluations more robust. We present a new method for scrambling CNFs, which allows to gradually increase the effect of scrambling, from keeping the scrambled CNF close to the original CNF, to complete random permutation of variables, clauses, and phases of literals. We used this method to scramble benchmarks from the last two SAT competitions and solved them with the best solvers in the main track of the last SAT competition. As expected our experimental results suggest that scrambling has a substantial effect on the performance of individual solvers but surprisingly has little effect on rankings among solvers. As a consequence we argue that only using our method of scrambling is not enough to increase robustness of competitions and evaluations in general.