The Number Decision Diagram (NDD) is a finite-state 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 [BL01], one addresses the problem of counting the number of distinct elements in a set of vectors represented as an NDD. An algorithm is described for performing an exact count without enumerating explicitly the vectors, which makes it capable of handling very large sets. As an auxiliary result, an efficient projection method is also developed, which allows to construct efficiently NDDs from quantified formulas, and thus makes it possible to apply the counting technique to sets specified by formulas. The algorithms introduced in this work have been implemented in the verification tool LASH [LAS], and applied successfully to various counting problems.