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

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