Semiring Labelled Decision Diagrams, Revisited: Canonicity and Spatial Efficiency Issues

International audienceExisting languages in the valued decision diagrams (VDDs) family, including ADD, AADD, and those of the SLDD family, prove to be valuable target languages for compiling multivariate functions. However, their efficiency is directly related to the size of the compiled formulae. In practice, the existence of canonical forms may have a major impact on the size of the compiled VDDs. While efficient normalization procedures have been pointed out for ADD and AADD the canonicity issue for SLDD formulae has not been addressed so far. In this paper, the SLDD family is revisited. We modify the algebraic requirements imposed on the valuation structure so as to ensure tractable conditioning, optimization and normalization for some languages of the revisited SLDD family. We show that AADD is captured by this family. Finally, we compare the spatial efficiency of some languages of this family, from both the theoretical side and the practical side