• de

Algorithms for BDDs with different variable orders

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


  • Ch. Meinel, H. Sack, C. Stangier:
    Overcoming Ordering Restrictions for Synthesizing Binary Decision Diagrams,
    in Proc. 17th IEEE NORCHIP, Oslo (Norway), 1999.



  • DAAD Vigoni  Program
  • Politecnico Torino


  • Integration of MULVAR Algorithms in the CUDD BDD Package
  • Integration of MULVAR in the PDTRAV  traversal package