DSM-based variable ordering heuristic for reduced computational effort of symbolic supervisor synthesis

We consider the influence that the variable order of Binary Decision Diagrams (BDDs) has on the computational effort that is required for symbolic supervisor synthesis. In recent research it has been shown that improving the variable order can result in a substantial decrease of synthesis effort. We propose the combined use of the Dependency Structure Matrices (DSMs) and the matrix reordering heuristics Cuthill-McKee and Sloan to minimize the Weighted Event Span (WES) of the variable order. This is done by placing variables that often appear together in transition relations near each other. By performing benchmark experiments, we measure the reduction in synthesis effort by utilizing a variable order with minimized WES. The experiments show that our approach is competitive in reducing computational effort compared to FORCE, a state of practice variable ordering heuristic. Moreover, the best improvements in effort reduction are shown for the most computationally demanding models tested.