基于反例与证明抽象的单实例增量SAT求解方法
计算机科学中的逻辑
2010-08-13 v1
摘要
本文提出了一种高效、组合的位级验证抽象方法，将两种广泛使用的抽象方法——基于反例的抽象（CBA）和基于证明的抽象（PBA）——结合为单一、增量的SAT问题，以自底向上的方式交织CBA和PBA来构建抽象。本文论证了新方法在概念和实现上均比先前方法更简单。额外的好处是，PBA部分无需证明日志记录，从而允许使用更广泛的SAT求解器。
引用
@article{arxiv.1008.2021,
title = {A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction},
author = {Niklas Een and Alan Mishchenko and Nina Amla},
journal= {arXiv preprint arXiv:1008.2021},
year = {2010}
}
备注
Accepted for FMCAD 2010