Calculate image of a set for a function represented as an array of ROBDD's

Question

I have a set of integers, represented as a Reduced Ordered Binary Decision Diagram (ROBDD) (interpreted as a function which evaluates to true iff the input is in the set) which I shall call Domain, and an integer function (which I shall call F) represented as an array of ROBDD's (one entry per bit of the result).

Now I want to calculate the image of the domain for F. It's definitely possible, because it could trivially be done by enumerating all items from the domain, apply F, and insert the result in the image. But that's a horrible algorithm with exponential complexity (linear in the size of the domain), and my gut tells me it can be faster. I've been looking into the direction of:

1. apply Restrict(Domain) to all bits of F
2. do magic

But the second step proved difficult. The result of the first step contains the information I need (at least, I'm 90% sure of it), but not in the right form. Is there an efficient algorithm to turn it into a "set encoded as ROBDD"? Do I need an other approach?

Answer 1

Define two set-valued functions:

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).

Then when the sequences are empty, we have our full problem:

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

From the full domain we can define two subsets:

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().

This process can be applied recursively to generate D for every sequence.

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

We can then determine N(x) for the full sequences:

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

The parent nodes can be produced from the two children, until we've produced N().

If at any point we determine that D(d1...dm) is empty, then we know that N(d1...dm) is also empty, and we can avoid processing that branch. This is the main optimization.

The following code (in Python) outlines the process:

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

Let S(x1, x2, x3...xn) be the indicator function for the set S, so that S(x1, x2...xn) = true if (x1, x2,...xn) is an element of S. Let F1(x1, x2, x3... xn), F2(),... Fn() be the individual functions that define F. Then I could ask if a particular bit pattern, with wild cards, is in the image of F by forming the equation e.g. S() & F1() & ~F2() for bit-pattern 10 and then solving this equation, which I presume that I can do since it is an ROBDD.

Of course you want a general indicator function, which tells me if abc is in the image. Extending the above, I think you get S() & (a&F1() | ~a&~F1()) & (b&F2() | ~b&~F2()) &... If you then re-order the variables so that the original x1, x2, ... xn occur last in the ROBDD order, then you should be able to prune the tree to return true for the case where any setting of the x1, x2, ... xn leads to the value true, and to return false otherwise.

(of course you could run of space, or patience, waiting for the re-ordering to work).