You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
207 lines
8.9 KiB
207 lines
8.9 KiB
\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}
|
|
|
|
|