Application driven variable reordering and an example implementation in reachability analysis

Variable reordering is the main approach to minimize the size of Ordered Binary Decision Diagrams. But despite the huge effort spent, up to now, to design different reordering heuristics, their performance often does not meet the needs of the applications. In many OBDD-based computations, the time cost for reordering dominates the time spent by the computation itself. There are some known approaches for accelerating the reordering by taking advantage of structural properties of OBDDs and functions represented. In this paper, we propose a reordering method that exploits application specific information. The main idea is to drive the reordering process by the computation. This effects an acceleration of the whole computation rather than of the reordering only. The power of the approach is illustrated by speeding up forward traversal of finite state machines