A Faster Counterexample Minimization Algorithm Based on Refutation Analysis
Shengyu Shen, Ying Qin, SiKun Li · Design, Automation, and Test in Europe · 2005
A hot research topic is the elimination of irrelevant variables from a counterexample, to make it more easily understood. The BFL (brute force lifting) 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 the SAT (satisfiability) solver for each candidate variable to be eliminated. The key to reducing time overhead is to eliminate multiple variables simultaneously. Therefore, we propose a faster counterexample minimization algorithm based on refutation analysis. We perform refutation analysis on those UNSAT instances of BFL, to extract the set of variables that lead to UNSAT. All variables not belonging to this set can be eliminated simultaneously as irrelevant variables. Thus we can eliminate multiple variables with only one call to the SAT solver. Theoretical analysis and experimental results show that our algorithm can be 2 to 3 orders of magnitude faster than the existing BFL algorithm, and with only minor loss in counterexample minimization ability.