CUDD：将变量转换为输出

Question

我正在使用 CUDD C++，我想知道是否可以执行以下操作：

目前，我将下一个 table 存储在 bdd:

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

如果原始输出的值为 1，是否可以创建另一个具有 2 个输出的 table，提取 x2、x3 的值？:

期望的输出：

|-----||-----|-----|
|  x1 ||  x2 |  x3 |
|-----||-----|-----|
|  0  ||  1  |  0  |
|-----||-----|-----|
|  1  ||  0  |  1  |
|-----||-----|-----|

我已经尝试使用 ExistAbastract() 命令并获得了 2 个 bdds 和正确的数据，但 x2 和 x3 仍然是输入。是否可以根据y的值将x2和x3从变量转换为输出？

Answer 1

您的第一个 table 是一个值 table，它为 x1、x2、x3 的每个组合定义了 y 的值，因此可以表示为变量 x1 的 BDD ,x2,x3.

您想要的输出 table 只有双线左侧的 y1。因此，您需要两个 BDD x2 和 x3，其范围仅超过 x1 的值。

请注意，如果对于 x1 的某个值，存在 x2、x3 的多种组合使得 y(x1,x2,x3)=True，则您的问题是不明确的。但如果情况并非如此，这里有一个有效的解决方案。

让我们只考虑您想要 x2 的函数的情况（其他情况类似）。你存在抽象 x3 并得到：

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

不错的开始。现在你想要的最终函数是 y 为真的行中 x2 的值。让我们分解一下：

对于 x1 的所有值，如果最终函数的输出为真，则 y(x1,true) 为真
对于 x1 的所有值，如果最终函数的输出为假，则 y1(x1,false) 为真。

我们可以将第一个案例构建为：

(y & x2).ExistAbstract(x2)

这个表达式已经足够了，因为这个表达式是一个函数，无论如何对于所有其他输入值 returns FALSE。

CUDD：将变量转换为输出

CUDD: Converting variables to outputs

binary

binary-decision-diagram

cudd