Restructuring Resolution Refutations for Interpolation

Abstract

Interpolants are the cornerstone of several approximate verification techniques. Current interpolation techniques restrict the search heuristics of the underlying decision procedure to compute interpolants, incurring a negative impact on performance, and apply primarily to the lazy proof explication framework. We bridge the gap between fast decision procedures that aggressively use propositional reasoning and slower interpolating decision procedures by extending the scope of the latter to non-lazy approaches and relaxing the restrictions on search heuristics. Both are achieved by combining a simple set of transformations on resolution refutations. Our experiments show that this method leads to speedups when computing interpolants and to reductions in proof size.