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.

• G. Cabodi, S. Quer, Ch. Meinel, H. Sack, A. Slobodová, Chr. Stangier: 
  Binary Decision Diagrams and the Multiple Variable Order Problem 
  IWLS'98 (Poster)

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