Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Interpolant based Decision Procedure for Quantifier-free Presburger Arithmetic

Shuvendu Lahiri and Krishna Kumar Mehra

Abstract

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.

Details

Publication typeArticle
Published inJournal on Satisfiability, Boolean Modeling and Computation (JSAT '07)
Pages0
NumberMSR-TR-2005-121
InstitutionMicrosoft Research
> Publications > Interpolant based Decision Procedure for Quantifier-free Presburger Arithmetic