Binary Decision Diagrams and the Multiple Variable Order Problem
Binary Decision Diagrams and the Multiple Variable Order Problem
复制标题
二元决策图和多变量阶问题
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
Christian Stangier
中科院分区：
文献类型：
--
作者：
G. Cabodi;S. Quer;C. Meinel;Harald Sack;A. Slobodová;Christian Stangier
有序二叉决策图（OBDDs）是CAD中处理和表示布尔函数的首选。由于OBDD的大小在很大程度上取决于所选择的变量顺序，所以在寻找和改进现有变量顺序方面花费了很多精力。如果在OBDD应用中使用这些优化技术，则必须经常科普不同变量阶数的OBDD（例如，表示顺序验证中的转换关系和可达状态集）。为了将OBDD有效地操作和表示为多根OBDD，需要公共变量顺序。在本文中，我们提出了解决多变量阶问题的方法，即，我们提出了启发式方法，根据所涉及的OBDD的原始变量顺序计算非常合适的中间变量顺序
Ordered Binary Decision Diagrams (OBDDs) are the first choice in manipulating and representing Boolean functions in CAD. Since the size of an OBDD heavily depends on the chosen variable order, much effort is spent in finding good and improving existing variable orders. If these optimizing techniques are used in OBDD applications, one has to cope with OBDDs of different variable orders very often (e.g., representing the transition relation and the reachable state set in sequential verification). For an efficient manipulation and represention of OBDDs as a multi rooted OBDD, a common variable order is desired. In this paper we present approaches for the solution of the multiple variable order problem, i.e., we present heuristics that compute a well suited intermediate variable order based on the original variable orders of the involved OBDDs