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

Question

我有一组整数，表示为约序二元决策图 (ROBDD) (解释为在输入位于集合中的情况下计算为真的函数)，我将调用域；整数函数(我将调用F)表示为ROBDD的数组(结果的每位一个条目)。

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

1. 对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的指示函数，使得S(x1，x2...xn) = true if (x1，x2，...xn)是S.，F2()，.Fn()是定义F的单个函数，那么我可以通过对位模式10的方程(例如S() & F1()和~F2() )的形成，然后求解这个方程，这样我就可以在F的图像中找到一个特定的比特模式，因为它是一个ROBDD。

当然，您需要一个通用的指示函数，它告诉我abc是否在图像中。扩展以上，我认为得到了S() & (a&F1() x~a&~f_1())和(b&F_2()_x~b&~F_2())&……如果然后重新排序变量，使原始的x1，x2，.xn在ROBDD顺序中最后出现，那么您应该能够修剪树以返回x1、x2、.的任何设置的true。xn导致值true，否则返回false。

(当然，你可以利用空间，或者耐心，等待重新排序开始工作)。