Interpolant based Decision Procedure for Quantifier-Free Presburger Arithmetic
Shuvendu K. Lahiri, Krishna K. Mehra · Journal on Satisfiability Boolean Modeling and Computation · 2007
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 satisfia