Reducing Interpolant Circuit Size Through SAT-Based Weakening

• Published in: IEEE transactions on computer-aided design of integrated circuits and systems 2020-07, Vol.39 (7), p.1524-1531
• Main Authors: Cabodi, G., Camurati, P. E., Palena, M., Pasini, P., Vendraminetto, D.
• Format: Article
• Language: English
• Subjects: Boolean functions; Canonical forms; Circuits; Compaction; Data structures; Hardware; Interpolation; Logic gates; Logic synthesis; Model checking
• ISSN: 0278-0070; 1937-4151
• DOI: 10.1109/TCAD.2019.2915317

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. 1 Some of the techniques here described were presented in a preliminary version at FMCAD'16 [1] .