软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2006年
5期
1034-1041
,共8页
模型检验%反例压缩%悖论分析%增量式求解%安全断言
模型檢驗%反例壓縮%悖論分析%增量式求解%安全斷言
모형검험%반례압축%패론분석%증량식구해%안전단언
使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的BFL(brute force lifting)算法,其时间开销过大.为此,提出一种基于悖论分析和增量式SAT(boolean satisfiablilty problem)的快速反例压缩算法.首先,根据反证法和排中律原理,该算法对每一个自由变量v,构造一个SAT问题,以测试v是否能够避免反例.而后对其中不可满足的SAT问题,进行悖论分析,抽取出导致悖论的变量集合.所有不属于该集合的变量,均可作为无关变量直接剔除.同时,该算法使用增量式SAT求解方法,以避免反复搜索冗余状态空间.理论分析和实验结果表明,与BFL算法相比,该算法能够在不损失压缩率的前提下获得1～2个数量级的加速.
使用反例壓縮算法,從反例中剔除冗餘信息,從而使反例易于理解,是目前的研究熱點.然而,目前壓縮率最高的BFL(brute force lifting)算法,其時間開銷過大.為此,提齣一種基于悖論分析和增量式SAT(boolean satisfiablilty problem)的快速反例壓縮算法.首先,根據反證法和排中律原理,該算法對每一箇自由變量v,構造一箇SAT問題,以測試v是否能夠避免反例.而後對其中不可滿足的SAT問題,進行悖論分析,抽取齣導緻悖論的變量集閤.所有不屬于該集閤的變量,均可作為無關變量直接剔除.同時,該算法使用增量式SAT求解方法,以避免反複搜索冗餘狀態空間.理論分析和實驗結果錶明,與BFL算法相比,該算法能夠在不損失壓縮率的前提下穫得1～2箇數量級的加速.
사용반례압축산법,종반례중척제용여신식,종이사반례역우리해,시목전적연구열점.연이,목전압축솔최고적BFL(brute force lifting)산법,기시간개소과대.위차,제출일충기우패론분석화증량식SAT(boolean satisfiablilty problem)적쾌속반례압축산법.수선,근거반증법화배중률원리,해산법대매일개자유변량v,구조일개SAT문제,이측시v시부능구피면반례.이후대기중불가만족적SAT문제,진행패론분석,추취출도치패론적변량집합.소유불속우해집합적변량,균가작위무관변량직접척제.동시,해산법사용증량식SAT구해방법,이피면반복수색용여상태공간.이론분석화실험결과표명,여BFL산법상비,해산법능구재불손실압축솔적전제하획득1～2개수량급적가속.
