IC3 的触发子句推进策略

我们提出了一种改进著名的 IC3 算法的方法，用于检测有限状态系统的安全属性。我们收集算法在子句传播阶段由 SAT 求解器计算的模型，并将其用作见证，解释为何相应的子句无法向前推进。仅当某个子句的见证模型证伪了新添加的子句时，重新检查该子句以进行推进才有意义。由于这种触发测试既计算成本低廉又具有足够的精度，我们可以始终尽可能地将子句推进到最远。实验表明，该策略显著提高了 IC3 的性能。