Reduction of Interpolants for Logic Synthesis

Slides

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 Interpo- lation 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 unsatisfiability 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.