Single Clause Assumption without Activation Literals to Speed-up IC3

We extend the well-established assumption-basedinterface of incremental SAT solvers to clauses, allowing theaddition of a temporary clause that has the same lifespan asliteral assumptions. Our approach is efficient and easy to im-plement in modern CDCL-based solvers. Compared to previousapproaches, it does not come with any memory overhead and doesnot slow down the solver due to disabled activation literals, thuseliminating the need for algorithms like IC3 to restart the SATsolver. All clauses learned under literal and clause assumptionsare safe to keep and not implicitly invalidated for containing anactivation literal. These changes increase the quality of learnedclauses, resulting in better generalization for IC3. We implementthe extension in the SAT solver CaDiCaL and evaluate it with theIC3 implementation in the model checker ABC. Our experimentson the benchmarks from a recent hardware model checkingcompetition show a speedup for the average SAT call and areduction in number of calls per verification instance, resultingin a substantial improvement in model checking time.