假设我使用BDD来表示关系中的元组集合。为简单起见，考虑值为0或1的元组。例如:R = {<0,0,1>， <1,0,1>， <0,0,0>}表示具有三个变量的BDD中的三元关系，例如x, y和z(每个元组的元素一个)。我想要实现的是这样一个操作:给定一个像R的bdd和一个立方体C，当C中的变量被抽象时，返回R的包含唯一元组的子集。
例如，如果C包含变量x(它表示每个元组中的第一个元素)，则函数的结果必须是{<0,0,0>}。注意，当x被抽象掉时，元组<0,0,1>和<1,0,1>变得"相同"。
现在假设R = {<0,0,1>， <1,0,1>， <0,0,0>， <1,0,0>}，我们想再次抽象x。在这种情况下，我希望常数false作为结果，因为在抽象x之后，R中没有唯一的元组。
非常感谢任何帮助。
这可以通过三个简单的步骤完成:
- 创建两个bdd，其中包含要抽象的变量的限制值:
- R[x=0] =
- R[x=1] =限制R与x=1
- 对新的bdd应用异或操作
- Q = R[x=0] xor R[x=1]
- 枚举Q 的所有模型
应用到你的例子:
- R = {& lt; 0, 0, 1> & lt; 1, 0, 1> & lt; 0, 0, 0>} = x∧(¬¬y∧z)∨(x∧¬y∧z)∨(¬x∧y∧¬¬z)
- R[x=1] = {<0,1>} = (y∧z)
- R (x = 0) = {& lt; 0,1> & lt; 0, 0>} =(¬y z∧∨)(y∧¬¬z)
- Q = R[x=1] xor R[x=0] = (y∧z)
这里的直觉是异或将取消两个bdd中出现的条目。
这很容易(但具有指数复杂度)推广到几个抽象变量的情况。