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.
This work was partially funded by a grant of the “Communauté française de Belgique — Direction de la recherche scientifique
— Actions de recherche concertées”, and by the European Commission (FET project ADVANCE, contract No IST-1999-29082).