Interpolant based Decision Procedure for Quantifier-Free Presburger Arithmetic

Abstract

Recently, off-the-shelf Boolean SAT solvers have been used to construct ground decision procedures for various theories, including Quantifier-Free Presburger (QFP) arithmetic. One such approach (often called the eager approach) is based on a satisfiability-preserving translation to a Boolean formula. Eager approaches are usually based on encoding integers as bit-vectors and su er from the loss of structure and sometime very large size for the bit-vectors.

In this paper, we present a decision procedure for QFP that is based on alternately under and over-approximating a formula, where Boolean interpolants are used to compute the overapproximation. The novelty of the approach lies in using information from each phase (either underapproximation or overapproximation) to improve the other phase. Our preliminary experiments indicate that the algorithm consistently outperforms approaches based on eager and very lazy methods, on a set of verification benchmarks. In our experience, the use of interpolants results in better abstractions being generated compared to an earlier method based on proofs directly.