algorithm - 扩展查找由 BDD 表示的关系中的唯一元组

Question

将 {<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 与输入的结合来重建预期的关系。

总之，问题是：必须对 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 = uniqueAbstract(E,c);
    return ite(top(f), uniqueThen, uniqueElse);
  }
}

EDIT2：在尝试了三种不同的实现之后，仍然存在一些性能问题。让我来描述他们三个。

1. 我的方法的 AC 实现，让我称之为参考实现4。
2. 用户 meolic 在接受的答案3中提出的实现。
3. 两者之间的混合方法和可用2。

本次更新的目标是分析一下使用这三种方法的结果。由于此时时间度量似乎会误导判断它们，因此我决定在一组不同的度量上评估实现。

• 递归调用
• 缓存命中
• 抽象简单。无需存在抽象即可解决函数调用的次数。
• 抽象复合体：需要存在抽象解决函数调用的次数。
• 存在抽象：对存在抽象的调用次数。

实现 1 的结果：（21123 毫秒）：唯一抽象统计：递归调用：1728549.000000 缓存命中：638745.000000 非抽象：67207.000000 简单抽象：0.000000 复杂抽象：0.000000 现有抽象：1593430.000000

实现 2 的结果：（运行时间：54727 毫秒）唯一抽象统计：递归调用：191585.000000 缓存命中：26494.000000 简单抽象：59788.000000 复杂抽象：12011.000000 现有抽象：24022.000000

实现 3 的结果：（运行时间：20215 毫秒）唯一抽象统计：递归调用：268044.000000 缓存命中：30668.000000 简单抽象：78115.000000 复杂抽象：46473.000000 现有抽象：92946.000000

编辑 3：根据 ITE 5实施每个逻辑操作后获得以下结果。

1. uniqueAbstractRecRef (21831 ms) 唯一抽象统计：总调用：1723239 优化调用：0 总存在抽象调用：30955618 对存在抽象的唯一抽象调用：2385915 总 ite 调用：3574555 在总时间中，uniqueAbstractRecRef 需要 4001 毫秒 (12.4%)

2. uniqueAbstractSERec (56761 ms) 唯一抽象统计：总调用：193627 优化调用：60632 总存在抽象调用：16475806 对存在抽象的唯一抽象调用：24304 总 ite 调用：1271844 在总时间中，uniqueAbstractSERec 需要 33918 ms (51.5%)

3. uniqueAbstractRec (20587 ms) 唯一抽象统计：总调用：270205 优化调用：78486 总存在抽象调用：13186348 对存在抽象的唯一抽象调用：93060 总 ite 调用：1256872 在总时间中，uniqueAbstractRec 需要 3354 ms (10.6%)

Answer 1

这是我的实现。我研究了作者提出的解决方案，在我看来，如果不是唯一的简单的基于 BDD 的任意排序解决方案，它就是最好的。但是，如果算法以我的方式实现，可能会有一些改进——请检查。我在 BDD 包上使用了我自己的包装器，但你应该不会有任何麻烦来理解它。

编辑：我已经简化了解决方案，不再使用函数 Bdd_GetVariableChar() 。

/* TESTING SOLUTION FOR QUESTION ON STACK OVERFLOW */
/* bdd_termFalse,bdd_termTrue: Boolean constants */
/* Bdd_isTerminal(f): check if f is Boolean constant */
/* Bdd_Low(f),Bdd_High(f): 'else' and 'then' subfunction */
/* Bdd_Top(f): literal function representing topvar of f */
/* Bdd_IsSmaller(f,g): check if topvar of f is above topvar of g */
/* existentialAbstraction(f,cube): \exist v.f for all v in cube */

