Search

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, 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. [ABSTRACT FROM AUTHOR]

We address the problem of reducing the size of Craig’s interpolants used in SAT-based model checking. Craig’s interpolants are AND-OR circuits, generated by post-processing refutation proofs of SAT solvers. Being highly redundant, their compaction is typically tackled by reducing the proof graph and/or by exploiting standard logic synthesis techniques. In this paper, we propose a set of ad-hoc logic synthesis functions that, revisiting known logic synthesis approaches, specifically address speed and scalability. Though general and not restricted to interpolants, these techniques target the main sources of redundancy in combinational circuits. This paper includes an experimental evaluation, showing the benefits of the proposed techniques, on a set of benchmark interpolants arising from hardware model checking problems. [ABSTRACT FROM AUTHOR]