%0 Journal Article
%T A Fast Counterexample Minimization Algorithm with Refutation Analysis and Incremental SAT<br>基于悖论分析和增量求解的快速反例压缩算法
%A SHEN Sheng-Yu
%A LI Si-Kun
%A <br>沈胜宇
%A 李思昆
%J 软件学报
%D 2006
%I 
%X 使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的BFL(brute force lifting)算法,其时间开销过大.为此,提出一种基于悖论分析和增量式SAT(boolean satisfiablilty problem)的快速反例压缩算法.首先,根据反证法和排中律原理,该算法对每一个自由变量v,构造一个SAT问题,以测试v是否能够避免反例.而后对其中不可满足的SAT问题,进行悖论分析,抽取出导致悖论的变量集合.所有不属于该集合的变量,均可作为无关变量直接剔除.同时,该算法使用增量式SAT求解方法,以避免反复搜索冗余状态空间.理论分析和实验结果表明,与BFL算法相比,该算法能够在不损失压缩率的前提下获得1～2个数量级的加速.
%K model checking
%K counterexample minimization
%K refutation analysis
%K incremental SAT
%K safety assertion<br>模型检验
%K 反例压缩
%K 悖论分析
%K 增量式求解
%K 安全断言
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=DC84253F3F921886&yid=37904DC365DD7266&vid=BCA2697F357F2001&iid=94C357A881DFC066&sid=78996380F3108204&eid=8F39F7FDA07C2566&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=15