%0 Journal Article %A Seshia, Sanjit A. %A Bryant, Randal %D 2001 %T Deciding quantifier-free Presburger formulas using finite instantiation based on parameterized solution bounds %U https://kilthub.cmu.edu/articles/journal_contribution/Deciding_quantifier-free_Presburger_formulas_using_finite_instantiation_based_on_parameterized_solution_bounds/6604652 %R 10.1184/R1/6604652.v1 %2 https://kilthub.cmu.edu/ndownloader/files/12095057 %K Algebra %K Boolean. %K Constraint programming (Computer science) %X Abstract: "Given a formula [Phi] in quantifier-free Presburger arithmetic, it is well known that, if there is a satisfying solution to [Phi], there is one whose size, measured in bits, is polynomially bounded in the size of [Phi]. In this paper, we consider a special class of quantifier-free Presburger formulas in which most linear constraints are separation (difference-bound) constraints, and the non-separation constraints are sparse. This class has been observed to commonly occur in software verification problems. We derive a new solution bound in terms of parameters characterizing the sparseness of linear constraints and the number of non-separation constraints, in addition to traditional measures of formula size. In particular, the number of bits needed per integer variable is linear in the number of non-separation constraints and logarithmic in the number and size of non-zero coefficients in them, but is otherwise independent of the total number of linear constraints in the formula. The derived bound can be used in a decision procedure based on instantiating integer variables over a finite domain and translating the input quantifier-free Presburger formula to an equi-satisfiable Boolean formula, which is then checked using a Boolean satisfiability solver. We present empirical evidence indicating that this method can greatly outperform other decision procedures." %I Carnegie Mellon University