SAT技术的生命周期
Life span of SAT techniques
AI总结：
该研究针对SAT求解器CaDiCaL的4项特性，在2009-2022年SAT竞赛基准上通过逐一激活/禁用的方式测试，最终未能证实“禁用特性总有害、技术生命周期有限、特性相互模拟”三个假设。
摘要：
本文针对SAT求解器CaDiCaL的4项不同特性——阻塞子句消除、活化（vivification）、即时自蕴含归约、提升变量消元界值，在2009年至2022年的SAT Competitions基准测试集上展开研究。我们通过逐一激活、逐一禁用这些特性的方式开展研究。针对实验我们提出三个假设：（i）禁用特性始终会产生负面影响；（ii）这些技术的生命周期有限；（iii）各特性之间存在相互模拟的关系。我们的实验未能证实其中任何一个假设。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
