2

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

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

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

我想bdd根据 x2 的值将前一个表拆分为两个单独的 s ，然后删除该节点：

如果x2 = 0：

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

如果x2 = 1：

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

可能吗？

4

2 回答 2

4

几乎没有关于 CUDD 库的 C++ 接口的文档的原因是它只是 C 函数的包装器，对此有大量文档。

C++ 包装器主要用于摆脱使用 C 接口的代码需要执行的所有 Cudd_Ref(...) 和 Cudd_RecursiveDeref(...) 调用。请注意，如果需要，您也可以使用 C++ 代码中的 C 接口。

要执行您想要执行的操作，您必须组合 CUDD 提供的布尔运算符，以获取具有所需属性的新布尔函数。

第一步是限制s到 x=0 和 x=1 的情况：

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

正如您所注意到的，新的 BDD 并没有（还）忘记 x 变量的值。您希望它们对 x 的值“不在乎”。由于您已经知道 x 被限制为 s0 和 s1 中的一个特定值，因此您可以使用存在抽象运算符：

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

请注意，x这里用作所谓的立方体（见下文）。

这些现在是您想要的 BDD。

立方体说明：如果你同时从多个变量中抽象出来，你应该首先从所有要抽象的变量中计算出这样一个立方体。立方体主要用于表示一组变量。从数学逻辑可知，如果您从存在性或普遍意义上抽象出多个变量，那么抽象出这些变量的顺序并不重要。由于 CUDD 中的递归 BDD 操作尽可能在成对（或三元组）的 BDD 上实现，因此 CUDD 在内部也将一组变量表示为一个多维数据集，因此存在抽象操作可以只在 (1)将执行存在抽象，以及 (2) 表示要从中抽象的变量集的 BDD。

于 2019-03-20T12:22:27.757 回答
0

以下是使用 Cython 绑定到 Python 包的 CUDD 的方法dd，它使用常量值替换变量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 版本dd可以使用pip install dd. 此处描述dd了使用模块的安装。dd.cudd

于 2020-02-23T14:36:53.783 回答