Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Model Checking

TL;DR

This paper explores how bandwidth and wavefront reduction algorithms can improve static variable ordering in symbolic model checking, leading to more efficient event locality and resource usage.

Contribution

It demonstrates the applicability of bandwidth and wavefront reduction techniques to static variable ordering, including handling asymmetric matrices with the Sloan algorithm.

Findings

Bandwidth reduction algorithms improve variable ordering quality.

The Sloan algorithm on the total graph yields optimal variable orders.

Standard sparse matrix operations can compute good variable orders in milliseconds.

Abstract

We demonstrate the applicability of bandwidth and wavefront reduction algorithms to static variable ordering. In symbolic model checking event locality plays a major role in time and memory usage. For example, in Petri nets event locality can be captured by dependency matrices, where nonzero entries indicate whether a transition modifies a place. The quality of event locality has been expressed as a metric called (weighted) event span. The bandwidth of a matrix is a metric indicating the distance of nonzero elements to the diagonal. Wavefront is a metric indicating the degree of nonzeros on one end of the diagonal of the matrix. Bandwidth and wavefront are well studied metrics used in sparse matrix solvers. In this work we prove that span is limited by twice the bandwidth of a matrix. This observation makes bandwidth reduction algorithms useful for obtaining good variable orders. One major issue we address is that the reduction algorithms can only be applied on symmetric matrices, while the dependency matrices are asymmetric. We show that the Sloan algorithm executed on the total graph of the adjacency graph gives the best variable orders. Practically, we demonstrate that our work allows to call standard sparse matrix operations in Boost and ViennaCL, computing very good static variable orders in milliseconds. Future work is promising, because a whole new spectrum of more off-the-shelf algorithms, including metaheuristic ones, become available for variable ordering.