Selecting Critical Implications with Set-Covering Formulation for SAT-Based Bounded Model Checking

Provided by: Institute of Electrical & Electronic Engineers
Topic: Hardware
Format: PDF
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, the authors propose a framework for a parallel deduction engine to reduce implication learning time. They propose a novel set-cover technique for optimal selection of constraint clauses.

Find By Topic