Symbolic Reasoning with Weighted and Normalized Decision Diagrams |
| |
Authors: | J rn Ossowski,Christel Baier |
| |
Affiliation: | Universität Bonn, Institut für Informatik I, Römerstrasse 164, 53117 Bonn, Germany |
| |
Abstract: | 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. |
| |
Keywords: | Weighted decision diagrams factored edge-valued binary decision diagrams normalized algebraic decision diagrams minimum/maximum calculation solving linear equation systems |
本文献已被 ScienceDirect 等数据库收录! |
|