CUDD UM

Basic Data Structures

Nodes

BDDs、ADD和ZDDs是由DdNode组成的。一个DdNode（简称node）是一个有几个字段的结构。Those that are of interest to the application that uses the CUDD package as a black box are the variable index , the reference  count, and the value. The remaining fields are pointers that connect nodes among themselves and that are used to implement the unique  table. (See Section 3.2.2.)

index字段持有标记该节点的变量名称。变量的索引是一个永久属性，反映了创建的顺序。索引0对应的是首先创建的变量。在具有32位指针的机器上，变量的最大数量是可以存储在无符号短整数中的最大值减去1。最大的索引被保留给常数节点。当使用64位指针时，变量的最大数量是可以存储在无符号整数中的最大值减去1。

当变量被重新排序以减少决策图的大小时，变量的顺序可能会发生变化，但它们会保留其索引。该软件包会跟踪变量的排列组合（以及它的逆向）。应用不受变量重新排序的影响，除了以下情况。

1、如果应用程序使用生成器（Cudd_ForeachCube和Cudd_ForeachNode）并且启用了重新排序，那么它必须注意不要调用任何可能创建新节点（从而可能触发重新排序）的操作。这是因为图表中的立方体（即路径）和节点会因为重新排序而改变。

2、如果应用程序使用Cudd_bddConstrain并重新排序，那么Cudd_bddConstrain作为一个图像限制器的属性就会丢失。

CUDD包依靠垃圾收集来回收不再使用的图所使用的内存。垃圾收集所采用的方案是基于为每个节点保留一个引用计数。被计算的引用包括内部引用（来自其他节点的引用）和外部引用（通常来自调用环境的引用）。当应用程序创建一个新的BDD、ADD或ZDD时，它必须通过调用Cudd_Ref来明确增加其引用计数。同样，当一个图不再需要时，应用程序必须调用Cudd_RecursiveDeref（对于BDD和ADD）或Cudd_RecursiveDerefZdd（对于ZDD）来 "回收 "该图的节点。

Terminal节点携带一个值。这对ADD特别重要。默认情况下，该值是一个双数。要改变成不同的东西（例如，一个整数），必须修改包并重新编译。目前对这个过程的支持是非常初级的。

The Manager

在BDDs、ADDs和ZDDs中使用的所有节点都保存在特殊的哈希表中，称为唯一表。具体来说，BDD和ADD共享同一个唯一表，而ZDD则有自己的表。顾名思义，唯一表的主要目的是保证每个节点都是唯一的；也就是说，没有其他节点被相同的变量和相同的子节点所标记。这种唯一性属性使得决策图成为典范。唯一表和一些辅助数据结构构成了DdManager（简称管理器）。尽管只使用导出函数的应用程序不需要关心管理器的大部分细节，但它必须在以下意义上与管理器打交道。应用程序必须通过调用一个适当的函数来初始化管理器。见第3.3节。）随后，它必须将一个指向管理器的指针传递给所有操作决策图的函数。

除了一些统计计数器之外，CUDD包中没有全局变量。因此，在同一个应用程序中，很可能有多个管理器同时活动。

Cache

决策图的高效递归操作需要使用一个表来存储计算结果。这个表在这里被称为缓存，因为它被有效地处理成一个容量可变但有限的缓存。CUDD软件包默认从一个小的缓存开始，然后增加它的大小，直到没有进一步的好处，或者达到一个极限大小。用户可以通过选择缓存大小的初始值和极限值来影响这一政策。

Initializing and Shutting Down a DdManager

要使用CUDD包中的函数，首先要通过调用Cudd_Init来初始化该包本身。这个函数需要四个参数。

1、numVars : 它是BDDs和ADD的初始变量数。如果应用程序所需的变量总数是已知的，那么用该数量的变量创建一个管理器的效率会略高。如果这个数字是未知的，可以将其设置为0，或者设置为变量数量的任何其他下限。请求比实际需要更多的变量并不是不正确的，但是效率不高。

