loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Design, Automation and Test in Europe (DATE'05) Volume 2
A Faster Counterexample Minimization Algorithm Based on Refutation Analysis
Munich, Germany
March 07-March 11
ISBN: 0-7695-2288-2
ShengYu Shen, National University of Defence Technology
Ying Qin, National University of Defence Technology
SiKun Li, National University of Defence Technology
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.
Citation:
ShengYu Shen, Ying Qin, SiKun Li, "A Faster Counterexample Minimization Algorithm Based on Refutation Analysis," date, vol. 2, pp.672-677, Design, Automation and Test in Europe (DATE'05) Volume 2, 2005
Usage of this product signifies your acceptance of the Terms of Use.