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

A Fast Counterexample Minimization Algorithm with Refutation Analysis and Incremental SAT

作　　者：沈胜宇[1] 李思昆[1] 

机构地区：[1]国防科学技术大学计算机学院,湖南长沙410073

出　　处：《软件学报》2006年第5期1034-1041,共8页Journal of Software

基　　金：国家自然科学基金~~

摘　　要：使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的BFL（brute force lifting）算法,其时间开销过大.为此,提出一种基于悖论分析和增量式SAT（boolean satisfiablilty problem）的快速反例压缩算法.首先,根据反证法和排中律原理,该算法对每一个自由变量v,构造一个SAT问题,以测试v是否能够避免反例.而后对其中不可满足的SAT问题,进行悖论分析,抽取出导致悖论的变量集合.所有不属于该集合的变量,均可作为无关变量直接剔除.同时,该算法使用增量式SAT求解方法,以避免反复搜索冗余状态空间.理论分析和实验结果表明,与BFL算法相比,该算法能够在不损失压缩率的前提下获得1～2个数量级的加速.It is a hot research topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. BFL （brute force lifting） algorithm is the most effective one among all the existing approaches, but its time overhead is very large due to one call to SAT （boolean satisfiability problem） solver per candidate variable to be eliminated. So a faster algorithm based on refutation analysis and incremental SAT is proposed. The counterexample minimization problem is first translated into a set of SAT instances for each free variable v, to determine if v can prevent the counterexample. Then refutation analysis on those UNSAT （unsatisfiable） instances is performed, to extract the set of variables that lead to refutation. All variables that don＇t belong to this set can be eliminated directly as irrelevant variables. At the same time, the incremental SAT approach is employed to share conflict clauses between similar instances, such that the overlapped state space can be prevented from being searched repeatedly. Theoretical analysis and experimental result show that this approach run much faster than BFL algorithm, and with minor lost in reduction rate.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]