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

• 作者: 李思昆 沈胜宇
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检验 反例压缩 悖论分析 增量式求解 安全断言
• 年，卷（期）: 2006,（5）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 1034-1041
• 页数: 8页
• 分类号: TP301
• 字数: 6912字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李思昆	国防科学技术大学计算机学院	133	1339	18.0	31.0
2	沈胜宇	国防科学技术大学计算机学院	8	30	3.0	5.0