Dicas para a preparação de listas de exercícios da disciplina MAC0239 (Introdução à Lógica e Verificação de Programas) no IME-USP.
Tips for preparing exercises for MAC0239 (Introduction to Logic and Program Verification) at IME-USP.
\documentclass[a4paper]{article}
\usepackage[portuguese]{babel} % Permite escrever em português
\usepackage[utf8]{inputenc} % Permite digitar acentuações diretamente
\usepackage{amsmath} % Permite diagramação matemática avançada
\usepackage{parskip} % Remove identação de parágrafos e adiciona espaço entre eles
\usepackage[usenames,dvipsnames,table]{xcolor} % Permite usar cores
\usepackage{fancyvrb} % Desenha conteúdos verbatim com caixas ao redor
\PassOptionsToPackage{hyphens}{url}\usepackage{hyperref} % Permite adicionar url's clicáveis
% Configura a exibição de urls
\hypersetup{
colorlinks = true,
urlcolor = blue,
linkcolor = blue,
citecolor = red
}
\usepackage{logicproof} % PAra construir demonstrações lógicas
\usepackage{tikz} % Para construir árvores e BDDs
\usetikzlibrary{trees,positioning}
% ------------------------------------------------------------------------------------
% ------------------------------------------------------------------------------------
\title{Dicas para a preparação de relatórios em formato digital utilizando \LaTeX}
\author{MAC0239 -- Introdução à Lógica e Verificação de Programas}
\date{\small{criado por Luiz Carlos Vieira (outubro de 2015)}}
\begin{document}
\maketitle
\section{Introdução}
Você pode fazer seus relatórios em formato digital utilizando qualquer editor. Porém, há muitas vantagens em usar o \LaTeX~pra isso.
Primeriamente, você não precisa se preocupar com a formatação, pois o \LaTeX~faz isso sozinho pra você. Você apenas constrói o texto e usa marcadores (comandos) especiais para indicar o que de especial quer construir. Por exemplo, a notação matemática permite definir equações em um parágrafo separado usando dois cifrões (\verb!$$!) para abrir e fechar o ambiente da equação.
Por exemplo, o código a seguir:
\begin{verbatim}
$$
x = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}
$$
\end{verbatim}
Gera o seguinte resultado:
$$
x = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}
$$
Também se pode adicionar equações no meio do texto usando apenas um cifrão (\verb!$!) como delimitador. Por exemplo, a fórmula $a^2 = b^2 + c^2 - 2b \cdot c \cdot \cos{\theta}$ é produzida pelo código:\\
\verb!$a^2 = b^2 + c^2 - 2b \cdot c \cdot \cos{\theta}$!
No nosso caso, a notação matemática é utilizada para escrever as fórmulas lógicas estudadas. Alguns exemplos:
O código:
\begin{verbatim}
$$
\lnot p \to q
$$
\end{verbatim}
Gera o seguinte resultado:
$$
\lnot p \to q
$$
O código:
\begin{verbatim}
$$
\{ \phi_1, \phi_2, \dots, \phi_n \} \vdash \psi
$$
\end{verbatim}
Gera o seguinte resultado:
$$
\{ \phi_1, \phi_2, \dots, \phi_n \} \vdash \psi
$$
O código:
\begin{verbatim}
$$
\Delta \models \psi
$$
\end{verbatim}
Gera o seguinte resultado:
$$
\Delta \models \psi
$$
Há um pacote que estende muitíssimo as capacidades de representação matemática do \LaTeX~chamado ``amsmath''. Para utilizá-lo, inclua o comando \verb!\usepackage{amsmath}! no \href{http://edobay.50webs.com/latex/estrutura.html}{preâmbulo} do seu documento. Uma ajuda completa sobre a notação matemática (do pacote ``amsmath''), com os símbolos e seus respectivos comandos, está disponível neste guia (PDF em inglês): \url{ftp://ftp.ams.org/pub/tex/doc/amsmath/short-math-guide.pdf}.
Em segundo lugar, o \LaTeX~conta com um bom número de pacotes que facilitam enormemente a criação de provas de dedução natural, arvores sintáticas e diagramas de decisão binária. Esses serão explorados a seguir neste documento.
\subsection{Criando os documentos online com o Overleaf}
A ferramenta Overleaf (\url{https://www.overleaf.com}) é gratuita (com alguma limitação de espaço para os projetos) e permite criar os documentos online. É uma ótima alternativa, principalmente para trabalhos colaborativos (o link do projeto pode ser compatilhado). Mas, para quem preferir trabalhar off-line, basta fazer o download do \LaTeX~para o sistema operacional de sua preferência em \url{http://latex-project.org/ftp.html}.
O código deste documento também está acessível no Overleaf, neste link:\\
\url{https://www.overleaf.com/read/prbcswrntmtt}.
\subsection{Material de apoio sobre o \LaTeX}
A lista a seguir reune algumas fontes que podem ser utilizadas para aprender mais sobre o \LaTeX:
\begin{itemize}
\item Tutorial de \LaTeX~para escrita científica: \url{http://sbi.iqsc.usp.br/files/Manual-SBI_LATEX_2013-.pdf}
\item Introdução ao \LaTeX: \url{http://www.mat.ufmg.br/~regi/topicos/intlat.pdf}
\item \LaTeX~wikibooks (em inglês): \url{https://en.wikibooks.org/wiki/LaTeX}
\item \LaTeX~for logicians (em inglês): \url{http://www.logicmatters.net/latex-for-logicians/}
\item TextStudio (editor multiplataforma popular): \url{http://www.texstudio.org/}
\end{itemize}
\pagebreak % força uma quebra de página aqui
%======================================================
\section{Criando o Processo de Inferência}
Usando apenas a notação matemática do \LaTeX~é possível construir fórmulas da lógica proposicional. Mas pode ser muito útil usar também o pacote de macros ``logicproof'' (inclua o comando \verb!\usepackage{logicproof}! no preâmbulo do documento), que permite fazer processos de dedução no mesmo estilo apresentado em sala de aula (com endentações e quadros).
Esse pacote pode já estar disponível na sua instalação do \LaTeX, mas caso não esteja ele pode ser baixado daqui: \url{http://www.ctan.org/tex-archive/macros/latex/contrib/logicproof}. A documentação pode ser encontrada aqui (em inglês): \url{http://repositorios.cpai.unb.br/ctan/macros/latex/contrib/logicproof/logicproof.pdf}.
\subsection{Exemplos utilizando o pacote ``logicproof''}
\subsubsection{Exemplo 1}
% O ~ no código abaixo apenas força um espaço em branco
Prove a validade do argumento: $p \land q \to r ~ \vdash ~ p \to ( q \to r )$
Detalhamento da prova utilizando o pacote ``logicproof'':
\begin{logicproof}{2}
p \land q \to r & premissa\\
\begin{subproof}
p & hipótese\\
\begin{subproof}
q & hipótese\\
p \land q & $\land_i (2) (3)$\\
r & $\to_e (1) (4)$
\end{subproof}
q \to r & $\to_i (3-5)$
\end{subproof}
p \to (q \to r) & $\to_i (2-6)$
\end{logicproof}
Abaixo se encontra o código utilizado para criar essa prova:
\begin{Verbatim}[frame=single]
\begin{logicproof}{2}
p \land q \to r & premissa\\
\begin{subproof}
p & hipótese\\
\begin{subproof}
q & hipótese\\
p \land q & $\land_i (2) (3)$\\
r & $\to_e (1) (4)$
\end{subproof}
q \to r & $\to_i (3-5)$
\end{subproof}
p \to (q \to r) & $\to_i (2-6)$
\end{logicproof}
\end{Verbatim}
Nesse código, as linhas são construídas utilizando um \& para separar a expressão lógica do texto da justificativa, assim:
\verb!<expressão> & <justificativa>!
E cada quadro é construído com um ou mais blocos \textit{subproof} aninhados, assim:
\begin{Verbatim}
\begin{subproof}
<expressão> & <justificativa>\\
\begin{subproof}
<expressão> & <justificativa>\\
<expressão> & <justificativa>
\end{subproof}
<expressão> & <justificativa>\\
<expressão> & <justificativa>
\end{subproof}
\end{Verbatim}
Observações importantes:
\begin{itemize}
\item O número $2$ na linha com o comando \verb!\begin{logicproof}{2}! é o número máximo de quadros (\textit{subproofs}) aninhados. Mude esse número se necessário, sempre de acordo com o número de quadros aninhados na prova que quer representar.
\item O comando \verb!\\!, que indica uma quebra de linha forçada, não deve ser utilizado na última linha de um bloco \textit{subproof}.
\item O comando \verb!\begin{logicproof}! não precisa estar dentro de um ambiente matemático (isto é, entre \$\$ e \$\$), pois ele já cria um ambiente matemático automaticamente. Porém, a justificativa em uma linha é texto puro! Então, se precisar usar símbolos matemáticos nela (como neste exemplo), escreva entre \$ e \$ (ambiente matemático na linha).
\item Note o uso do \textit{underline} (\_) para fazer subscritos (o comando matemático para fazer sobrescritos é o acento circunflexo: \verb!^!). A notação matemática utiliza o próximo símbolo ao \textit{underline}, então \verb!$\land_i$! resulta em $\land_i$. Para evitar confusão, quando precisar utilizar mais símbolos dentro de um subscrito (ou fazer subscritos aninhados), use chaves (\{ e \}) para delimitar o conteúdo. Exemplo: \verb!$\lor_i2$! resulta em $\lor_i2$ (só o $i$ foi considerado no subscrito); \verb!$\lor_i_2$! resulta em erro de compilação (\textit{double subscript}), e \verb!$\lor_{i_2}$! resulta em $\lor_{i_2}$ (o que é a notação intencionada).
\end{itemize}
\pagebreak % força uma quebra de página
\subsubsection{Exemplo 2}
Prove a validade do argumento: $\vdash ~ (q \to r) \to ((\lnot q \to \lnot p) \to (p \to r))$
Detalhamento da prova utilizando o pacote ``\textit{logicproof}'':
\begin{logicproof}{3}
\begin{subproof}
q \to r & hipótese\\
\begin{subproof}
\lnot q \to \lnot p & hipótese\\
\begin{subproof}
p & hipótese\\
\lnot\lnot p & $\lnot\lnot_i (3)$\\
\lnot\lnot q & $MT (2) (4)$\\
q & $\lnot\lnot_e (5)$\\
r & $\to_e (1) (6)$
\end{subproof}
p \to r & $\to_i (3-7)$
\end{subproof}
(\lnot q \to \lnot p) \to (p \to r) & $\to_i (2-8)$
\end{subproof}
(q \to r) \to ((\lnot q \to \lnot p) \to (p \to r)) & $\to_i (1-9)$
\end{logicproof}
Código dessa prova:
\begin{Verbatim}[frame=single]
\begin{logicproof}{3}
\begin{subproof}
q \to r & hipótese\\
\begin{subproof}
\lnot q \to \lnot p & hipótese\\
\begin{subproof}
p & hipótese\\
\lnot\lnot p & $\lnot\lnot_i (3)$\\
\lnot\lnot q & $MT (2) (4)$\\
q & $\lnot\lnot_e (5)$\\
r & $\to_e (1) (6)$
\end{subproof}
p \to r & $\to_i (3-7)$
\end{subproof}
(\lnot q \to \lnot p) \to (p \to r) & $\to_i (2-8)$
\end{subproof}
(q \to r) \to ((\lnot q \to \lnot p) \to (p \to r)) &
$\to_i (1-9)$
\end{logicproof}
\end{Verbatim}
%======================================================
\pagebreak
\section{Criando árvores e diagramas de decisão binária}
O ``TikZ'' é um dos pacotes mais poderosos do \LaTeX, pois permite criar gráficos, figuras e diagramas de todo o tipo. O guia \href{http://cremeronline.com/LaTeX/minimaltikz.pdf}{``A very minimal introduction to TikZ''} (em inglês) serve como uma ótima introdução para quem desejar explorar esse ótimo pacote mais a fundo. Há também este \href{http://www.texample.net/tikz/examples/}{outro site} com inúmeros exemplos, incluindo desde grafos e mapas meitais a calendários e tablaturas musicais. O pacote também já deve estar disponível na sua instalação do \LaTeX, mas pode ser baixado daqui: \url{https://www.ctan.org/pkg/pgf}.
Os exemplos desse documento utilizam configurações específicas (árvores e posicionamento de nós), então a declaração no preâmbulo é feita assim:
\begin{Verbatim}
\usepackage{tikz}
\usetikzlibrary{trees,positioning}
\end{Verbatim}
\subsection{Exemplos utilizando o pacote ``TikZ''}
\subsubsection{Exemplo 1 - Árvore Sintática}
Considere a função $\phi \equiv (p \land r) \lor (\lnot{p} \land q \land r)$. Sua árvore sintática é a seguinte:
\begin{figure}[h!]
\centering
\begin{tikzpicture}[sibling distance=6em, scale=0.7,
every node/.style = {draw=none, align=center}
]
\node {$\lor$}
child { node[xshift=-1em] {$\land$}
child { node {$p$} }
child { node {$r$} }
}
child { node[xshift=1em] {$\land$}
child { node {$\lnot$}
child { node {$p$} }
}
child { node {$\land$}
child { node {$q$} }
child { node {$r$} }
}
};
\end{tikzpicture}
\caption{Árvore sintática de $\phi \equiv (p \land r) \lor (\lnot{p} \land q \land r)$}
\end{figure}
O código para a construção dessa árvore utiliza um bloco \verb!tikzpicture! para desenho, e vários blocos do tipo \verb!node! (para desenhar um nó da árvore) e do tipo \verb!child! (para estabelecer a relação hierárquica em árvores). O bloco \verb!tikzpicture! recebe também alguns parâmetros que permitem configurar a distância entre os nós em um mesmo nível (\textit{siblings}), a escala do desenho, e detalhes do estilo de desenho geral dos nós (configuração \verb!every node!).
Usando os comandos \verb!node! e \verb!child! faz com que o próprio pacote organize os nós em uma estrutura de árvore pra você. Entretanto, alguns nós podem acabar sobrepostos, o que pode ser configurado ajustando a distância entre os nós de mesmo nível (parâmetro \verb!sibling distance!) ou simplesmente movendo um nó no eixo $x$ com o parâmetro \verb!xshift! no próprio nó (há também o \verb!yshift!) para forçar posicionamento de um nó no eixo $y$).
Observe que o texto de um nó (colocado entre \{ e \}) também pode ser formatado em notação matemática utilizando \$ e \$. O código da árvore sintática apresentada anteriormente é o seguinte:
\begin{Verbatim}[frame=single]
\begin{figure}[h!]
\centering
\begin{tikzpicture}[sibling distance=6em, scale=0.7,
every node/.style = {
draw=none, align=center
}
]
\node {$\lor$}
child { node[xshift=-1em] {$\land$}
child { node {$p$} }
child { node {$r$} }
}
child { node[xshift=1em] {$\land$}
child { node {$\lnot$}
child { node {$p$} }
}
child { node {$\land$}
child { node {$q$} }
child { node {$r$} }
}
};
\end{tikzpicture}
\caption{Árvore sintática de $\phi \equiv (p \land r) \lor
(\lnot{p} \land q \land r)$}
\end{figure}
\end{Verbatim}
Para detalhes sobre os elementos da linguagem, por favor consulte a documentação do pacote.
\pagebreak
\subsubsection{Exemplo 2 - Árvore de Decisão Binária}
Os nós e arestas nos BDDs precisam de estilos customizados para definir a aresta trecejada como ``lo'' (de \textit{low}) e a aresta sólida como ``hi'' (de \textit{high}). Essa definição de estilos pode ser reutilizada por todos os diagramas com o comando \verb!tikzset!, sendo definida da seguinte forma:
\begin{Verbatim}[frame=single]
% Configuração geral de estilos para o desenho de ROBDDs
\tikzset{%
% Estilo para nós de decisão
decision/.style={shape=circle, draw, solid, align=center},
% Estilo para nós terminais
terminal/.style={shape=rectangle, draw, solid,
align=center, scale=0.7},
% Estilo para a linha tracejada (low) reta
lo/.style={edge from parent/.style={dashed,draw}},
% Estilo para a linha tracejada (low) encurvada
lo-bend/.style={dashed, bend right=15,
edge from parent path={
(\tikzparentnode\tikzparentanchor)
edge [dashed, draw, bend right=15]
(\tikzchildnode\tikzchildanchor)
}
},
% Estilo para a linha solida (high) reta
hi/.style={edge from parent/.style={solid,draw}},
% Estilo para a linha solida (high) encurvada
hi-bend/.style={solid, bend left=15,
edge from parent path={
(\tikzparentnode\tikzparentanchor)
edge [solid, draw, bend left=15]
(\tikzchildnode\tikzchildanchor)
}
}
}
\end{Verbatim}
Os nomes dos estilos estão antes de \verb!/.style! e os parâmetros internos são os mesmos já utilizados na árvore sintática ou alguns novos (para encurvar uma linha -- \verb!bend left=15! -- ou para fazer o nó ter um formato circular -- \verb!shape=circle!). Novamente, para detalhes sobre cada parâmetro, por favor consulte a documentação do pacote.
\tikzset{%
% Estilo para nós de decisão
decision/.style={shape=circle, draw, solid, align=center},
% Estilo para nós terminais
terminal/.style={shape=rectangle, draw, solid,
align=center, scale=0.7},
% Estilo para a linha tracejada (low) reta
lo/.style={edge from parent/.style={dashed,draw}},
% Estilo para a linha tracejada (low) encurvada
lo-bend/.style={dashed, bend right=15,
edge from parent path={
(\tikzparentnode\tikzparentanchor)
edge [dashed, draw, bend right=15]
(\tikzchildnode\tikzchildanchor)
}
},
% Estilo para a linha solida (high) reta
hi/.style={edge from parent/.style={solid,draw}},
% Estilo para a linha solida (high) encurvada
hi-bend/.style={solid, bend left=15,
edge from parent path={
(\tikzparentnode\tikzparentanchor)
edge [solid, draw, bend left=15]
(\tikzchildnode\tikzchildanchor)
}
}
}
\pagebreak
Este exemplo reutiliza a mesma função $\phi \equiv (p \land r) \lor (\lnot{p} \land q \land r)$ do exemplo anterior. A árvore de decisão binária criada para ele é a seguinte:
\begin{figure}[h!]
\centering
\begin{tikzpicture}[sibling distance=6em, scale=1.0]
\node[decision] {$p$}
child[lo, xshift=-5em] { node[decision] {$q$}
child[lo, xshift=-1em] { node[decision] {$r$}
child[lo] { node[terminal] {$0$}}
child[hi] { node[terminal] {$0$} }
}
child[hi, xshift=1em] { node[decision] {$r$}
child[lo] { node[terminal] {$0$}}
child[hi] { node[terminal] {$1$} }
}
}
child[hi, xshift=5em] { node[decision] {$q$}
child[lo, xshift=-1em] { node[decision] {$r$}
child[lo] { node[terminal] {$0$}}
child[hi] { node[terminal] {$1$} }
}
child[hi, xshift=1em] { node[decision] {$r$}
child[lo] { node[terminal] {$0$}}
child[hi] { node[terminal] {$1$} }
}
};
\end{tikzpicture}
\caption{Árvore de decisão binária para $\phi \equiv (p \land r) \lor (\lnot{p} \land q \land r)$}
\end{figure}
Apenas para mérito de comparação, essa é a tabela-verdade de $\phi$ -- observe como a árvore de decisão tem exatamente as mesmas combinações de valorações para as variáveis, tanto que a sequência de nós terminais (da esquerda para a direita) e a mesma da valoração da fórmula (última coluna, de cima pra baixo):
\begin{table}[h!]
\setlength{\tabcolsep}{4pt}
\definecolor{LightCyan}{rgb}{0.88,1,1}
\rowcolors{1}{}{LightCyan}
\caption{Tabela-verdade de $\phi \equiv (p \land r) \lor (\lnot{p} \land q \land r)$}
\begin{tabular}{c|c|c|c|c|c||c}
$\pmb{p}$ & $\pmb{q}$ & $\pmb{r}$ & $\pmb{\lnot{p}}$ & $\pmb{p \land r}$ & $\pmb{\lnot{p} \land q \land r}$ & $\pmb{(p \land r) \lor (\lnot{p} \land q \land r)}$\\
\hline
$0$ & $0$ & $0$ & $1$ & $0$ & $0$ & $0$\\
$0$ & $0$ & $1$ & $1$ & $0$ & $0$ & $0$\\
$0$ & $1$ & $0$ & $1$ & $0$ & $0$ & $0$\\
$0$ & $1$ & $1$ & $1$ & $0$ & $1$ & $1$\\
$1$ & $0$ & $0$ & $0$ & $0$ & $0$ & $0$\\
$1$ & $0$ & $1$ & $0$ & $1$ & $0$ & $1$\\
$1$ & $1$ & $0$ & $0$ & $0$ & $0$ & $0$\\
$1$ & $1$ & $1$ & $0$ & $1$ & $0$ & $1$\\
\end{tabular}
\end{table}
O código para a criação dessa árvore é apresentado a seguir. Observe alguns detalhes:
\begin{itemize}
\item Os nós (\verb!node!) e as arestas (\verb!child!) utilizam os estilos definidos anteriormente (``decision'' e ``terminal'' para os nós, e ``lo'' e ``hi'' para as arestas).
\item Os nós do segundo nível são afastados (para a esquerda e para a direita, usando valores negativo e positivo no comando \verb!xshift!) para deixar o aspecto visual mais agradável.
\item O texto dos nós é definido utilizando a notação matemática (\verb!$ <conteúdo> $!), para deixar condizente com as mesmas fontes usadas na criação das fórmulas.
\item O bloco \verb!figure! não é do pacote ``TikZ'', e sim do \LaTeX. Ele permite colocar a figura em um \href{https://en.wikibooks.org/wiki/LaTeX/Floats,_Figures_and_Captions}{\textit{floater}} (uma caixa que flutua junto com o texto, utilizada justamente para exibir figuras). Note que o bloco \verb!tikzpicture! é colocado dentro do bloco \verb!figure!. Para detalhes, consulte a documentação do \LaTeX.
\end{itemize}
Eis o código para criação da árvore:
\begin{Verbatim}[frame=single]
\begin{figure}[h!]
\centering
\begin{tikzpicture}[sibling distance=6em, scale=1.0]
\node[decision] {$p$}
child[lo, xshift=-5em] { node[decision] {$q$}
child[lo, xshift=-1em] { node[decision] {$r$}
child[lo] { node[terminal] {$0$}}
child[hi] { node[terminal] {$0$} }
}
child[hi, xshift=1em] { node[decision] {$r$}
child[lo] { node[terminal] {$0$}}
child[hi] { node[terminal] {$1$} }
}
}
child[hi, xshift=5em] { node[decision] {$q$}
child[lo, xshift=-1em] { node[decision] {$r$}
child[lo] { node[terminal] {$0$}}
child[hi] { node[terminal] {$1$} }
}
child[hi, xshift=1em] { node[decision] {$r$}
child[lo] { node[terminal] {$0$}}
child[hi] { node[terminal] {$1$} }
}
};
\end{tikzpicture}
\caption{Árvore de decisão binária para $\phi \equiv
(p \land r) \lor (\lnot{p} \land q \land r)$}
\end{figure}
\end{Verbatim}
\pagebreak
\subsubsection{Exemplo 3 - Diagrama de Decisão Binária}
Se as simplificações C1-C3 forem efetuadas sobre a árvore do exemplo anterior, o seguinte diagrama de decisão binária (de ordem $[p, q, r]$ e reduzido) será obtido:
\begin{figure}[h!]
\centering
\begin{tikzpicture}[sibling distance=6em, scale=1.0]
\node[decision](p) {$p$}
child[lo, xshift=-3em] { node[decision](q) {$q$}
child[hi, xshift=3em] { node[decision](r) {$r$}
child[lo] { node[terminal](0) {$0$} }
child[hi] { node[terminal](1) {$1$} }
}
};
\draw[hi-bend] (p) to (r);
\draw[lo-bend] (q) to (0);
\end{tikzpicture}
\caption{ROBDD para $\phi \equiv (p \land r) \lor (\lnot{p} \land q \land r)$}
\end{figure}
O código para a criação desse diagrama é o seguinte:
\begin{Verbatim}[frame=single]
\begin{figure}[h!]
\centering
\begin{tikzpicture}[sibling distance=6em, scale=1.0]
\node[decision](p) {$p$}
child[lo, xshift=-3em] { node[decision](q) {$q$}
child[hi, xshift=3em] { node[decision](r) {$r$}
child[lo] { node[terminal](0) {$0$} }
child[hi] { node[terminal](1) {$1$} }
}
};
\draw[hi-bend] (p) to (r);
\draw[lo-bend] (q) to (0);
\end{tikzpicture}
\caption{ROBDD para $\phi \equiv (p \land r) \lor
(\lnot{p} \land q \land r)$}
\end{figure}
\end{Verbatim}
Observe que como esse diagrama não é mais uma árvore e sim um grafo, há a necessidade de fazer ligações entre nós \textit{que não são filhos}. Por exemplo, o nó $p$ agora tem uma ligação direta com o nó $r$ (que na verdade é filho de $q$). Essas ligações diretas são efetuadas com o comando \verb!draw!. Ele também permite utilizar os mesmos estilos já criados (e no exemplo usamos as arestas curvas apenas para dar um visual bacana ao diagrama). Observe também que ser possível ligar os nós, eles precisam ser \textit{nomeados}. Isso é feito nomeando os nós. Por exemplo, no código \verb!child[lo] { node[terminal]!\textcolor{red}{(0)}\verb! {$0$} }! o $0$ entre parênteses (em vermelho) é o nome desse nó terminal, utilizado para fazer a conexão com o nó $q$ no código: \verb!\draw[lo-bend] (q) to (0);!.
\end{document}