基于悖论分析和增量求解的快速反例压缩算法

摘要：

使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的BFL(brute force lifting)算法,其时间开销过大.为此,提出一种基于悖论分析和增量式SAT(boolean satisfiablilty problem)的快速反例压缩算法.首先,根据反证法和排中律原理,该算法对每一个自由变量v,构造一个SAT问题,以测试v是否能够避免反例.而后对其中不可满足的SAT问题,进行悖论分析,抽取出导致悖论的变量集合.所有不属于该集合的变量,均可作为无关变量直接剔除.同时,该算法使用增量式SAT求解方法,以避免反复搜索冗余状态空间.理论分析和实验结果表明,与BFL算法相比,该算法能够在不损失压缩率的前提下获得1～2个数量级的加速.

关键词：模型检验、反例压缩、悖论分析、增量式求解、安全断言

所属期刊栏目：17

分类号：TP301(计算技术、计算机技术)

资助基金：中国科学院资助项目60573173

在线出版日期：2006-05-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：1034-1041