BDD2FDD, clarification in solving certain terms

0 votes

I am  not able to figure out how the below terms marked in red are solved. I understood the algorithm but I am not able to figure out these below terms in red. Could you please explain this? (2022.02 Paper)

(0 ⊕ b ∧ 1) ⊕ a ∧ Apply(⊕,(0 ⊕ b ∧ BDD2FDD(n0)),(0 ⊕ b ∧ 1)

(0 ⊕ b ∧ 1) ⊕ a ∧ (0 ⊕ b ∧ Apply(⊕,(BDD2FDD(n0)), 1)

(0 ⊕ b ∧ 1) ⊕ a ∧ (0 ⊕ b ∧ Apply(⊕,(0 ⊕ c ∧ 1), 1)

(0 ⊕ b ∧ 1) ⊕ a ∧ (0 ⊕ b ∧ (1 ⊕ c ∧ (1 ⊕ 0)))

(0 ⊕ b ∧ 1) ⊕ a ∧ (0 ⊕ b ∧ (1 ⊕ c ∧ 1)

1 Answer

+1 vote

You have to consider the function BDD2FDD and also the Apply algorithm to understand the single steps. Indeed, the computation of the example solution has some unclarities which should be better explained here:

```    BDD2FDD(n3)
= BDD2FDD(n2) ⊕ a ∧ Apply(⊕, BDD2FDD(n1), BDD2FDD(n2))
// BDD2FDD(n2) = BDD2FDD(b) = (0⊕b∧1)
= (0⊕b∧1)⊕a∧Apply(⊕,BDD2FDD(n1),(0⊕b∧1))
// BDD2FDD(n1) = 0⊕b∧BDD2FDD(n0)
= (0⊕b∧1)⊕a∧Apply(⊕,(0⊕b∧BDD2FDD(n0)),(0⊕b∧1))
// Apply(⊕,(0⊕b∧BDD2FDD(n0)),(0⊕b∧1)) = (0⊕0)⊕b∧Apply(⊕,BDD2FDD(n0),1)
= (0⊕b∧1)⊕a∧(0⊕b∧Apply(⊕,(BDD2FDD(n0)),1))
// BDD2FDD(n0) = 0⊕c∧1
= (0⊕b∧1)⊕a∧(0⊕b∧Apply(⊕,(0⊕c∧1),1))
// Apply(⊕,(0⊕c∧1),1) = (0⊕1)⊕c∧1
= (0⊕b∧1)⊕a∧(0⊕b∧(1⊕c∧1))
```

Some remarks should clarify the computation: In general, if two formulas φ:⇔φ0⊕x∧δ (with δ:⇔φ0⊕φ1) and ψ:⇔ψ0⊕x∧ρ (with ρ:⇔ψ0⊕ψ1) are given, then we have φ⊕ψ⇔((φ0⊕ψ0)⊕x∧(δ⊕ρ)) (see pages 134-136 of the BDD chapter). Hence, the ⊕ operation has to be recursively applied to the high- and low-parts of the given FDDs φ and ψ which is exactly what the Apply algorithm for BDD does if it would be applied to the FDDs. Hence, we can simply (mis-)use the BDD algorithm for Apply with ⊕ and the FDDs (even though the Apply algorithm is meant to work with BDDs) and it will correctly compute the result. However, we have to use the FDD elimination rule.

In particular, to compute Apply(⊕,(0⊕b^BDD2FDD(n0)),(0⊕b^1)), we can proceed as follows: We consider the "low-parts" 0 and 0, and the "high-parts" BDD2FDD(n0) and 1, so that Apply(⊕,(0⊕b∧BDD2FDD(n0)),(0⊕b∧1)) is the same as (0⊕0)⊕b∧Apply(⊕,BDD2FDD(n0),1).

In the second case, we have to compute Apply(⊕,(0⊕c∧1),1) which is reduced by the Apply algorithm to (0⊕1)⊕c∧1 which is same as 1⊕c∧1.

by (147k points)
edited by
1) (0⊕b∧1)⊕a∧Apply(⊕,(0⊕b∧BDD2FDD(n0)),(0⊕b∧1))

(0⊕b∧1)⊕a∧(0⊕b∧Apply(⊕,(BDD2FDD(n0)),1))  (Since 0⊕b is present in both the terms (0⊕b∧BDD2FDD(n0)),(0⊕b∧1)), we brought the term 0⊕b outside). Is my understanding correct?

2) Apply(⊕,(0⊕c∧1),1) = (0⊕1)⊕c∧1
I am a little confused about how to implement the apply algorithm with the above using
Apply(op,Φ,L) = XΦ?Apply(op,Φ1,L) : Apply(op,Φ0,L)

Please help me with this.
I have seen that a comment in the computation was broken into a separate line which may have been also confusing. I have fixed that and have added more details on the computation that hopefully clarify that.

0 votes
2 answers
0 votes
2 answers
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer