arXiv:2501.18612v2 Announce Type: cross 摘要：IC3算法，也被称为PDR（Procedure Directed Reasoning），是一种基于SAT求解器的模型检查算法，由于其高效性、可扩展性和完整性，在近年来对领域产生了显著影响。该算法利用SAT求解器解决一系列与相对归纳相关的SAT查询。在这篇论文中，我们基于对我们观察到的这些SAT查询的独特特征进行了一些建立在IC3上的SAT求解器优化。通过观察到SAT查询不一定需要对所有变量进行决策，我们在每次求解过程前计算需要决策的变量子集，同时确保结果不受影响。此外，注意到VSIDS中的二叉堆操作开销不小，我们用桶取代二叉堆，以实现常数时间操作。进一步地，我们支持临时子句而无需为每次求解过程分配新的激活变量，从而消除了重置求解器的需求。我们开发了一种新的轻量级CDCL SAT求解器GipSAT，集成了这些优化。全面的评估突显了GipSAT所取得的性能提升。具体来说，基于GipSAT的IC3在求解时间上比基于MiniSat实现的IC3平均速度快了3.61倍。