LAC
/
Questionnaire-2024
3
0
Fork 0
Code Issues Pull Requests Projects Releases 9 Wiki Activity
Browse Source

added solutions for ass1 bdds
continuous-integration/drone/push Build is passing
Details
continuous-integration/drone/tag Build is passing
Details

main release_bdd
sp 2 months ago
parent
4764fb59b4
commit
fe4fdbc6b0
6 changed files with 273 additions and 1 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      bdds/bdds.tex
  2. 5
      bdds/ex1.tex
  3. 114
      bdds/ex1_sol.tex
  4. 5
      bdds/ex2.tex
  5. 142
      bdds/ex2_sol.tex
  6. 2
      compile

6
bdds/bdds.tex
View File

@ -172,4 +172,10 @@
{bdds/0018_sol.tex}
{3cm}
\question{bdds/ex1.tex}
{bdds/ex1_sol.tex}
{3cm}
\question{bdds/ex2.tex}
{bdds/ex2_sol.tex}
{3cm}
\end{questionSection}

5
bdds/ex1.tex
View File

@ -0,0 +1,5 @@
\item \points{3} Construct a reduced ordered binary decision diagram (ROBDD) for the formula
$$f = (p \lor q) \land \neg (p \land q) \land r$$
using \textit{variable order} $q < p < r$. Use complemented edges and a node for \texttt{true} as the only constant node. To simplify drawing, you may assume that \textit{dangling edges} point to the constant node. Write down all cofactors that you compute to obtain the final result and mark them in the graph.

114
bdds/ex1_sol.tex
View File

