Interpolant based Decision Procedure for Quantifier-free Presburger Arithmetic

Recently, there have been two popular approaches for SAT-based theorem proving — eager and lazy. Eager approaches are based on a satisfiability preserving translation to a Boolean formula, whereas the lazy approaches perform an incremental translation to SAT. Eager approaches are usually based on encoding integers as bit-vectors and suffer from lack of structure and sometime very large size for the bit-vectors. Lazy approaches suffer from large number of invocations of theory decision procedures and the complexity of the decision procedures for integer linear arithmetic. In this paper, we present a decision procedure for Quantifier-free Presburger arithmetic that is based on alternately under and over-approximating a formula. We use Boolean interpolants to compute the overapproximation. The algorithm seems to address the bottlenecks of both eager and lazy approaches, and improve on both. The algorithm consistently outperforms approaches based on eager and lazy methods on a set of verification benchmarks.