Counting the Solutions of Presburger Equations without Enumerating Them

The Number Decision Diagram (NDD) has recently been proposed
as a powerful representation system for sets of integer vectors. In
particular, NDDs can be used for representing the sets of solutions of
arbitrary Presburger formulas, or the set of reachable states of some
systems using unbounded integer variables. In this paper, we address
the problem of counting the number of distinct elements in a set of
vectors represented as an NDD. We give an algorithm that is able to
perform an exact count without enumerating explicitly the vectors,
which makes it capable of handling very large sets. As an auxiliary
result, we also develop an efficient projection method that allows to
construct efficiently NDDs from quantified formulas, and thus makes it
possible to apply our counting technique to sets specified by
formulas. Our algorithms have been implemented in the verification
tool LASH, and applied successfully to various counting problems.