Optimization techniques for craig interpolant compaction in unbounded model checking

This paper addresses the problem of reducing the size of Craig interpolants generated within inner steps of SAT-based Unbounded Model Checking. Craig interpolants are obtained from refutation proofs of unsatisfiable SAT runs, in terms of and/or circuits of linear size, w.r.t. the proof. Existing techniques address proof reduction, whereas interpolant compaction is typically considered as an implementation problem, tackled using standard logic synthesis techniques. We propose an integrated three step process, in which we: (1) exploit an existing technique to detect and remove redundancies in refutation proofs, (2) apply combinational logic reductions (constant propagation, ODC-based simplifications, and BDD-based sweeping) directly on the proof graph data structure, (3) eventually apply ad hoc combinational logic synthesis steps on interpolant circuits. The overall procedure is novel (as well as parts of the above listed steps), and represents an advance w.r.t. the state-of-the art. The paper includes an experimental evaluation, showing the benefits of the proposed technique, on a set of benchmarks from the Hardware Model Checking Competition 2011.