Lecture Notes in Computer Science, 2006, Volume 3845/2006, 213-224, DOI: 10.1007/11605157_18

Computing Affine Hulls over \mathbb Q{\mathbb Q} and \mathbb Z{\mathbb Z} from Sets Represented by Number Decision Diagrams

Louis Latour

View Related Documents

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 \mathbb Q{\mathbb Q} or over \mathbb Z{\mathbb Z} 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 O(|Q| ·|Srn| ·n ){\mathcal O}(|{\mathcal Q}| \cdot |{\Sigma_r^n}| \cdot n ) and O(|Q3| ·|Srn| ·n3 ){\mathcal O}(|{\mathcal Q}^3| \cdot |{\Sigma_r^n}| \cdot {n^3} ) respectively, where n is the number of components of the vectors represented by the NDD, and |Q| and Σrn_{r}^{n} 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.

Fulltext Preview

Image of the first page of the fulltext document