Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

The problem of computing Craig interpolants in SAT and SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for interpolant generation have been presented for some theories of interest —including that of equality and uninterpreted functions

$({\mathcal{EUF}})$

, linear arithmetic over the rationals

$({\mathcal{LA}(\mathbb{Q})})$

, and their combination— and they are successfully used within model checking tools. For the theory of linear arithmetic over the integers

$({\mathcal{LA}(\mathbb{Z})})$

, however, the problem of finding an interpolant is more challenging, and the task of developing efficient interpolant generators for the full theory

${\mathcal{LA}(\mathbb{Z})}$

is still the objective of ongoing research.

In this paper we try to close this gap. We build on previous work and present a novel interpolation algorithm for SMT

$({\mathcal{LA}(\mathbb{Z})})$

, which exploits the full power of current state-of-the-art SMT

$({\mathcal{LA}(\mathbb{Z})})$

solvers. We demonstrate the potential of our approach with an extensive experimental evaluation of our implementation of the proposed algorithm in the

MathSAT

SMT solver.