标签: cudd

将{<1,2>,<1,3>,<1,7>,<0,4>}视为关系R的元组集合.现在考虑R(通过其隶属函数)表示为BDD.也就是说,表示R的BDD取决于变量{x1,x2,y1,y2,y3},其中{x1,x2}用于表示每个元组的第一个元素,{y1,y2,y3}用于表示第二个要素.

现在,考虑在第一个元素中查找具有唯一值的元组集的问题.对于上面的关系,该集合将是{<0,4>}.所有其他元素都被丢弃,因为它们是第一个组件中具有1的多个值.

作为第二个例子,考虑与元组{<1,2>,<1,3>,<1,7>,<2,3>,<2,5>,<0,4>}的关系.在这种情况下,预期结果仍为{<0,4>},因为2作为第一个元素出现不止一次.

该问题还可以被视为抽象出变量{y1,y2,y3},使得仅保留{x1,x2}的唯一值.利用该结果,可以通过计算所得BDD与输入BDD的结合来重建预期关系.

总之,问题是:哪些是必须在R的表示上执行的BDD操作,以获得仅具有唯一元组的BDD.

请注意,这是此问题的一般化

编辑1: 以下代码反映了我到目前为止的实现.但是,我想知道是否有可能获得更高效的版本.为简单起见,我故意省略了计算表的处理(这对于获得更好的时间复杂度至关重要).另外,我使用&,| 而且!表示对BDD的连接,分离和补充操作.

BDD uniqueAbstract(BDD f, BDD cube) {
  if ((f.IsZero() || f.IsOne()) && !cube.IsOne())
    return zero();
  BDD T = high(f);
  BDD E = low(f);
  if(level(f) == level(c)) { // current var is abstracted
    BDD uniqueThen = uniqueAbstract(T, high(c));
    BDD existElse = existAbstract(E, high(c));

    BDD existThen = existAbstract(T, high(c));
    BDD uniqueElse = uniqueAbstract(E, high(c));

    return (uniqueThen & !existElse) | (uniqueElse & !existThen)
  } else {
    BDD uniqueThen = uniqueAbstract(T,c);
    BDD uniqueElse = …

我正在使用 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 的值将前一个表分成两个单独的 s ，然后删除该节点：

如果x2 = 0：

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