Research Topic: Algorithms for BDDs with different variable orders
Since the size of an OBDD heavily depends on its variable order, much effort is spent on he computation of good variable orders and their improvement. When applying common optimization techniques one often has to cope with different variable orderings, e.g., in sequential analysis for representing transition relation and reachable state set, where further efficient manipulation requires a common variable order. We are developing algorithms for this task.
Technical Reports:
- Ch. Meinel, H. Sack, Chr. Stangier, A. Wagner:
Do We Really Need Common Variable Orders for Synthesizing OBDDs? - G. Cabodi, S. Quer, Ch. Meinel, H. Sack, A. Slobodová, Chr. Stangier:
Binary Decision Diagrams and the Multiple Variable Order Problem
Publications:
- Ch. Meinel, H. Sack, C. Stangier:
Overcoming Ordering Restrictions for Synthesizing Binary Decision Diagrams,
in Proc. 17th IEEE NORCHIP, Oslo (Norway), 1999.
People:
- Prof. Dr. Christoph Meinel
- Dipl. Inform. Harald Sack
- Dr. Anna Slobodova
- Dipl. Inform. Christian Stangier
- Dipl. Inform. Arno Wagner
- Dr. Gianpiero Cabodi (Torino)
- Dipl. Ing. Stefano Quer (Torino)
Projects:
- DAAD Vigoni Program
- Politecnico Torino
Activities:
- Integration of MULVAR Algorithms in the CUDD BDD Package
- Integration of MULVAR in the PDTRAV traversal package
