Set-cover-based critical implications selection to improvesat-based bounded model checking
Mahmoud Elbayoumi, Michael S. Hsiao, Mustafa Y. ElNainay · 2013
The effectiveness of Satisfiability (SAT)-based Bounded Model Checking (BMC) critically relies on the deductive power of the BMC instance. Although implication relationships have been used to help SAT solver to make more deductions, too many such implications would result in a large number of clauses and potentially degrade the underlying SAT solver performance. In this paper, we have formulated clause selection as a set-cover problem. Secondly, we have proposed a novel greedy strategy for optimal selection of static logic clauses. This technique maximizes the number of literals that can be deduced by the SAT solver during the Boolean Constraint Propagation (BCP) operation. Our strategy improves BMC by 1.74x against the case where all extended implications were added to the BMC instance. Compared with the original BMC without any implications, up to 55.32x speedup can be achieved.