@ -0,0 +1,114 @@
\begin{cofactors}
$f$ \= $= (((p \lor q) \land \lnot (p \land q)) \land r)$\\
\>$f_{q}$ \= $= (\lnot (p \land q) \land r)$\\
\>\>$f_{qp}$ \= $= \false$\\
\>\>$f_{q\lnot p}$ \= $= r$\\
\>\>\>$f_{q\lnot pr}$ \= $= \true$\\
\>\>\>$f_{q\lnot p\lnot r}$ \= $= \false$\\
\>$f_{\lnot q}$ \= $= (p \land r)$\\
\>\>$f_{\lnot qp}$ \= $= f_{q\lnot p}$\\
\>\>$f_{\lnot q\lnot p}$ \= $= \false$\\
\end{cofactors}
The final ROBDD:
\begin{center}
\scalebox{0.75}{
\begin{tikzpicture}[>=latex,line join=bevel,]
\pgfsetlinewidth{1bp}
%%
\pgfsetcolor{black}
% Edge: f_E -> q0
\draw [] (72.5bp,210.99bp) .. controls (72.5bp,200.92bp) and (72.5bp,185.47bp) .. (72.5bp,175.3bp);
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (72.5bp,195.3bp) node {\Large$\bullet$};
% Edge: f_q -> p1
\draw [] (123.5bp,152.99bp) .. controls (123.5bp,142.92bp) and (123.5bp,127.47bp) .. (123.5bp,117.3bp);
\draw (123.5bp,137.3bp) node {\Large$\bullet$};
% Edge: f_q!p -> r2
\draw [] (72.5bp,94.988bp) .. controls (72.5bp,84.921bp) and (72.5bp,69.474bp) .. (72.5bp,59.304bp);
% Edge: f_!q -> p3
\draw [] (21.5bp,152.99bp) .. controls (21.5bp,142.92bp) and (21.5bp,127.47bp) .. (21.5bp,117.3bp);
% Edge: q0 -> p3
\draw [] (65.409bp,155.21bp) .. controls (55.665bp,144.51bp) and (38.243bp,125.38bp) .. (28.531bp,114.72bp);
\draw (41.998bp,129.51bp) node {\Large$\bullet$};
% Edge: q0 -> p1
\draw [] (79.591bp,155.21bp) .. controls (89.335bp,144.51bp) and (106.76bp,125.38bp) .. (116.47bp,114.72bp);
% Edge: p3 -> r2
\draw [] (28.591bp,97.213bp) .. controls (38.335bp,86.514bp) and (55.757bp,67.385bp) .. (65.469bp,56.72bp);
% Edge: p3 -> 3
\draw [] (21.5bp,94.988bp) .. controls (21.5bp,79.384bp) and (21.5bp,50.854bp) .. (21.5bp,49.086bp);
\draw (21.5bp,69.086bp) node {\Large$\bullet$};
% Edge: p1 -> r2
\draw [] (116.41bp,97.213bp) .. controls (106.66bp,86.514bp) and (89.243bp,67.385bp) .. (79.531bp,56.72bp);
\draw (92.998bp,71.507bp) node {\Large$\bullet$};
% Edge: p1 -> 0
\draw [] (123.5bp,94.988bp) .. controls (123.5bp,79.384bp) and (123.5bp,50.854bp) .. (123.5bp,49.086bp);
% Edge: r2 -> 1
\draw [] (70.503bp,36.791bp) .. controls (67.934bp,23.663bp) and (63.77bp,2.3815bp) .. (63.513bp,1.0642bp);
% Edge: r2 -> 2
\draw [] (74.719bp,36.791bp) .. controls (77.573bp,23.663bp) and (82.2bp,2.3815bp) .. (82.486bp,1.0642bp);
\draw (78.237bp,20.608bp) node {\Large$\bullet$};
% Node: f_E
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (94.0bp,233.0bp) -- (51.0bp,233.0bp) -- (51.0bp,211.0bp) -- (94.0bp,211.0bp) -- cycle;
\draw (72.5bp,222.0bp) node {$f$};
\end{scope}
% Node: q0
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (72.5bp,164.0bp) ellipse (11.0bp and 11.0bp);
\draw (72.5bp,164.0bp) node {$q$};
\end{scope}
% Node: f_q
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (145.0bp,175.0bp) -- (102.0bp,175.0bp) -- (102.0bp,153.0bp) -- (145.0bp,153.0bp) -- cycle;
\draw (123.5bp,164.0bp) node {$f_{q}$};
\end{scope}
% Node: p1
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (123.5bp,106.0bp) ellipse (11.0bp and 11.0bp);
\draw (123.5bp,106.0bp) node {$p$};
\end{scope}
% Node: f_q!p
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (94.0bp,117.0bp) -- (51.0bp,117.0bp) -- (51.0bp,95.0bp) -- (94.0bp,95.0bp) -- cycle;
\draw (72.5bp,106.0bp) node {$f_{q\lnot p}$};
\end{scope}
% Node: r2
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (72.5bp,48.0bp) ellipse (11.0bp and 11.0bp);
\draw (72.5bp,48.0bp) node {$r$};
\end{scope}
% Node: f_!q
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (43.0bp,175.0bp) -- (0.0bp,175.0bp) -- (0.0bp,153.0bp) -- (43.0bp,153.0bp) -- cycle;
\draw (21.5bp,164.0bp) node {$f_{\lnot q}$};
\end{scope}
% Node: p3
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (21.5bp,106.0bp) ellipse (11.0bp and 11.0bp);
\draw (21.5bp,106.0bp) node {$p$};
\end{scope}
%
\end{tikzpicture}
}
\end{center}

5
bdds/ex2.tex
View File

@ -0,0 +1,5 @@
\item \points{3} Construct a reduced ordered binary decision diagram (ROBDD) for the formula
$$(a \lor \neg b) \land \neg(c \lor d) \lor (a \land b),$$
using \textit{variable order} $a < b < c < d$. Use complemented edges and a node for \texttt{true} as the only constant node. To simplify drawing, you may assume that \textit{dangling edges} point to the constant node. Write down all cofactors that you compute to obtain the final result and mark them in the graph.

