Computing interpolants without proofs

Abstract. We describe an incremental algorithm for computing inter-polants for a pair ϕA, ϕB of formulas in propositional logic. In contrast with the common approaches, our method does not require a proof of unsatisfiability of ϕA ∧ ϕB, and can be realized using any SAT solver as a black box. We achieve this by combining model enumeration with the ability to easily generate interpolants in the special case that one of the formulas is a cube.