2、numVarsZ : 它是ZDDs的初始变量数。关于该参数值的讨论，见第3.9节和第3.11节。

3、numSlots : 确定唯一表的每个子表的初始大小。每个变量都有一个子表。每个子表的大小是动态调整的，以反映节点的数量。通常情况下，使用这个参数的默认值就可以了，即CUDD_UNIQUE_SLOTS。

4、cacheSize : 它是缓冲区的初始大小（条目数）。它的默认值是CUDD_CACHE_SLOTS。

5、maxMemory : 它是最大内存占用的目标值（单位：字节）。该软件包使用这个值来决定两个参数（1、缓存将增长到的最大尺寸，与命中率或唯一表的尺寸无关。2、唯一表的增长将优先于垃圾收集的最大尺寸。）如果maxMemory被设置为0，CUDD会尝试根据可用的内存来猜测一个好的值。

A typical call to Cudd_Init  may look like this:

  manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);

要收回与管理器相关的所有内存，应用程序必须调用Cudd_Quit 。这通常是在退出前完成的。

Setting Parameters

该软件包提供了几个函数来设置控制各种功能的参数。例如，该包有一种自动的方法来确定一个更大的唯一表是否会使应用程序运行得更快。在这种情况下，软件包会进入一个 "快速增长 "模式，在这个模式下，唯一子表的大小调整比垃圾回收更受青睐。然而，当唯一表达到一个给定的大小时，包会返回到正常的 "慢速增长 "模式，尽管导致过渡到快速增长的条件仍然存在。快速增长的极限大小可以通过Cudd_ReadLooseUpTo读取，并通过Cudd_SetLooseUpTo改变。其他几个参数也有类似的函数对。也见第4.8节。

Constant Functions

CUDD包定义了几个常量函数。这些函数在管理器初始化时被创建，并且可以通过管理器本身访问。

One, Logic Zero, and Arithmetic Zero

常数1（由Cudd_ReadOne返回）对BDDs、ADDs和ZDDs是通用的。然而，它对ADD和BDDs以及ZDDs的意义是不同的。由常数1节点组成的图仅代表ADD和BDDs的常数1功能。对于ZDDs，其含义取决于变量的数量。它是所有变量的补数的结合。反之，常数1函数的表示取决于变量的数量。Cudd_ReadZddOne返回n个变量的常数1函数。

常数0在ADD和ZDD中是通用的，但在BDD中不通用。BDD逻辑0与常数0的功能没有关系。它是通过常数1的补码（Cudd_Not）获得的。(它也由Cudd_ReadLogicZero返回。)所有其他常数都是针对ADD的。

Predefined Constants

除了0（由Cudd_ReadZero返回）和1，在初始化时还会创建以下常量函数。

1、PlusInfinity和MinusInfinity：在执行IEEE754浮点运算标准的计算机上，这两个常数被设置为有符号的无穷数。

2、Epsilon : 这个常数，最初设置为10^-12，用于比较浮点数值是否相等。

Background

背景值是一个常数，通常用来表示图中不存在的弧。考虑一个最短路径问题。两个没有电弧连接的节点可以被视为由一条无限长的电弧连接。因此，在最短路径问题中，将背景值设置为PlusInfinity是很方便的。另一方面，在网络流问题中，两个没有被弧连接的节点可以被视为由一条容量为0的弧连接。因此，对于这些问题，将背景值设为0更为方便。 一般来说，在表示稀疏矩阵时，背景值是隐含的假设值。

初始化时，背景值被设置为0，可以用Cudd_ReadBackground读取，用Cudd_SetBackground修改。背景值影响读取稀疏矩阵/图形的程序（Cudd_addRead和Cudd_addHarwell），打印出ADD的乘积之和表达式的程序（Cudd_PrintMinterm），立方体的生成器（Cudd_ForeachCube），以及计算最小值的程序（Cudd_CountMinterm）。

New Constants

新的常数可以通过调用Cudd_addConst创建。这个函数将检索所需常量的ADD，如果它已经存在，或者它将创建一个新的。显然，新的常数只应在操作ADD时使用。

