In this paper we take 4 different features of the SAT solver CaDiCaL, blocked clause elimination, vivification, on-the-fly self subsumption, and increasing the bound of variable elimination over the SAT Competitions benchmarks between 2009 and 2022. We study these features by both activating them one-by-one and deactivating them one-by-one. We have three hypothesis regarding the experiments: (i) disabling features is always harmful; (ii) the life span of the techniques is limited; and (iii) features simulate each other. Our experiments cannot confirm any of the hypothesis.

翻译：本文选取SAT求解器CaDiCaL的四种不同特征——阻塞子句消除、激活子句细化、动态自归约以及变量消除边界递增——基于2009年至2022年SAT竞赛基准测试展开研究。我们通过逐一启用和禁用这些特征来考察其性能影响。针对实验提出三项假设：（i）禁用特征始终对性能有害；（ii）各技术的生命周期有限；（iii）不同特征之间存在相互模拟效应。实验结果表明，上述假设均未得到证实。