Find unique tuples in a relation represented by a BDD

Question

Let's suppose I use a BDD to represent the set of tuples in a relation. For simplicity consider tuples with 0 or 1 values. For instance: R = {<0,0,1>, <1,0,1>, <0,0,0>} represent a ternary relation in a BDD with three variables, say x, y and z (one for each tuple's element). What I want is to implement an operation that given a bdd like for R and a cube C returns the subset of R that contains unique tuples when the variables in C are abstracted.

For instance, if C contains the variable x (which represents the first element in each tuple) the result of the function must be {<0,0,0>}. Notice that when x is abstracted away tuples <0,0,1> and <1,0,1> become "the same".

Now suppose R = {<0,0,1>, <1,0,1>, <0,0,0>, <1,0,0>} and we want to abstract x again. In this case I would expect the constant false as result because there is no unique tuple in R after abstracting x.

Any help is highly appreciated.

Answer 1

This could be done in three simple steps:

• Make two BDDs with restricted value of the variable you want to abstract:
  • R[x=0] = restrict R with x = 0
  • R[x=1] = restrict R with x = 1
• Apply XOR operation to this new BDDs
  • Q = R[x=0] xor R[x=1]
• Enumerate all models of Q

Applying this to your examples:

• R = {<0,0,1>, <1,0,1>, <0,0,0>} = (¬x ∧ ¬y ∧ z) ∨ (x ∧ ¬y ∧ z) ∨ (¬x ∧ ¬y ∧ ¬z)
• R[x=1] = {<0,1>} = (¬y ∧ z)
• R[x=0] = {<0,1>,<0,0>} = (¬y ∧ z) ∨ (¬y ∧ ¬z)
• Q = R[x=1] xor R[x=0] = (¬y ∧ ¬z)

Intuition here is that XOR will cancel entries that occur in both BDDs.
This is easily (but with exponential complexity) generalized to the case with several abstracted variables.