Find unique tuples in the relation presented by BDD

Question

Suppose I use BDD to represent a set of tuples in a relation. For simplicity, consider tuples with 0 or 1 values. For example: R = {<0,0,1>, <1,0,1>, <0,0,0>} represent a triple ratio in BDD with three variables, for example x, y and z (one for each element tuple). I want to implement an operation that gives bdd, as for R, and the cube C returns a subset of R that contains unique tuples when the variables from C. are abstracted.

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

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

Any help is greatly appreciated.

Answer 1

This can be done in three simple steps:

• Make two BDDs with the limited value of the variable you want to abstract:
  • R [x = 0] = limits R with x = 0
  • R [x = 1] = limit R with x = 1
• Apply XOR operation to these new BDDs
  • Q = R [x = 0] xor R [x = 1]
• List all Q models

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)

The intuition here is that XOR cancels the records that are found in both BDDs.
This is easy (but with exponential complexity) to generalize to the case with several abstract variables.