
VOLUME 1, ISSUE 2, PAPER 6
Deciding QuantifierFree Presburger Formulas Using Parameterized Solution Bounds

©Sanjit A Seshia, Carnegie Mellon University ©Randal E Bryant, Carnegie Mellon University 
Abstract
Given a formula in quantifierfree 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 quantifierfree Presburger formulas in which most linear constraints are
difference (separation) constraints, and the nondifference 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
nondifference 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 nondifference constraints and logarithmic
in the number and size of nonzero 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
quantifierfree Presburger formula to an equisatisfiable 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.

Publication date: December 19, 2005
Full Text: PDF  PostScript DOI: 10.2168/LMCS1(2:6)2005
Hit Counts: 11995 
Creative Commons  