Minimizing Counterexample with Unit Core Extraction and Incremental SAT

Abstract. It is a hotly researching topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. K Ravi proposes a two-stages counterexample minimization algorithm. This algorithm is the most effective one among all existing approaches, but time overhead of its second stage(called BFL) 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 unit core extraction and incremental SAT. First, for every unsatisfiable instance of BFL, we perform unit core extraction algorithm to extract the set of variables that are sufficient to lead to conflict, 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 searche...

• Type: Conference
• Year: 2005
• Where: VMCAI
• Authors: ShengYu Shen, Ying Qin, Sikun Li
• Keywords: Counterexample Minimization Algorithm, Irrelevant Variables, Software Engineering, Unit Core Extraction, VMCAI 2005