Computing affine hulls over ℚ and ℤ from sets represented by number decision diagrams

Abstract

Number Decision Diagrams (NDD) are finite automata representing sets of integer vectors and have recently been proposed as an efficient data structure for representing sets definable in Presburger arithmetic. In this context, some work has been done in order to generate formulas or sets of generators from the NDDs. Taking another step in this direction, this paper present algorithms that takes as input an NDD and computes the affine hull over ℚ or over ℤ of the set represented by the NDD, i.e., the smallest set defined by a conjunction of equations or by a conjunction of equations and congruence relations that includes the set represented by the NDD. Our algorithms run in time Ο(|Q|·|Σrn|·n) and Ο(|Q|3·|Σrn|·n 3) respectively, where n is the number of components of the vectors represented by the NDD, and |Q| and Σrn are the number of states and the alphabet of the NDD. On a prototype implementation, the computations of affine hulls of NDDs with more than 100000 states are done in seconds. © Springer-Verlag Berlin Heidelberg 2006.