Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis

摘要

We investigate the use of bandwidth and wavefront reduction algorithms to determine a static BDD variable ordering. The aim is to reduce the size of BDDs arising in symbolic reachability. Previous work showed that minimizing the (weighted) event span of the variable dependency graph yields small BDDs. The bandwidth and wavefront of symmetric matrices are well studied metrics, used in sparse matrix solvers, and many bandwidth and wavefront reduction algorithms are readily available in libraries like Boost and ViennaCL. In this paper, we transform the dependency matrix to a symmetric matrix and apply various bandwidth and wavefront reduction algorithms, measuring their influence on the (weighted) event span. We show that Sloan's algorithm, executed on the total graph of the dependency matrix, yields a variable order with minimal event span. We demonstrate this on a large benchmark of Petri nets, DVE, PROMELA, B, and mCRL2 models. As a result, good static variable orders can now be determined in milliseconds by using standard sparse matrix solvers.