Bdd_Edge specialAbstraction(Bdd_Edge f, Bdd_Edge cube) {
  if (Bdd_isTerminal(cube)) return f;
  if (Bdd_isTerminal(f)) return bdd_termFalse;
  if (Bdd_IsSmaller(f,cube)) {
    Bdd_Edge E,T;
    E = specialAbstraction(Bdd_Low(f),cube);
    T = specialAbstraction(Bdd_High(f),cube);
    return Bdd_ITE(Bdd_Top(f),T,E);
  } else if (Bdd_IsSmaller(cube,f)) {
    return bdd_termFalse;
  } else {
    Bdd_Edge E,T;
    cube = Bdd_High(cube);
    E = Bdd_Low(f);
    T = Bdd_High(f);
    if (Bdd_isEqv(E,bdd_termFalse)) {
      return specialAbstraction(T,cube);
    } else if (Bdd_isEqv(T,bdd_termFalse)) {
      return specialAbstraction(E,cube);
    } else {
      Bdd_Edge EX,TX,R;
      EX = existentialAbstraction(E,cube);
      TX = existentialAbstraction(T,cube);
      if (Bdd_isEqv(EX,TX)) return bdd_termFalse;
      R = Bdd_ITE(Bdd_ITE(EX,bdd_termFalse,T),
                  bdd_termTrue,
                  Bdd_ITE(TX,bdd_termFalse,E));
      return specialAbstraction(R,cube);
    }
  }
}

而且，是的，如果变量排序是固定的，x 高于 y，那么算法真的可以更有效 - 你可以从最复杂的“else”块中删除所有计算并返回 0。

以下是一些测试运行：

CUBE (JUST IN CASE YOU ARE NOT FAMILIAR WITH BDD ALGORITHMS)
  +  y1 y2 y3 y4 y5

ORIGINAL (ORDERED WITH X ABOVE Y)
  +  *x1 *x2 x3 *x4 x5 y1 *y2 y3 y4 y5
  +  *x1 x2 *x3 *x4 *x5 y1 y2 *y3 y4 y5
  +  *x1 x2 *x3 *x4 x5 *y1 y2 *y3 y4 y5
  +  *x1 x2 *x3 x4 *x5 y1 *y2 y3 *y4 *y5
  +  *x1 x2 x3 *x4 x5 *y1 *y2 *y3 *y4 y5
  +  *x1 x2 x3 *x4 x5 *y1 y2 y3 *y4 *y5
  +  x1 *x2 *x3 *x4 *x5 y1 y2 y3 y4 *y5
  +  x1 x2 *x3 x4 x5 *y1 *y2 *y4 *y5
  +  x1 x2 x3 *x4 *x5 *y1 *y2 *y3 y4 *y5

ABSTRACTION
  +  *x1 *x2 x3 *x4 x5
  +  *x1 x2 *x3 *x4
  +  *x1 x2 *x3 x4 *x5
  +  x1 *x2 *x3 *x4 *x5
  +  x1 x2 x3 *x4 *x5

ORIGINAL (ORDERED WITH Y ABOVE X)
  +  *y1 *y2 *y3 *y4 *y5 x1 x2 *x3 x4 x5
  +  *y1 *y2 *y3 *y4 y5 *x1 x2 x3 *x4 x5
  +  *y1 *y2 *y3 y4 *y5 x1 x2 x3 *x4 *x5
  +  *y1 *y2 y3 *y4 *y5 x1 x2 *x3 x4 x5
  +  *y1 y2 *y3 y4 y5 *x1 x2 *x3 *x4 x5
  +  *y1 y2 y3 *y4 *y5 *x1 x2 x3 *x4 x5
  +  y1 *y2 y3 *y4 *y5 *x1 x2 *x3 x4 *x5
  +  y1 *y2 y3 y4 y5 *x1 *x2 x3 *x4 x5
  +  y1 y2 *y3 y4 y5 *x1 x2 *x3 *x4 *x5
  +  y1 y2 y3 y4 *y5 x1 *x2 *x3 *x4 *x5