142
bdds/ex2_sol.tex
View File

@ -0,0 +1,142 @@
\begin{cofactors}
$f$ \= $= (((a \lor \lnot b) \land \lnot (c \lor d)) \lor (a \land b))$\\
\>$f_{a}$ \= $= (\lnot (c \lor d) \lor b)$\\
\>\>$f_{ab}$ \= $= \true$\\
\>\>$f_{a\lnot b}$ \= $= \lnot (c \lor d)$\\
\>\>\>$f_{a\lnot bc}$ \= $= \false$\\
\>\>\>$f_{a\lnot b\lnot c}$ \= $= \lnot d$\\
\>\>\>\>$f_{a\lnot b\lnot cd}$ \= $= \false$\\
\>\>\>\>$f_{a\lnot b\lnot c\lnot d}$ \= $= \true$\\
%\>\>\>$f_{a\lnot b\lnot c}$ \= $= f_{a\lnot b}$\\
\>$f_{\lnot a}$ \= $= (\lnot b \land \lnot (c \lor d))$\\
\>\>$f_{\lnot ab}$ \= $= \false$\\
\>\>$f_{\lnot a\lnot b}$ \= $= f_{a\lnot b}$\\
\end{cofactors}
The final ROBDD:
\begin{center}
\scalebox{0.75}{
\begin{tikzpicture}[>=latex,line join=bevel,]
\pgfsetlinewidth{1bp}
%%
\pgfsetcolor{black}
% Edge: f_E -> a0
\draw [] (72.5bp,268.99bp) .. controls (72.5bp,258.92bp) and (72.5bp,243.47bp) .. (72.5bp,233.3bp);
% Edge: f_a -> b1
\draw [] (123.5bp,210.99bp) .. controls (123.5bp,200.92bp) and (123.5bp,185.47bp) .. (123.5bp,175.3bp);
% Edge: f_a!b -> c2
\draw [] (72.679bp,152.99bp) .. controls (72.859bp,142.92bp) and (73.134bp,127.47bp) .. (73.316bp,117.3bp);
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (72.959bp,137.3bp) node {\Large$\bullet$};
% Edge: f_a!b!c -> d3
\draw [] (157.14bp,94.988bp) .. controls (151.54bp,84.544bp) and (142.84bp,68.308bp) .. (137.42bp,58.183bp);
\draw (146.86bp,75.812bp) node {\Large$\bullet$};
% Edge: f_!a -> b4
\draw [] (21.5bp,210.99bp) .. controls (21.5bp,200.92bp) and (21.5bp,185.47bp) .. (21.5bp,175.3bp);
\draw (21.5bp,195.3bp) node {\Large$\bullet$};
% Edge: a0 -> b4
\draw [] (65.409bp,213.21bp) .. controls (55.665bp,202.51bp) and (38.243bp,183.38bp) .. (28.531bp,172.72bp);
\draw (41.998bp,187.51bp) node {\Large$\bullet$};
% Edge: a0 -> b1
\draw [] (79.591bp,213.21bp) .. controls (89.335bp,202.51bp) and (106.76bp,183.38bp) .. (116.47bp,172.72bp);
% Edge: b4 -> c2
\draw [] (28.73bp,155.21bp) .. controls (38.665bp,144.51bp) and (56.429bp,125.38bp) .. (66.331bp,114.72bp);
\draw (52.722bp,129.38bp) node {\Large$\circ$};
% Edge: b4 -> 4
\draw [] (21.5bp,152.99bp) .. controls (21.5bp,137.38bp) and (21.5bp,108.85bp) .. (21.5bp,107.09bp);
% Edge: b1 -> c2
\draw [] (116.55bp,155.21bp) .. controls (107.0bp,144.51bp) and (89.915bp,125.38bp) .. (80.393bp,114.72bp);
\draw (93.714bp,129.64bp) node {\Large$\bullet$};
% Edge: b1 -> 0
\draw [] (123.32bp,152.99bp) .. controls (123.04bp,137.38bp) and (122.53bp,108.85bp) .. (122.5bp,107.09bp);
% Edge: c2 -> c2
%\draw [] (81.517bp,113.81bp) .. controls (91.167bp,119.7bp) and (102.5bp,117.1bp) .. (102.5bp,106.0bp) .. controls (102.5bp,94.898bp) and (91.167bp,92.297bp) .. (81.517bp,98.194bp);
%\draw (99.287bp,89.018bp) node {\Large$\bullet$};
% Edge: c2 -> d3
\draw [] (81.213bp,97.679bp) .. controls (92.583bp,86.887bp) and (113.71bp,66.836bp) .. (124.97bp,56.146bp);
\draw (110.47bp,69.914bp) node {\Large$\circ$};
% Edge: c2 -> 1
\draw [] (73.5bp,94.988bp) .. controls (73.5bp,79.384bp) and (73.5bp,50.854bp) .. (73.5bp,49.086bp);
% Edge: d3 -> 2
\draw [] (130.28bp,36.791bp) .. controls (127.43bp,23.663bp) and (122.8bp,2.3815bp) .. (122.51bp,1.0642bp);
% Edge: d3 -> 3
\draw [] (134.5bp,36.791bp) .. controls (137.07bp,23.663bp) and (141.23bp,2.3815bp) .. (141.49bp,1.0642bp);
\draw (137.65bp,20.692bp) node {\Large$\bullet$};
% Node: f_E
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (94.0bp,291.0bp) -- (51.0bp,291.0bp) -- (51.0bp,269.0bp) -- (94.0bp,269.0bp) -- cycle;
\draw (72.5bp,280.0bp) node {$f$};
\end{scope}
% Node: a0
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (72.5bp,222.0bp) ellipse (11.0bp and 11.0bp);
\draw (72.5bp,222.0bp) node {$a$};
\end{scope}
% Node: f_a
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (145.0bp,233.0bp) -- (102.0bp,233.0bp) -- (102.0bp,211.0bp) -- (145.0bp,211.0bp) -- cycle;
\draw (123.5bp,222.0bp) node {$f_{a}$};
\end{scope}
% Node: b1
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (123.5bp,164.0bp) ellipse (11.0bp and 11.0bp);
\draw (123.5bp,164.0bp) node {$b$};
\end{scope}
% Node: f_a!b
\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_{a\lnot b}$};
\end{scope}
% Node: c2
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (73.5bp,106.0bp) ellipse (11.0bp and 11.0bp);
\draw (73.5bp,106.0bp) node {$c$};
\end{scope}
% Node: f_a!b!c
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (184.0bp,117.0bp) -- (141.0bp,117.0bp) -- (141.0bp,95.0bp) -- (184.0bp,95.0bp) -- cycle;
\draw (162.5bp,106.0bp) node {$f_{a\lnot b\lnot c}$};
\end{scope}
% Node: d3
\begin{scope}
\definecolor{strokecol}{rgb}{0.0,0.0,0.0};
\pgfsetstrokecolor{strokecol}
\draw (132.5bp,48.0bp) ellipse (11.0bp and 11.0bp);
\draw (132.5bp,48.0bp) node {$d$};
\end{scope}
% Node: f_!a
\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 a}$};
\end{scope}
% Node: b4
\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 {$b$};
\end{scope}
%
\end{tikzpicture}
}
\end{center}

2
compile
View File

@ -104,7 +104,7 @@ compile_wrapper() {
compile_chapter() {
#for chapter in smtzthree proplogic satsolver ndpred predlogic ndpred smt bdd eqchecking symbenc temporal
for chapter in satsolver
for chapter in bdd
do
set_chapter "\\chapter${chapter}true"
compile_wrapper "$chapter" "$@"

Write Preview
Loading…
Cancel
Save