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}