Symbolic Reasoning with Weighted and Normalized Decision Diagrams

Jörn OssowskiJörn Ossowski, Christel BaierChristel Baier

DOI Link

Jörn Ossowski, Christel Baier
Symbolic Reasoning with Weighted and Normalized Decision Diagrams
Proc. of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS), volume 151 of Electronic Notes in Theoretical Computer Science, 39--56, 2006. Elsevier

Details
Bibtex

KurzfassungAbstract
Several variants of Bryant's ordered binary decision diagrams have been suggested in the literature to reason about discrete functions. In this paper, we introduce a generic notion of weighted decision diagrams that captures many of them and present criteria for canonicity. As a special instance of such weighted diagrams, we introduce a new BDD-variant for real-valued functions, called normalized algebraic decision diagrams. Regarding the number of nodes and arithmetic operations like addition and multiplication, these normalized diagrams are as efficient as factored edge-valued binary decision diagrams, while several other operators, like the calculation of extrema, minimum or maximum of two functions or the switch from real-valued functions to boolean functions through a given threshold, are more efficient for normalized diagrams than for their factored counterpart.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{OB2006,
  author    = {J{\"{o}}rn Ossowski and Christel Baier},
  title     = {Symbolic Reasoning with Weighted and Normalized Decision Diagrams},
  booktitle = {Proc. of the 12th Symposium on the Integration of Symbolic
               Computation and Mechanized Reasoning (CALCULEMUS)},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {151},
  publisher = {Elsevier},
  year      = {2006},
  pages     = {39--56},
  doi       = {10.1016/J.ENTCS.2005.11.022}
}