Interpolant generation without constructing resolution graph.
Journal
2009 International Conference on Computer-Aided Design, ICCAD 2009, San Jose, CA, USA, November 2-5, 2009
Pages
9-12
Date Issued
2009
Author(s)
Abstract
In this paper, we proposed a novel interpolant generation algorithm without constructing the resolution graph of the unsatisfiability proof. Our algorithm generates the interpolant by building sub-interpolants from conflict analyses and then merges them based on the last decision conflict. The experimental results show that our algorithm has the advantages over the prior interpolant generation techniques in both memory usage and interpolation circuit size. Copyright 2009 ACM.
SDGs
Other Subjects
Computer aided design; Circuit size; Conflict analysis; Decision conflicts; Generation algorithm; Generation techniques; Interpolants; Memory usage; Resolution graphs; Interpolation
Type
conference paper