Selecting critical implications with set-covering formulation for SAT-based Bounded Model Checking

摘要

The effectiveness of 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, frequently an excessive number of implications has been used. Too many such implications can result in a large number of clauses that could potentially degrade the underlying SAT solver performance. In this paper, we first propose a framework for a parallel deduction engine to reduce implication learning time. Secondly, we propose a novel set-cover technique for optimal selection of constraint clauses. This technique depends on maximizing the number of literals that can be deduced by the SAT solver during the BCP (Boolean Constraint Propagation) operation. Our parallel deduction engine can achieve a 5.7× speedup on a 36-core machine. In addition, by selecting only those critical implications, our strategy improves BMC by another 1.74× against the case where all extended implications were added to the BMC instance. Compared with the original BMC without any implication clauses, up to 55.32× speedup can be achieved.