|
Published Articles >> Table of Contents >> Abstract
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)
pp. 100-109
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
Sanjit A. Seshia, Carnegie Mellon University, Pittsburgh, PA
Randal E. Bryant, Carnegie Mellon University, Pittsburgh, PA
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2004.1319604
Send link to a friend
| Abstract |
|
Given a formula Φ in quantifier-free 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 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.
|
 Additional Information
|
Citation:
Sanjit A. Seshia, Randal E. Bryant,
"Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds,"
lics,
pp. 100-109,
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04),
2004
|
|
