Increasing the deducibility in CNF instances for efficient SAT-based bounded model checking

In this paper, we propose low-cost static deduction techniques by combining binary resolution and static logic implications to efficiently extract invariant relations from a gate-level netlist. We show that processing our techniques across the circuit nodes helps us to learn highly nontrivial relations. All the relations learned in a user-defined finite window are then quickly replicated over the entire bound for BMC. These powerful relations, when added as new constraint clauses to the original formula, help to significantly increase the deductive power for the SAT engine, thereby pruning a larger portion of the search space. Experimental results on ISCAS89 and ITC99 benchmarks show that more than an order of magnitude performance improvement can be obtained using the proposed learning techniques.