Paper Info
Title
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
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.
Year
DOI
Venue
2005
10.2168/LMCS-1(2:6)2005
LICS '04 Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science
Keywords
DocType
Volume
linear constraint,decision procedure,total number,boolean satis- fiability,input quantifier-free presburger formula,carnegie mellon university.,parameterized solution bounds,decision procedures,equi-satisfiable boolean formula,quantifier-free presburger formula,integer linear programming,non-separation constraint,integer variable,presburger arithmetic,formula size,quantifier-free presburger arithmetic,quantifier-free presburger,difference separation constraints. this work was done while the first author was at the school of computer science,finite instantiation,satisfiability,software verification,empirical evidence,electronics packaging,boolean functions,computability,decidability,encoding,bismuth,logic,computational complexity,cost accounting,arithmetic,boolean satisfiability,computer science,polynomials,hardware
Journal
abs/cs/0508044
Issue
ISSN
ISBN
2
1043-6871
0-7695-2192-4
Citations 
PageRank 
References 
30
2.00
23
Authors
2
Name
Order
Citations
PageRank
Sanjit A. Seshia12226168.09
Randal E. Bryant292041194.64