\documentclass[12pt,a4paper]{report}

\usepackage{latexsym}

\pagestyle{empty}
\begin{document} \large

\noindent {\bf\Large Procedimento Reduce:}

\vspace*{.5cm}
\begin{flushleft}
{\bf Entrada:} um OBDD {\em bdd\/}. \\
{\bf Sa\'{\i}da:} um OBDD equivalente reduzido.
\end{flushleft}

\vspace*{.3cm}
\begin{tabbing}
xxx\=xx\=xxx\=xxxxxx\= \kill
{\bf se} {\em bdd\/} tem mais de duas folhas (de r\a'otulos V e F) {\bf ent\~ao} \\
 \> remova as folhas duplicadas; \\
 \> dirija as arestas que apontavam para as folhas removidas para \\
 \> \> \> as n\~ao removidas \\
{\bf fimse}; \\
{\bf repita} enquanto poss\a'{\i}vel \\
 \> 1. \> {\bf se} ambas as arestas de um nodo n\~ao folha $v_i$ apontam
                         para \\
 \>    \> \> \>  um mesmo $v_j$ {\bf ent\~ao} \\
 \>    \> \> elimine $v_i$; \\
 \>    \> \> fa\c ca as arestas que apontavam para $v_i$ apontar para $v_j$ \\
 \>    \> {\bf fimse}; \\
 \> 2. \>  {\bf se} dois nodos de r\a'otulo $v_i$ s\~ao ra\a'{\i}zes de sub-BDDs
                         id\^enticos {\bf ent\~ao} \\
 \>    \> \> elimine um deles; \\
 \>    \> \> fa\c ca as arestas que apontavam para ele apontar para o outro \\
 \>    \> {\bf fimse} \\
{\bf fimrepita}.
\end{tabbing}

\vspace*{1cm}
\noindent {\bf\Large Algoritmos para propridades de f\'ormulas:}

\begin{itemize}
 \item $A$ \'e {\bf satisfat\'{\i}vel} sse existe \framebox{V} no OBDD reduzido para $A$.
 \item $A$ \'e {\bf false\'avel} sse existe \framebox{F} no OBDD reduzido para $A$.
 \item $A$ \'e {\bf v\'alida} sse o OBDD reduzido para $A$ \'e \framebox{V}.
 \item $A$ \'e {\bf insatisfat\'{\i}vel} sse o OBDD reduzido para $A$ \'e \framebox{F}.
 \item $A\equiv B$ sse se os OBDDs reduzidos de $A$ e $B$ s\~ao id\^enticos.
\end{itemize}


\pagebreak
\noindent {\bf\Large Procedimento Apply:}

\vspace*{.5cm}
\begin{flushleft}
{\bf Entrada:} um operador booleano {\em op\/}, dois OBDDs, $\mbox{\em bdd}_1$ para
$A_1$ e $\mbox{\em bdd}_2$ para $A_2$, tais que a uni\~ao dos conjuntos de ordenamentos
dos \'atomos dos dois OBDDs \'e compat\'{\i}vel. \\
{\bf Sa\'{\i}da:} um OBDD para a f\'ormula $A_1 \,\mbox{\em op\/}\, A_2$.
\end{flushleft}

\vspace*{.3cm}
\begin{tabbing}
xxx\=xx\=xxx\=xxxxxx\= \kill
{\bf se} $\mbox{\em bdd}_1$ e $\mbox{\em bdd}_2$ s\~ao folhas de r\a'otulos $\nu_1$
              e $\nu_2$ {\bf ent\~ao} \\
 \> retorne uma folha de r\a'otulo $\nu_1 \,\mbox{\em op\/}\, \nu_2$ \\
{\bf sen\~aose} as ra\a'{\i}zes de $\mbox{\em bdd}_1$ e $\mbox{\em bdd}_2$
                s\~ao rotuladas com o mesmo \a'atomo $p$ {\bf ent\~ao} \\
 \> retorne o BDD de raiz rotulada com $p$, cujo sub-BDD \a`a esquerda \\
 \> \> (direita) \a'e obtido executando o algoritmo nos sub-BDDs \a`a esquerda \\
 \> \> (direita) de $\mbox{\em bdd}_1$ e $\mbox{\em bdd}_2$ \\
{\bf sen\~aose} a raiz de $\mbox{\em bdd}_i$ tem r\a'otulo $p_i$ para $i=1,2$ e $p_1<p_2$ {\bf ent\~ao} \\
 \> retorne o BDD com raiz rotulada com $p_1$, cujo sub-BDD \a`a esquerda \\
 \> \> (direita) \a'e obtido executando o algoritmo com $\mbox{\em bdd}_1$ e o sub-BDD \\
 \> \> \a`a esquerda (direita) de $\mbox{\em bdd}_2$; \\
 \> isto \a'e feito tamb\a'em se $\mbox{\em bdd}_2$ \a'e folha e $\mbox{\em bdd}_1$ n\~ao \a'e \\
{\bf sen\~ao} (tem-se o caso sim\a'etrico ao anterior)\\
 \> retorne o BDD com raiz rotulada com $p_2$, cujo sub-BDD \a`a esquerda \\
 \> \> (direita) \a'e obtido executando o algoritmo com o sub-BDD \\
 \> \> \a`a esquerda (direita) de $\mbox{\em bdd}_1$ e $\mbox{\em bdd}_2$ \\
{\bf fimse}; \\
\end{tabbing}

\pagebreak
\noindent {\bf\Large Procedimento Restrict:}

\vspace*{.5cm}
\begin{flushleft}
{\bf Entrada:} um OBDD {\em bdd\/} para uma f\'ormula $A$, um \'atomo $p$ que ocorre em $A$
 e um valor $\nu\in\{\mbox{V},\mbox{F}\}$. \\
{\bf Sa\'{\i}da:} um OBDD para $A|_{p=\nu}$.
\end{flushleft}

\vspace*{.3cm}
\begin{tabbing}
xx\=xxx\=xxx\=xxxxxx\= \kill
1. \>{\bf se} a raiz de \mbox{\em bdd\/} \a'e uma folha {\bf ent\~ao} \\
   \> \> retorne a folha \\
2. \>{\bf sen\~aose} a raiz de \mbox{\em bdd\/} \a'e rotulada com $p$ {\bf ent\~ao} \\
   \> \> retorne o sub-BDD falso ou verdadeiro, de acordo com $\nu$ \\
3. \>{\bf sen\~ao} (a raiz de \mbox{\em bdd\/} \a'e rotulada com $q\not=p$)\\
   \> \> retorne o BDD com raiz rotulada com $q$, cujo sub-BDD \a`a esquerda \\
 \> \> \a'e obtido executando o algoritmo com o sub-BDD \a`a esquerda de \mbox{\em bdd\/},\\
 \> \> e cujo sub-BDD \a`a direita \a'e obtido executando o algoritmo com o \\
 \> \> sub-BDD \a`a direita de \mbox{\em bdd\/}\\
 \>{\bf fimse}. \\
\end{tabbing}

\end{document}
