Reducing interpolant circuit size through SAT-based weakening

We address the problem of reducing the size of Craig's interpolants (ITPs) used in SAT-based model checking. Whereas it is well known that ITPs are highly redundant, their compaction is typically tackled by reducing the proof graph and/or by exploiting standard logic synthesis techniques. Furthermore, strengthening and weakening have been studied as options to control ITP quality. In this paper,1 we propose an SAT-based ITP weakening/strengthening technique, for ITP compaction, where the UNSAT core extracted from an additional SAT query is used to obtain a gate-level abstraction of the ITP. The abstraction introduces fresh new variables at gate cuts that must be quantified out in order to obtain a valid ITP. We show how to efficiently quantify them out, by working on a negation normal form representation of the circuit. This paper includes an experimental evaluation, showing the benefits of the proposed approach, on a set of benchmark ITPs arising from hardware model checking problems.