iRank: A Variable Order Metric for DEDS Subject to Linear Invariants

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{$}{$}{_}{ackslash}mathrm {{}Rank{}}{$}{$}, a new variable order metric that exploits the knowledge embedded in these invariants. We evaluate i{$}{$}{_}{ackslash}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.