ABSTRACTION
  +  *x1 *x2 x3 *x4 x5
  +  *x1 x2 *x3 *x4
  +  *x1 x2 *x3 x4 *x5
  +  x1 *x2 *x3 *x4 *x5
  +  x1 x2 x3 *x4 *x5

ORIGINAL (MIXED ORDER)
  +  *x1 *x2 y1 *y2 y3 y4 y5 x3 *x4 x5
  +  *x1 x2 *y1 *y2 *y3 *y4 y5 x3 *x4 x5
  +  *x1 x2 *y1 y2 *y3 y4 y5 *x3 *x4 x5
  +  *x1 x2 *y1 y2 y3 *y4 *y5 x3 *x4 x5
  +  *x1 x2 y1 *y2 y3 *y4 *y5 *x3 x4 *x5
  +  *x1 x2 y1 y2 *y3 y4 y5 *x3 *x4 *x5
  +  x1 *x2 y1 y2 y3 y4 *y5 *x3 *x4 *x5
  +  x1 x2 *y1 *y2 *y3 *y4 *y5 *x3 x4 x5
  +  x1 x2 *y1 *y2 *y3 y4 *y5 x3 *x4 *x5
  +  x1 x2 *y1 *y2 y3 *y4 *y5 *x3 x4 x5

ABSTRACTION
  +  *x1 *x2 x3 *x4 x5
  +  *x1 x2 *x3 *x4
  +  *x1 x2 *x3 x4 *x5
  +  x1 *x2 *x3 *x4 *x5
  +  x1 x2 x3 *x4 *x5

Answer 2

如果变量以 x1 和 x2 位于 BDD 顶部的方式排序，则存在简单而有效的解决方案。

第二个例子考虑 BDD。

您可以（按广度优先顺序）遍历它的前两层以获得四个子 BDD。每个可能的组合一个x1,x2。其中三个子 BDD 根植于y1，第四个是空的（常量 False）。

现在您可以计算每个子 BDD 中的元素数量（Knuth 的第 4 卷分册 1 中的算法 C，按位技巧和技术；二进制决策图）。

如果 sub-BDD 中的元素数量大于 1，则将其删除（从父节点直接到 的快捷方式False），否则保持原样。

通过在计算元素时记住部分结果，可以单次运行该算法。

Answer 3

一种方法涉及直接翻译唯一性的定义：

R(x,y) and forall z . ~R(x,z) or y = z

一个实现可能如下所示：

def inspect(function, name, nvars):
    sys.stdout.write(name) # avoid print's trailing space or newline
    function.summary(nvars) # minterm count needs number of variables
    function.printCover()

import sys
from cudd import Cudd
m = Cudd()

nx = 2
ny = 3
x = [m.bddVar() for i in range(nx)]
y = [m.bddVar() for i in range(ny)]

R = (~x[0] & x[1] & (~y[0] & y[1] | y[1] & y[2]) |
     x[0] & ~x[1] & (y[0] ^ y[1]) & y[2] |
     ~x[0] & ~x[1] & y[0] & ~y[1] & ~y[2])

# This approach is independent of variable order.  We are free to enable
# reordering or call it explicitly.
m.reduceHeap()

inspect(R, 'R', nx+ny)

# Create auxiliary variables and selector function.
z = [m.bddVar() for i in range(ny)]
zcube = reduce(lambda a, b: a & b, z)
P = ~m.xeqy(y,z)

# A pair is in L iff:
#   - it is in R
#   - there is no other pair in R with the same x and different y
L = R & ~(R.swapVariables(y,z).andAbstract(P,zcube))

inspect(L, 'L', nx+ny)

运行该代码的结果：

R: 10 nodes 1 leaves 6 minterms
01-11 1
10101 1
10011 1
00100 1
0101- 1

L: 6 nodes 1 leaves 1 minterms
00100--- 1

前两个变量编码该对的第一个元素；接下来的三个变量编码该对的第二个元素；最后三个变量是辅助变量。

该代码将 DeMorgan 应用于上述公式以利用andAbstract.