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:3030m Talk | iRank: a variable order metric for DEDS subject to linear invariants TACASLink to publication | ||
| 17:0030m Talk | Edge-Specified Reduction Binary Decision Diagrams TACASLink to publication | ||
| 17:3030m Talk | Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS Jens Katelaan , Christoph Matheja RWTH Aachen University, Florian Zuleger Vienna University of TechnologyLink to publication | ||