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

Question

我有一组整数，表示为 降序二元决策图 (ROBDD ）（当且仅当输入在集合中时，被解释为一个计算结果为 true 的函数），我将其称为 Domain，以及一个整数函数（我将其称为 F），表示为 ROBDD 数组（ROBDD 的每一位都有一个条目） 结果）。

现在我想计算 F 的域图像。这绝对是可能的，因为它可以通过枚举域中的所有项目、应用 F 并将结果插入图像中来简单地完成。但这是一个可怕的算法，具有指数复杂性（与域的大小呈线性关系），而且我的直觉告诉我它可以更快。我一直在研究以下方向：

1. 将 Restrict(Domain) 应用于 F 的所有位，
2. 发挥魔法

但第二步被证明很困难。第一步的结果包含我需要的信息（至少我有 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 的指示函数，因此如果 (x1, x2,...xn) 是一个元素，则 S(x1, x2...xn) = true设 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、...xn 的任何设置导致值 true 的情况下返回 true，否则返回 false。

（当然，您可能会因为空间不足或耐心等待重新排序而起作用）。