\begin{cofactors} $f_{a}$ \= $= b \lor(c \biimp d)$ \\ \>$f_{ab}$ \= $= \true $\\ \>$f_{a\lnot b}$ \= $= c \biimp d$ \\ \>\>$f_{a\lnot bc}$ \= $= d$ \\ \>\>\>$f_{a\lnot b c d}$ \= $= \true$ \\ \>\>\>$f_{a\lnot bc\lnot d}$ \= $= \false$ \\ \>\>$f_{a\lnot b\lnot c}$ \= $= \lnot d = f_{abc}$ \\ $f_{\lnot a}$ \= $=\true $ \end{cofactors} The final ROBDD:\\ \begin{center} \begin{bdd} \node[func node] (f) {$f$}; \node[cofactor] (a1) [below of=f] {$a$}; \node[phantom] (aR) [below right of=a1] {}; \node[cofactor] (b1) [below left of=a1] {$b$}; \node[phantom] (bL) [below left of=b1] {}; \node[cofactor] (c1) [below right of=b1] {$c$}; \node[cofactor] (d1) [below of=c1] {$d$}; \node[phantom] (dL) [below left of=d1] {}; \node[phantom] (dR) [below right of=d1] {}; \funcEdge{f}{a1} \thenEdge{a1}{b1} \elseEdge{a1}{aR} \thenEdge{b1}{bL} \elseEdge{b1}{c1} \thenEdge[bend right]{c1}{d1} \negatedEdge[bend left]{c1}{d1} \thenEdge{d1}{dL} \elseEdge{d1}{dR} \end{bdd} \end{center}