
CMUCS03210
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS03210
Deciding QuantifierFree Presburger Formulas using
Finite Instantiation based on Parameterized Solution Bounds
Sanjit A. Seshia, Randal E. Bryant
December 2003
CMUCS03210.ps
CMUCS03210.pdf
Keywords: Presburger arithmetic, Boolean satisfiability, separation
(differencebound) constraints, solution bounds, finite instantiation,
decision procedures, theorem proving
Given a formula φ in quantifierfree Presburger arithmetic,
it is well known that, if there is a satisfying solution to φ,
there is one whose size, measured in bits, is polynomially bounded
in the size of φ. In this paper, we consider a special class of
quantifierfree Presburger formulas in which most linear constraints
are separation (differencebound) constraints, and the nonseparation
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 nonseparation 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 nonseparation 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 (SAT) solver.
We present empirical evidence indicating that this method can greatly
outperform other decision procedures.
19 pages
