Research Topic: Accelerating the Variable Reordering Process

The only way to decrease the size of BDDs is by finding better variable orders. The most powerful method is dynamic reordering during the construction of the BDD. Unfortunately common reordering strategies are sometimes too time consuming.

We have introduced different techniques for accelerating the process of variable reordering. These techniques utitlize either structural or semantical information from the given BDDs. These techniques have been applied to different tasks like combinatorical verification, reachability analysis and symbolic model checking.

Technical Reports:

• Ch. Meinel, A. Slobodová:

Accelerating OBDD-Minimization by Means of Structural and Semantical Properties
• Ch. Meinel, K. Schwettmann, A. Slobodová:

Application Driven Variable Reordering and an Example in Reachability Analysis
• Ch. Meinel, Chr. Stangier:

Increasing Efficiency of Symbolic Model Checking by Accelerating Dynamic Variable Reordering
• Ch. Meinel, A. Slobodová, P. Willems:

Block-Restricted Reordering - Extended Experiments -
• Ch. Meinel, A. Slobodová:

Speeding up Variable Reordering of OBDDs

Publications:

• Ch. Meinel, C. Stangier:

Speeding Up Symbolic Model Checking by Accelerating Dynamic Variable Reordering, in Proc. of 10th GLS-VLSI, Chicago,USA, 2000.
• Ch. Meinel, K. Schwettmann, A. Slobodová :

Application Driven Variable Reordering and an Example Implementation in Reachability Analysis ASP-DAC'99, Hongkong, 1999, pp. 327-330
• Ch. Meinel, Ch. Stangier:

Speeding Up Symbolic Model Checking, 5th International Conference on Advanced Computer Systems (ACS'98), Szczecin, Polen, 1998.
• Ch. Meinel, A. Slobodová:

Sample Method for Minimization of OBDDs SOFSEM'98 , Jasna (Slowakia), 1998.
• Ch. Meinel, A. Slobodová:

Sample Method for Minimization of OBDDs IWLS'98, Granlibakken Resort, Lake Tahoe (Kalifornien, USA), 1998, pp. 311 - 316
• Ch. Meinel, A. Slobodová:

Speeding up Variable Ordering of OBDDs Proc.of IEEE ICCD'97, Austin (Texas, USA), 1997, pp. 338-343.
• Ch. Meinel, A. Slobodová:

Speeding up Variable Reordering of OBDDs, IWLS, Granlibakken Resort, Lake Tahoe (USA), 1997.

People:

• Prof. Dr. Christoph Meinel
• Dipl. Inform. Christian Stangier
• Dipl. Inform. Arno Wagner
• Dipl. Inform. Klaus Schwettmann
• Dr. Anna Slobodova (now: Compaq, Boston)

Activities:

• OHO :  OBDD Heuristics Online