## Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds

journal contribution

posted on 01.01.1990, 00:00 by Sanjit A Seshia, Randal E. BryantGiven a formula in quantifier-free Presburger arithmetic, if it has a satisfying
solution, there is one whose size, measured in bits, is polynomially bounded in the size
of the formula. In this paper, we consider a special class of quantifier-free Presburger
formulas in which most linear constraints are difference (separation) constraints, and the
non-difference constraints are sparse. This class has been observed to commonly occur in
software verification. We derive a new solution bound in terms of parameters characterizing
the sparseness of linear constraints and the number of non-difference constraints, in
addition to traditional measures of formula size. In particular, we show that the number
of bits needed per integer variable is linear in the number of non-difference 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. In addition to
our main theoretical result, we discuss several optimizations for deriving tighter bounds in
practice. Empirical evidence indicates that our decision procedure can greatly outperform
other decision procedures.