\begin{cofactors} $f$ \= $= (((p \land q) \lor (r \land \lnot s)) \lor ((\lnot p \land t) \land u))$\\ \>$f_{p}$ \= $= (q \lor (r \land \lnot s))$\\ \>\>$f_{pq}$ \= $= \true$\\ \>\>$f_{p\lnot q}$ \= $= (r \land \lnot s)$\\ \>\>\>$f_{p\lnot qr}$ \= $= \lnot s$\\ \>\>\>\>$f_{p\lnot qrs}$ \= $= \false$\\ \>\>\>\>$f_{p\lnot qr\lnot s}$ \= $= \true$\\ \>\>\>$f_{p\lnot q\lnot r}$ \= $= \false$\\ \>$f_{\lnot p}$ \= $= ((r \land \lnot s) \lor (t \land u))$\\ \>\>$f_{\lnot pr}$ \= $= (\lnot s \lor (t \land u))$\\ \>\>\>$f_{\lnot prs}$ \= $= (t \land u)$\\ \>\>\>\>$f_{\lnot prst}$ \= $= u$\\ \>\>\>\>\>$f_{\lnot prstu}$ \= $= \true$\\ \>\>\>\>\>$f_{\lnot prst\lnot u}$ \= $= \false$\\ \>\>\>\>$f_{\lnot prs\lnot t}$ \= $= \false$\\ \>\>\>$f_{\lnot pr\lnot s}$ \= $= \true$\\ \>\>$f_{\lnot p\lnot r}$ \= $= f_{\lnot prs}$\\ \end{cofactors} The final ROBDD: \begin{center} \scalebox{0.75}{ \begin{tikzpicture}[>=latex,line join=bevel,] \pgfsetlinewidth{1bp} %% \pgfsetcolor{black} % Edge: f_E -> p0 \draw [] (128.5bp,326.99bp) .. controls (128.5bp,316.92bp) and (128.5bp,301.47bp) .. (128.5bp,291.3bp); % Edge: f_p -> q1 \draw [] (174.49bp,268.99bp) .. controls (169.27bp,258.54bp) and (161.15bp,242.31bp) .. (156.09bp,232.18bp); % Edge: f_p!q -> r2 \draw [] (198.75bp,210.99bp) .. controls (194.88bp,200.67bp) and (188.89bp,184.7bp) .. (185.08bp,174.55bp); \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (192.1bp,193.28bp) node {\Large$\bullet$}; % Edge: f_p!qr -> s3 \draw [] (231.61bp,152.99bp) .. controls (230.71bp,142.92bp) and (229.33bp,127.47bp) .. (228.42bp,117.3bp); \draw (230.2bp,137.22bp) node {\Large$\bullet$}; % Edge: f_!p -> r4 \draw [] (82.685bp,268.99bp) .. controls (88.094bp,258.54bp) and (96.501bp,242.31bp) .. (101.74bp,232.18bp); % Edge: f_!pr -> s5 \draw [] (21.5bp,210.99bp) .. controls (21.5bp,200.92bp) and (21.5bp,185.47bp) .. (21.5bp,175.3bp); % Edge: f_!prs -> t6 \draw [] (73.394bp,152.99bp) .. controls (74.293bp,142.92bp) and (75.672bp,127.47bp) .. (76.58bp,117.3bp); % Edge: f_!prst -> u7 \draw [] (161.32bp,94.988bp) .. controls (155.91bp,84.544bp) and (147.5bp,68.308bp) .. (142.26bp,58.183bp); % Edge: p0 -> r4 \draw [] (124.77bp,269.5bp) .. controls (120.75bp,259.27bp) and (114.38bp,243.06bp) .. (110.32bp,232.73bp); \draw (117.64bp,251.35bp) node {\Large$\circ$}; % Edge: p0 -> q1 \draw [] (132.4bp,269.5bp) .. controls (136.66bp,259.14bp) and (143.42bp,242.66bp) .. (147.66bp,232.36bp); % Edge: r4 -> s5 \draw [] (97.724bp,215.22bp) .. controls (81.436bp,204.49bp) and (46.704bp,181.6bp) .. (30.356bp,170.83bp); % Edge: r4 -> t6 \draw [] (107.27bp,210.63bp) .. controls (107.97bp,197.09bp) and (108.15bp,172.79bp) .. (102.5bp,153.0bp) .. controls (98.455bp,138.84bp) and (89.518bp,124.18bp) .. (83.501bp,115.32bp); \draw (94.602bp,131.96bp) node {\Large$\circ$}; % Edge: s5 -> t6 \draw [] (28.821bp,155.68bp) .. controls (39.494bp,145.01bp) and (59.224bp,125.28bp) .. (69.998bp,114.5bp); % Edge: s5 -> 7 \draw [] (21.5bp,152.99bp) .. controls (21.5bp,137.38bp) and (21.5bp,108.85bp) .. (21.5bp,107.09bp); \draw (21.5bp,127.09bp) node {\Large$\circ$}; % Edge: t6 -> u7 \draw [] (85.344bp,97.679bp) .. controls (96.906bp,86.887bp) and (118.39bp,66.836bp) .. (129.84bp,56.146bp); % Edge: t6 -> 6 \draw [] (77.5bp,94.988bp) .. controls (77.5bp,79.384bp) and (77.5bp,50.854bp) .. (77.5bp,49.086bp); \draw (77.5bp,69.086bp) node {\Large$\bullet$}; % Edge: u7 -> 4 \draw [] (135.28bp,36.791bp) .. controls (132.43bp,23.663bp) and (127.8bp,2.3815bp) .. (127.51bp,1.0642bp); % Edge: u7 -> 5 \draw [] (139.5bp,36.791bp) .. controls (142.07bp,23.663bp) and (146.23bp,2.3815bp) .. (146.49bp,1.0642bp); \draw (142.65bp,20.692bp) node {\Large$\bullet$}; % Edge: q1 -> r2 \draw [] (156.32bp,212.0bp) .. controls (161.89bp,201.61bp) and (170.99bp,184.62bp) .. (176.59bp,174.16bp); \draw (167.15bp,191.79bp) node {\Large$\bullet$}; % Edge: q1 -> 0 \draw [] (151.5bp,210.99bp) .. controls (151.5bp,195.38bp) and (151.5bp,166.85bp) .. (151.5bp,165.09bp); % Edge: r2 -> s3 \draw [] (188.29bp,154.74bp) .. controls (197.08bp,144.03bp) and (212.32bp,125.48bp) .. (220.98bp,114.93bp); % Edge: r2 -> 3 \draw [] (173.89bp,155.63bp) .. controls (164.66bp,146.64bp) and (148.71bp,130.93bp) .. (135.5bp,117.0bp) .. controls (131.64bp,112.93bp) and (127.11bp,107.7bp) .. (126.56bp,107.06bp); \draw (139.66bp,122.18bp) node {\Large$\circ$}; % Edge: s3 -> 1 \draw [] (225.71bp,94.988bp) .. controls (222.93bp,79.384bp) and (217.83bp,50.854bp) .. (217.52bp,49.086bp); % Edge: s3 -> 2 \draw [] (229.11bp,94.988bp) .. controls (231.62bp,79.384bp) and (236.2bp,50.854bp) .. (236.49bp,49.086bp); \draw (233.31bp,68.833bp) node {\Large$\bullet$}; % Node: f_E \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (150.0bp,349.0bp) -- (107.0bp,349.0bp) -- (107.0bp,327.0bp) -- (150.0bp,327.0bp) -- cycle; \draw (128.5bp,338.0bp) node {$f$}; \end{scope} % Node: p0 \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (128.5bp,280.0bp) ellipse (11.0bp and 11.0bp); \draw (128.5bp,280.0bp) node {$p$}; \end{scope} % Node: f_p \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (201.0bp,291.0bp) -- (158.0bp,291.0bp) -- (158.0bp,269.0bp) -- (201.0bp,269.0bp) -- cycle; \draw (179.5bp,280.0bp) node {$f_{p}$}; \end{scope} % Node: q1 \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (151.5bp,222.0bp) ellipse (11.0bp and 11.0bp); \draw (151.5bp,222.0bp) node {$q$}; \end{scope} % Node: f_p!q \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (224.0bp,233.0bp) -- (181.0bp,233.0bp) -- (181.0bp,211.0bp) -- (224.0bp,211.0bp) -- cycle; \draw (202.5bp,222.0bp) node {$f_{p\lnot q}$}; \end{scope} % Node: r2 \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (181.5bp,164.0bp) ellipse (11.0bp and 11.0bp); \draw (181.5bp,164.0bp) node {$r$}; \end{scope} % Node: f_p!qr \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (254.0bp,175.0bp) -- (211.0bp,175.0bp) -- (211.0bp,153.0bp) -- (254.0bp,153.0bp) -- cycle; \draw (232.5bp,164.0bp) node {$f_{p\lnot qr}$}; \end{scope} % Node: s3 \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (227.5bp,106.0bp) ellipse (11.0bp and 11.0bp); \draw (227.5bp,106.0bp) node {$s$}; \end{scope} % Node: f_!p \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (99.0bp,291.0bp) -- (56.0bp,291.0bp) -- (56.0bp,269.0bp) -- (99.0bp,269.0bp) -- cycle; \draw (77.5bp,280.0bp) node {$f_{\lnot p}$}; \end{scope} % Node: r4 \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (106.5bp,222.0bp) ellipse (11.0bp and 11.0bp); \draw (106.5bp,222.0bp) node {$r$}; \end{scope} % Node: f_!pr \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (43.0bp,233.0bp) -- (0.0bp,233.0bp) -- (0.0bp,211.0bp) -- (43.0bp,211.0bp) -- cycle; \draw (21.5bp,222.0bp) node {$f_{\lnot pr}$}; \end{scope} % Node: s5 \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (21.5bp,164.0bp) ellipse (11.0bp and 11.0bp); \draw (21.5bp,164.0bp) node {$s$}; \end{scope} % Node: f_!prs \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (94.0bp,175.0bp) -- (51.0bp,175.0bp) -- (51.0bp,153.0bp) -- (94.0bp,153.0bp) -- cycle; \draw (72.5bp,164.0bp) node {$f_{\lnot prs}$}; \end{scope} % Node: t6 \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (77.5bp,106.0bp) ellipse (11.0bp and 11.0bp); \draw (77.5bp,106.0bp) node {$t$}; \end{scope} % Node: f_!prst \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (188.0bp,117.0bp) -- (145.0bp,117.0bp) -- (145.0bp,95.0bp) -- (188.0bp,95.0bp) -- cycle; \draw (166.5bp,106.0bp) node {$f_{\lnot prst}$}; \end{scope} % Node: u7 \begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (137.5bp,48.0bp) ellipse (11.0bp and 11.0bp); \draw (137.5bp,48.0bp) node {$u$}; \end{scope} % \end{tikzpicture} } \end{center}