binary - CUDD:BDD 的操作

Question

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

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

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

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

如果x2 = 0:

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

如果 x2 = 1:

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

这可能吗？

Answer 1

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

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

要完成您想做的事情，您必须组合 CUDD 提供的 bool 运算符，从而获得具有所需属性的新 bool 函数。

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

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

正如您所注意到的，新的 BDD(还)没有忘记 x 变量的值。您希望它们“不关心”w.r.t 到 x 的值。由于您已经知道 x 被限制为 s0 和 s1 中的一个特定值，您可以使用存在抽象运算符:

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

请注意，x 在这里用作所谓的立方体(见下文)。

这些现在是您想要的 BDD。

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