CUDD: BDDs的操作

Question

我正在使用CUDD C++接口(https://github.com/ivmai/cudd)，但是几乎没有关于这个库的任何信息。我想知道如何根据一个变量的值删除它。

例如，我现在将下一个表存储在一个bdd中

|-----|-----|-----|
|  x1 |  x2 |  y  |
|-----|-----|-----|
|  0  |  0  |  1  |
|-----|-----|-----|
|  0  |  1  |  1  |
|-----|-----|-----|
|  1  |  0  |  1  |
|-----|-----|-----|
|  1  |  1  |  0  |
|-----|-----|-----|

我希望根据bdd的值将上一个表拆分成两个单独的x2，然后删除该节点：

如果是x2 = 0

|-----|-----|
|  x1 |  y  |
|-----|-----|
|  0  |  1  |
|-----|-----|
|  1  |  1  |
|-----|-----|

如果是x2 = 1

|-----|-----|
|  x1 |  y  |
|-----|-----|
|  0  |  1  |
|-----|-----|
|  1  |  0  |
|-----|-----|

有可能吗？

Answer 1

CUDD库的C++接口上几乎没有文档，原因是它只是C函数的包装器，其中有大量的文档。

C++包装器主要用于消除所有Cudd_Ref(.)和Cudd_RecursiveDeref(.)调用使用C接口的代码将需要这样做。请注意，如果需要的话，也可以使用C++代码中的C接口。

要完成您想要做的事情，您必须将CUDD提供的布尔运算符组合起来，从而获得一个新的布尔函数和所需的属性。

第一步是将s限制为x=0和x=1情况：

BDD s0 = s & !x;
BDD s1 = s & x;

正如您注意到的，新的BDDs (尚未)忽略了x变量的值。您希望它们是“不关心”w.r.t对x的值。由于您已经知道x仅限于s0和s1中的一个特定值，所以可以使用存在抽象运算符：

s0 = s0.ExistAbstract(x);
s1 = s1.ExistAbstract(x);

请注意，x在这里用作一个所谓的多维数据集(见下文)。

这些都是你想要的BDD。

立方体解释：--如果您同时从多个变量中抽象，那么您应该先从要抽象的所有变量中计算出这样一个多维数据集。多维数据集主要用于表示一组变量。从数学逻辑来看，如果你存在或普遍地抽象出多个变量，那么抽象化这些变量的顺序就无关紧要了。由于CUDD中的递归BDD操作是在BDDs的对(或三重)上实现的，所以CUDD内部也将一组变量表示为一个多维数据集，这样存在抽象操作就可以只在(1)执行存在抽象的BDD上工作，(2) BDD表示要从其中抽象的变量集。多维数据集作为BDD的内部表示不应该与开发人员仅使用CUDD (而不是扩展CUDD)相关，只是表示变量的BDDD也可以用作多维数据集。

Answer 2

使用Cython绑定到package dd的CUDD的一种方法如下所示，它使用常量值替换变量x2。

import dd.cudd as _bdd

bdd = _bdd.BDD()
bdd.declare('x1', 'x2')
# negated conjunction of the variables x1 and x2
u = bdd.add_expr(r'~ (x1 /\ x2)')

let = dict(x2=False)
v = bdd.let(let, u)
assert v == bdd.true, v

let = dict(x2=True)
w = bdd.let(let, u)
w_ = bdd.add_expr('~ x1')
assert w == w_, (w, w_)

通过将import语句更改为import dd.autoref as _bdd，相同的代码在纯Python中运行。纯Python版本的dd可以与pip install dd一起安装。dd与dd.cudd模块的安装描述为这里。