A Novel Technique for Computing Craig Interpolants in Satisfiabilility Modulo the Theory of Integer Linear Arithmetic

In this thesis we present a solution to the interpolation problem of LA(Z) based on interpolant generation for conjunctions of LA(Z) equalities and weak inequalities. Although our approach was inspired by Brillout et al.’s interpolating sequent calculus, it differs from the latter in that our interpolation method is based on cutting-plane proofs of unsatisfiability rather than sequent-calculus proofs and consists of interpolation rules built to reflect the cutting plane rules. The proposed algorithm has been implemented within MATHSAT SMT solver and tested for simple cases