CUDD

The CUDD package provides functions to manipulate Binary Decision Diagrams (BDDs) [5,3], Algebraic Decision Diagrams (ADDs) [1], and Zero-suppressed Binary Decision Diagrams (ZDDs) [12]. BDDs are used to represent switching functions; ADDs are used to represent function from to an arbitrary set. ZDDs represent switching functions like BDDs; however, they are much more efficient than BDDs when the functions to be represented are characteristic functions of cube sets, or in general, when the ON-set of the function to be represented is very sparse. They are inferior to BDDs in other cases. The package provides a large set of operations on BDDs, ADDs, and ZDDs, functions to convert BDDs into ADDs or ZDDs and vice versa, and a large assortment of variable reordering methods.


References in zbMATH (referenced in 148 articles )

Showing results 101 to 120 of 148.
Sorted by year (citations)
  1. Pan, Guoqiang; Sattler, Ulrike; Vardi, Moshe Y.: BDD-based decision procedures for the modal logic \textbfK (2006)
  2. Sinz, Carsten; Küchlin, Wolfgang; Feichtinger, Dieter; Görtler, Georg: Checking consistency and completeness of on-line product manuals (2006) ioport
  3. Thiebaux, S.; Gretton, C.; Slaney, J.; Price, D.; Kabanza, F.: Decision-theoretic planning with non-Markovian rewards (2006)
  4. Wimmer, Ralf; Herbstritt, Marc; Hermanns, Holger; Strampp, Kelley; Becker, Bernd: SIGREF -- a symbolic bisimulation tool box (2006)
  5. De Wulf, Martin; Doyen, Laurent; Raskin, Jean-François: Almost ASAP semantics: from timed models to timed implementations (2005)
  6. Harding, Aidan; Ryan, Mark; Schobbens, Pierre-Yves: A new algorithm for strategy synthesis in LTL games (2005)
  7. Huang, Jinbo; Darwiche, Adnan: Using DPLL for efficient OBDD construction (2005)
  8. Jin, HoonSang; Somenzi, Fabio: CirCUs: A hybrid satisfiability solver (2005)
  9. Pan, Guoqiang; Vardi, Moshe Y.: Symbolic techniques in satisfiability solving (2005)
  10. Pastor, Enric; Peña, Marco A.; Solé, Marc: TRANSYT: A tool for the verification of asynchronous concurrent systems (2005)
  11. Viamontes, G. F.; Markov, I. L.; Hayes, J. P.: Graph-based simulation of quantum computation in the density matrix representation (2005)
  12. Wang, Fuzhi; Kwiatkowska, Marta: An MTBDD-based implementation of forward reachability for probabilistic timed automata (2005)
  13. Cimatti, A.; Roveri, M.; Bertoli, P.: Conformant planning via symbolic model checking and heuristic search (2004)
  14. Dovier, Agostino; Piazza, Carla; Policriti, Alberto: An efficient algorithm for computing bisimulation equivalence (2004)
  15. Gröpl, Clemens; Prömel, Hans Jürgen; Srivastav, Anand: Ordered binary decision diagrams and the Shannon effect (2004)
  16. Horiyama, Takashi; Ibaraki, Toshihide: Reasoning with ordered binary decision diagrams (2004)
  17. Khurshid, Sarfraz; Marinov, Darko; Shlyakhter, Ilya; Jackson, Daniel: A case for efficient solution enumeration (2004)
  18. Kwiatkowska, Marta; Norman, Gethin; Parker, David: Probabilistic symbolic model checking with prism: a hybrid approach (2004) ioport
  19. Wegener, Ingo: BDDs -- design, analysis, complexity, and applications. (2004)
  20. Cimatti, A.; Pistore, M.; Roveri, M.; Traverso, P.: Weak, strong, and strong cyclic planning via symbolic model checking (2003)

Further publications can be found at: http://vlsi.colorado.edu/~fabio/CUDD/node7.html