文献阅读-We extend the well-established assumption-based interface of incremental SAT solvers to clauses, allowing the addition of a temporary clause that has the same lifespan as literal assumptions.

Abstract：

We extend the well-established assumption-based interface of incremental SAT solvers to clauses, allowing the addition of a temporary clause that has the same lifespan as literal assumptions.

Our approach is efficient and easy to implement in modern CDCL-based solvers.

Compared to previous approaches, it does not come with any memory overhead and does not slow down the solver due to disabled activation literals, thus eliminating the need for algorithms like IC3 to restart the SAT solver.

All clauses learned under literal and clause assumptions are safe to keep and not implicitly invalidated for containing an activation literal. These changes increase the quality of learned clauses, resulting in better generalization for IC3.

We implement the extension in the SAT solver CaDiCaL and evaluate it with the IC3 implementation in the model checker ABC. Our experiments on the benchmarks from a recent hardware model checking competition show a speedup for the average SAT call and a reduction in number of calls per verification instance, resulting in a substantial improvement in model checking time.

符号模型检查算法IC3

许多应用需要逐步解决一系列相关的SAT问题[2]，[3]，利用inprocessing技术[4]，[5]，[6]，使现代SAT求解器如此高效。Many applications require solving a sequence of related SAT problems incrementally [2], [3], making use of inprocessing techniques [4], [5], [6] that make modern SAT solvers so efficient.

与其他基于sat的增量技术(如有界模型检查(BMC)[7]、[8]和k-归纳[9]、[10])相比， IC3不依赖于展开转换函数。因此，IC3姿态的SAT查询明显更小，求解速度更快。但是，IC3在一个模型检查过程中进行的查询数量要高得多.

We illustrate the kind of queries that IC3 makes in the following example.