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 circuit compaction is typically considered as an implementation problem, tackled with standard logic synthesis techniques. We propose a three step interpolant computation process, specifically oriented to scalability, in which we: (1) exploit an existing technique to detect and remove redundancies in refutation proofs, (2) apply customized light weight combinational logic reductions (constant propagation, ODC-based simplifications, and BDD-based sweeping) directly on the proof graph data structure, (3) introduce an ad-hoc combinational reduction procedure for large interpolant circuits, based on the incrementality and divide-and-conquer paradigms. The main contributions of our approach are represented by the overall approach, the proposed combinational reduction technique, and a detailed experimental evaluation of the interpolant generation process, on a set of benchmarks from the Hardware Model Checking Competitions 2013 and 2014.