Exam Paper 2015.10.15: Question 2d

Question

According to the question statement- 

Formula x3 ∨ x4 should be considered 'alpha' in the algorithm and other diagram should be a ϕ. But in the solution, it is given vise.versa. 

I am referring to the below algorithm-

is the solution in the exam paper correct?

Answer 1

The solution is correct. You can use the teaching tool to convince yourself about this: Use the tool https://es.cs.uni-kl.de/tools/teaching/BDDAlgorithms.html, and select 

• action = Compose
• style = Show false leaf
• variable ordering : x1;x2;x3;x4
• first operand (bdd1) : x3 | x4
• second operand (bdd2) : true ⊕ x1 ⊕ x2 ⊕ x3 ⊕ x4
• variable for compose: x2

This will compute the BDD for [true ⊕ x1 ⊕ x2 ⊕ x3 ⊕ x4]{x2 := x3 | x4}, i.e., the BDD for true ⊕ x1 ⊕ (x3 | x4) ⊕ x3 ⊕ x4.