文献阅读——Single Clause Assumption without Activation Literals to Speed-up IC3

@inproceedings{DBLP:conf/fmcad/FroleyksB21,
  author       = {Nils Froleyks and
                  Armin Biere},
  title        = {Single Clause Assumption without Activation Literals to Speed-up {IC3}},
  booktitle    = {Formal Methods in Computer Aided Design, {FMCAD} 2021, New Haven,
                  CT, USA, October 19-22, 2021},
  pages        = {72--76},
  publisher    = {{IEEE}},
  year         = {2021},
  url          = {https://doi.org/10.34727/2021/isbn.978-3-85448-046-4\_15},
  doi          = {10.34727/2021/ISBN.978-3-85448-046-4\_15},
  timestamp    = {Tue, 07 Dec 2021 17:02:16 +0100},
  biburl       = {https://dblp.org/rec/conf/fmcad/FroleyksB21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

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 im plement 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.

摘要——我们将成熟的基于假设的增量SAT求解器接口扩展到了子句，允许添加一个与命题假设具有相同寿命的临时子句。我们的方法高效且易于在现代CDCL-based求解器中实现。与之前的方法相比，它不会带来任何内存开销，也不会因为禁用激活子句而减慢求解器的速度，从而消除了需要像IC3这样的SAT求解器重新启动的必要。在命题和子句假设下学习的所有子句都是安全的，不会因为包含激活子句而隐式失效。这些变化提高了学习子句的质量，从而为IC3提供了更好的泛化。我们在SAT求解器CaDiCaL中实现了该扩展，并与模型检查器ABC中的IC3实现进行了评估。在最近的硬件模型检查竞赛的基准测试上进行的实验显示，SAT调用平均速度加快，每个验证实例的调用次数减少，从而显著提高了模型检查时间。