Asymptotically Optimal Bounds for OBDDs and the Solution of Some Basic OBDD Problems
Asymptotically Optimal Bounds for OBDDs and the Solution of Some Basic OBDD Problems
复制标题
OBDD 的渐近最优界以及一些基本 OBDD 问题的解决
DOI：
10.1006/jcss.2000.1733
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
I. Wegener
中科院分区：
文献类型：
--
作者：
Beate Bollig;I. Wegener
有序二元决策图 (OBDD) 是当今最常见的动态数据结构或布尔函数的表示类型。许多应用领域包括验证、模型检查和计算机辅助设计。对于许多函数来说，估计 OBDD 大小很容易，但渐近最优边界仅在简单情况下才知道。本文提出了证明渐进最优界的方法，并将其应用于解决有关 OBDD 的一些基本问题。确定了 π-OBDD 合成步骤随后进行最佳重新排序的最大尺寸增加，以及确定性有限自动机和准简化 OBDD 的尺寸与 OBDD 尺寸相比的最大比率。此外，还研究了具有给定数量的 1 输入的函数的最坏情况 OBDD 大小。
Ordered binary decision diagrams (OBDDs) are nowadays the most common dynamic data structure or representation type for Boolean functions. Among the many areas of application are verification, model checking, and computer aided design. For many functions it is easy to estimate the OBDD size but asymptotically optimal bounds are only known in simple situations. In this paper, methods for proving asymptotically optimal bounds are presented and applied to the solution of some basic problems concerning OBDDs. The largest size increase by a synthesis step of π-OBDDs followed by an optimal reordering is determined as well as the largest ratio of the size of deterministic finite automata and quasi-reduced OBDDs compared to the size of OBDDs. Moreover, the worst case OBDD size of functions with a given number of 1-inputs is investigated.