It is a hot research topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. The BFL algorithm is the most effective counterexample minimization algorithm compared to all other approaches. But its time overhead is very large due to one call to SAT solver for each candidate variable to be eliminated. The key to reduce time overhead is to eliminate multiple variables simultaneously. Therefore, we propose a faster counterexample minimization algorithm based on refutation analysis in this paper. We perform refutation analysis on those UNSAT instances of BFL, to extract the set of variables that lead to UNSAT. All variables not belong to this set can be eliminated simultaneously as irrelevant variables. Thus we can eliminate multiple variables with only one call to SAT solver. Theoretical analysis and experiment result shows that, our algorithm can be 2 to 3 orders of magnitude faster than existing BFL algorithm, and with only minor lost in counterexample minimization ability.
展开▼
