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.