A fast counterexample minimization approach with refutation analysis and incremental SAT

ABSTRACT

It is a hotly research topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. BFL algorithm is the most effective Counterexample minimization algorithm compared to all other approaches, but its run time overhead is very large due to one call to SAT solver per candidate variable to be eliminated. So we propose a faster counterexample minimization algorithm based on refutation analysis and incremental SAT. First, for every UNSAT instance of BFL, we perform refutation analysis to extract the set of variables that lead to UNSAT, all variables not belong to this set can be eliminated simultaneously. In this way, we can eliminate many variables with only one call to SAT solver. At the same time, we employ incremental SAT approach to share learned clauses between similar instances of BFL, to prevent overlapped state space from being searched repeatedly. Theoretic analysis and experiment result shows that, our approach can be 1 to 2 orders of magnitude faster than BFL, and still retain the minimization ability of BFL.

REFERENCES

• 1: K Ravi and Fabio Somenzi. Minimal Assignments for Bounded Model Checking. In TACAS'04, pages 31--45, 2004. LNCS 2988.
• 2: HoonSang Jin , Kavita Ravi , Fabio Somenzi, Fate and Free Will in Error Traces, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.445-459, April 08-12, 2002
• 3: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 4: Alessandro Cimatti , Edmund M. Clarke , Enrico Giunchiglia , Fausto Giunchiglia , Marco Pistore , Marco Roveri , Roberto Sebastiani , Armando Tacchella, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.359-364, July 27-31, 2002
• 5: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 6: http://www.cbl.ncsu.edu/CBL_Docs/iscas89.html
• 7: N. Een and N. Sorensson. Temporal Induction by Incremental SAT Solving. In BMC'03.
• 8: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California