Creating Variables

决策图通常是由较简单的决策图组合而成的。当然，最简单的决策图不能以这种方式创建。在第3.5节中已经讨论了常数函数。在这一节中，我们讨论简单的变量函数，也被称为投影函数。

New BDD and ADD Variables

BDDs和ADDs的投影函数是不同的。BDDs的投影函数由一个内部节点组成，其两个出场弧都指向常数1。其他的弧是补足的。

另一方面，一个ADD投影函数，其else指针指向算术零函数。我们不应该把这两种类型的变量混在一起。在操作BDD时应使用BDD变量，而在操作ADD时应使用ADD变量。我们提供了三个函数来创建BDD变量。

1、Cudd_bddIthVar : 返回索引为i的投影函数，如果该函数不存在，将被创建。

2、Cudd_bddNewVar : 返回一个新的投影函数，其索引是调用时正在使用的最大索引，加上1。

3、Cudd_bddNewVarAtLevel : 与Cudd_bddNewVar类似。此外，它还允许指定新变量插入变量顺序中的位置。相比之下，Cudd_bddNewVar在顺序的最后加入新变量。

类似的函数有Cudd_addIthVar , Cudd_addNewVar , 和Cudd_addNewVarAtLevel。

New ZDD Variables

与BDDs和ADDs的投影函数不同，ZDDs的投影函数有n+1个节点的图，其中n是变量的数量。因此，当增加新的变量时，投影函数的ZDDs会发生变化。这将在第3.9节讨论。这里我们假设变量的数量是固定的。第i个投影函数的ZDD由Cudd_zddIthVar返回。

Basic BDD Manipulation

BDDs的常见操作可以通过调用Cudd_bddIte来完成。该函数以三个BDDs，f、g和h为参数，计算出f*g + f‘*h。与所有创建新的BDDs或ADD的函数一样，Cudd_bddIte返回的结果必须由调用者明确引用。Cudd_bddIte可以用来实现所有双参数布尔函数。然而，该包还提供了Cudd_bddAnd以及其他双操作数布尔函数，当调用双操作数函数时，其效率略高。下面的代码片段说明了如何为函数f = x0'x1'x2'x3'建立BDD。

        DdManager *manager;
        DdNode *f, *var, *tmp;
        int i;

        ...

        f = Cudd_ReadOne(manager);
        Cudd_Ref(f);
        for (i = 3; i >= 0; i--) {
            var = Cudd_bddIthVar(manager,i);
            tmp = Cudd_bddAnd(manager,Cudd_Not(var),f);
            Cudd_Ref(tmp);
            Cudd_RecursiveDeref(manager,f);
            f = tmp;
        }

这个例子说明了以下几点。

1、中间的结果必须是 "引用 "和 "去引用"。然而，var是一个投影函数，它的引用计数总是大于0，因此，没有调用Cudd_Ref 。

2、新的f必须分配给一个临时变量（本例中为tmp）。如果Cudd_bddAnd的结果直接分配给f，旧的f就会丢失，而且没有办法释放其节点。

3、语句f = tmp的效果与以下相同。

f = tmp;
Cudd_Ref(f)。
Cudd_RecursiveDeref(manager,tmp)。

4、通常情况下，"自下而上 "地构建BDD是更有效的。这就是为什么循环从3到0的原因。然而，请注意，在变量重新排序后，更高的索引并不一定意味着 "更接近底部"。当然，在这个简单的例子中，效率并不是一个问题。

5、如果我们想在重新排序后仍以自下而上的方式连接这些变量，我们应该使用Cudd_ReadInvPerm。不过，我们必须小心，在进入循环之前要固定连接的顺序。否则，如果发生重排，就有可能两次使用一个变量而跳过另一个变量。

标签：UM,函数,Cudd,CUDD,BDDs,ADD,节点,变量
来源： https://www.cnblogs.com/zhangzhangtabszj/p/14912703.html