Reduction of interpolants for logic synthesis

John D. Backes, Marc D. Riedel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations


Craig Interpolation is a state-of-the-art technique for logic synthesis and verification, based on Boolean Satisfiability (SAT). Leveraging the efficacy of SAT algorithms, Craig Interpolation produces solutions quickly to challenging problems such as synthesizing functional dependencies and performing bounded model-checking. Unfortunately, the quality of the solutions Is often poor. When interpolants are used to synthesize functional dependencies, the resulting structure of the functions may be unnecessarily complex. In most applications to date, interpolants have been generated directly from the proofs of unsatlsfiablllty that are provided by SAT solvers. In this work, we propose efficient methods based on incremental SAT solving for modifying resolution proofs In order to obtain more compact interpolants. This, In turn, reduces the cost of the logic that is generated for functional dependencies.

Original languageEnglish (US)
Title of host publication2010 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2010
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages8
ISBN (Print)9781424481927
StatePublished - 2010
Event2010 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2010 - San Jose, CA, United States
Duration: Nov 7 2010Nov 11 2010

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152


Other2010 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2010
Country/TerritoryUnited States
CitySan Jose, CA


Dive into the research topics of 'Reduction of interpolants for logic synthesis'. Together they form a unique fingerprint.

Cite this