arXiv:2501.18612v1 声称类型: cross 摘要: IC3 算法，也被称为 PDR，是一种基于 SAT 的模型检查算法，由于其高效性、可扩展性和完整性，在近年来对领域产生了重大影响。该算法利用 SAT 求解器解决了与相对归纳相关的系列 SAT 查询。基于对 IC3 中 SAT 查询的独特特征的观察，本文介绍了 GipSAT，一个针对 IC3 轻量级且专门优化的 SAT 求解器。通过观察到 SAT 查询不一定需要对所有变量进行决策，GipSAT 在每次求解前计算出需要决策的变量子集，同时确保结果不受影响。通过观察到 VSIDS 中二叉堆操作的开销不容忽视，GipSAT 使用桶而不是二叉堆来实现常数时间操作。GipSAT 支持临时子句，无需在每次求解前分配新的激活变量，从而避免了重置求解器的必要性。综合评估显示，GipSAT 实现了显著的性能提升。与 Minisat 相比，GipSAT 在求解时间上平均加速了 3.61 倍。