计算表示为 ROBDD 数组的函数的集合图像

Question

我有一组整数，表示为一个简化有序二进制决策图(ROBDD)(解释为一个函数，如果输入在集合中，则计算结果为真)，我将其称为Domain，还有一个整数函数(我将其称为F)表示为一个ROBDD的数组(结果的每比特一个条目)。

现在我想计算F的域的图像，这绝对是可能的，因为它可以简单地通过枚举域中的所有项，应用F，并将结果插入到图像中来完成。但这是一个指数复杂度的可怕算法(域的大小是线性的)，我的直觉告诉我它可以更快。我一直在看方向:

1. 对F
的所有位应用Restrict(Domain)

但第二步被证明是困难的。第一步的结果包含了我需要的信息(至少，我有90%的把握)，但不是正确的形式。是否有一个有效的算法，把它变成一个"集编码为ROBDD"?我需要其他方法吗?

Answer 1

定义两个集值函数:

N(d1...dn): The subset of the image where members start with a particular sequence of digits d0...dn. 
D(d1...dn): The subset of the inputs that produce N(d1...dn).

那么当序列为空时，我们有一个完整的问题:

D(): The entire domain. 
N(): The entire image.

从完整定义域我们可以定义两个子集:

D(0) = The subset of D() such that F(x)[1]==0 for any x in D().
D(1) = The subset of D() such that F(x)[1]==1 for any x in D().

这个过程可以递归地应用于每个序列生成D。

D(d1...d[m+1]) = D(d1...dm) & {x | F(x)[m+1]==d[m+1]}

则可以确定完整序列的N(x):

N(d1...dn) = 0 if D(d1...dn) = {}
N(d1...dn) = 1 if D(d1...dn) != {}

可以从两个子节点生成父节点，直到生成N()。

如果在任意点我们确定D(d1…dm)是空的，那么我们知道N(d1…dm)也是空的，我们可以避免处理这个分支。这是主要的优化。

以下代码(Python)概述了这个过程:

def createImage(input_set_diagram,function_diagrams,index=0):
  if input_set_diagram=='0':
    # If the input set is empty, the output set is also empty
    return '0'
  if index==len(function_diagrams):
    # The set of inputs that produce this result is non-empty
    return '1'
  function_diagram=function_diagrams[index]
  # Determine the branch for zero
  set0=intersect(input_set_diagram,complement(function_diagram))
  result0=createImage(set0,function_diagrams,index+1)
  # Determine the branch for one
  set1=intersect(input_set_diagram,function_diagram)
  result1=createImage(set1,function_diagrams,index+1)
  # Merge if the same
  if result0==result1:
    return result0
  # Otherwise create a new node
  return {'index':index,'0':result0,'1':result1}

Answer 2

设S(x1, x2, x3，…xn)为集合S的指示函数，使得S(x1, x2，…xn) = true，如果(x1, x2，…xn)是S的一个元素，设F1(x1, x2, x3，…)xn), F2(),…Fn()是定义F的单个函数，然后我可以通过形成方程来询问是否有一个带有通配符的特定位模式在F的图像中，例如S() &F1 (),~F2()位模式10，然后求解这个方程，我认为我可以这样做，因为它是一个ROBDD。

当然你需要一个通用的指示函数，它告诉我abc是否在图像中。延伸以上，我认为你得到S() &(a&F1() | ~a&~F1()) &(b&F2() | ~b&~F2()) &…如果你对变量重新排序，使原来的x1 x2…xn在ROBDD顺序中最后出现，那么对于x1, x2，…的任何设置，您应该能够修剪树以返回true。Xn导致值为true，否则返回false。

(当然，您可能会耗尽空间或耐心等待重新排序工作)。