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 iRank, a new variable order metric that exploits the knowledge embedded in these invariants. We evaluate iRank 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.
Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:30 - 18:00 | |||
16:30 30mTalk | iRank: a variable order metric for DEDS subject to linear invariants TACAS Link to publication | ||
17:00 30mTalk | Edge-Specified Reduction Binary Decision Diagrams TACAS Link to publication | ||
17:30 30mTalk | Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS Jens Katelaan , Christoph Matheja RWTH Aachen University, Florian Zuleger Vienna University of Technology Link to publication |