论文部分内容阅读
近些年来，基于SAT的限界模型检测方法作为基于BDD的限界模型检测方法的一种有效补充，已经得到了一定的发展。其中，大部分的研究成果都集中在了使用该方法来进行系统查错方面，而在正确性性质的验证上一直难有突破。原因在于正确性性质的验证依赖于一个完备上界，而这个完备上界在限界模型检测方法中很难实现。对传统限界模型检测中的编码方式进行相应改变，就能够在一定程度上解决这一问题，进行正确性性质的验证。在此基础上对该编码方法进行改进，从而提高它的求解效率，扩大其应用领域。