i _\mathrm Rank : A Variable Order Metric for DEDS Subject to Linear Invariants

Abstract

Finding good variable orders for decision diagrams is essential for their effective use. We consider Multiway Decision Diagrams (MDDs) encoding a set of fixed-size vectors satisfying a set of linear invariants. Two critical applications of this problem are encoding the state space of a discrete-event discrete state system (DEDS) and encoding all solutions to a set of integer constraints. After studying the relations between the MDD structure and the constraints imposed by the linear invariants, we define i $$_\mathrm {Rank}$$ , a new variable order metric that exploits the knowledge embedded in these invariants. We evaluate i $$_\mathrm {Rank}$$ against other previously proposed metrics on a benchmark of 40 different DEDS and show that it is a better predictor of the MDD size and it is better at driving heuristics for the generation of good variable orders.