Counting Solutions to Presburger Formulas: How and Why
Counting Solutions to Presburger Formulas: How and Why
Files
Publication or External Link
Date
1998-10-15
Authors
Pugh, William
Advisor
Citation
DRUM DOI
Abstract
We describe methods that are able to count the number of integer
solutions to selected free variables of a Presburger formula, or sum a
polynomial over all integer solutions of selected free variables of a
Presburger formula. This answer is given symbolically, in terms of
symbolic constants (the remaining free variables in the Presburger
formula).
For example, we can create a Presburger formula who's solutions correspond
to the iterations of a loop. By counting these, we obtain an estimate
of the execution time of the loop.
In more complicated applications, we can create Presburger formulas
who's solutions correspond to the distinct memory locations or cache lines
touched by a loop, the flops executed by a loop, or the array elements
that need to be communicated at a particular point in a distributed
computation. By counting the number of solutions, we can evaluate the
computation/memory balance of a computation, determine if a loop is
load balanced and evaluate message traffic and allocate message buffers.
(Also cross-referenced as UMIACS-TR-94-27)