2006 | OriginalPaper | Buchkapitel
Computing Affine Hulls over and from Sets Represented by Number Decision Diagrams
verfasst von : Louis Latour
Erschienen in: Implementation and Application of Automata
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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}$
or over
${\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
${\mathcal O}(|{\mathcal Q}| \cdot |{\Sigma_r^n}| \cdot n )$
and
${\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 Σ
$_{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.