摘要
使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的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.
出处
《软件学报》
EI
CSCD
北大核心
2006年第5期1034-1041,共8页
Journal of Software
基金
国家自然科学基金~~
关键词
模型检验
反例压缩
悖论分析
增量式求解
安全断言
model checking
counterexample minimization
refutation analysis
incremental SAT
safety assertion
