\section{Ordered Symbolic Derivation Diagrams}
\label{sec:osdd}

\myparagraph{PRISM.}  Programs in PRISM follow Prolog's syntax, as illustrated in Figs.~\ref{fig:intro-ex-palindrome} and~\ref{fig:intro-ex-birthday}. 
In a PRISM program, the \texttt{msw} relation (``multi-valued switch'')
has a special meaning: \texttt{msw(X,I,V)} says that \texttt{V} is the
outcome of the \texttt{I}-th instance from a family \texttt{X} of
random processes. The set of variables
$\{\mathtt{V}_i \mid \mathtt{msw(}p, i, \mathtt{V}_i\mathtt{)}\}$ are
i.i.d. for a given random process $p$.

The distribution parameters of the random variables are specified
separately.

% \comment{
% The program in Fig.~\ref{fig:hmm-prism} encodes a Hidden Markov Model
% (HMM) in PRISM. 
% % 
% \begin{wrapfigure}{r}{0.48\textwidth}
%   \vspace{-5pt}
%   \begin{center}
%     \includegraphics[width=0.39\textwidth]{hmm}
%   \end{center}
%   \caption{PRISM program for an HMM}
%   \label{fig:hmm-prism}
%   \vspace{-5pt}
% \end{wrapfigure}
% % 
% The set of observations is encoded as facts of predicate \texttt{obs},
% where \texttt{obs(I,V)} means that value \texttt{V} was observed at
% time \texttt{I}.  In the figure, the clause defining \texttt{hmm} says
% that \texttt{T} is the \texttt{N}-th state if we traverse the HMM
% starting at an initial state \texttt{S} (itself the outcome of the
% random process \texttt{init}).  In \texttt{hmm\_part(I, N, S, T)},
% \texttt{S} is the \texttt{I}-th state, \texttt{T} is the \texttt{N}-th
% state. The first clause of \texttt{hmm\_part} defines the conditions
% under which we go from the \texttt{I}-th state \texttt{S} to the
% \texttt{I+1}-th state \texttt{NextS}.  Random processes
% \texttt{trans(S)} and \texttt{emit(S)} give the distributions of
% transitions and emissions, respectively, from state \texttt{S}.
% }

The meaning of a PRISM program is given in terms of a
\emph{distribution semantics}~\cite{sato1997prism,sato2001parameter}.
A PRISM program is treated as a non-probabilistic logic program over a
set of probabilistic facts, i.e. the \texttt{msw} relation.  An instance of
the \texttt{msw} relation defines one choice of values of all random
variables.  A negation-free PRISM program is associated with a set of least models,
one for each \texttt{msw} relation instance.  A probability
distribution is then defined over the set of models, based on the
probability distribution of the \texttt{msw} relation instances.  This
distribution of least models is the semantics of a PRISM program.  Note that the
distribution semantics is declarative.  For a subclass of programs,
PRISM has an efficient procedure for computing this semantics based on
OLDT resolution~\cite{tamaki1986old}.
	
Inference in PRISM proceeds as follows.  When the goal selected at a
step is of the form \texttt{msw(X,I,Y)}, then \texttt{Y} is bound to a
possible outcome of a random process \texttt{X}.  \emph{Thus in PRISM,
  derivations are constructed by enumerating the possible outcomes of
  each random variable.}  The derivation step is associated with the
probability of this outcome.  If all random processes encountered in a
derivation are independent, then the probability of the derivation is
the product of probabilities of each step in the derivation.  If a set
of derivations are pairwise mutually exclusive, the probability of the
set is the sum of probabilities of each derivation in the set.
PRISM's evaluation procedure is defined only when the independence and
exclusiveness assumptions hold.  Finally, the probability of an answer
is the probability of the set of derivations of that answer.


\myparagraph{Notation.} We assume familiarity with common logic
programming terminology such as variables, terms, substitutions,
predicates and clauses. We use Prolog's convention, using identifiers
beginning with lower case letters to denote atomic constants or
function symbols, and those beginning with upper case letters to
denote variables.  We often use specific symbols such as $t$ to denote
ground terms, and $i,j,k$ to denote integer indices.  We assume an
arbitrary but fixed ordering "$\prec$" among variables and ground
terms.

A \textbf{\emph{type}} is a finite collection of ground terms.  In
this paper, types represent the space of outcomes of switches or
random processes.  For example in Palindrome example of Fig.~\ref{fig:intro-ex-palindrome}, the set of values $\{a,b\}$ is a type.
%
A variable $Y$ referring to the outcome of a switch $s$ is a typed
variable; its type, denoted $type(Y)$, is deemed to be the same as the
space of outcomes of $s$. The type of a ground term $t$ can be any of
the sets it is an element of.

\begin{Def}[Atomic Constraint]
  An atomic constraint, denoted $\beta$, is of the form $\{X=T\}$ or
  $\{X \neq T\}$, where $X$ is a variable and $T$ is a variable or a
  ground term of the same type as $X$.
\end{Def}

A set of atomic constraints representing their conjunction is called a
\textbf{\emph{constraint formula}}. Constraint formulas are denoted by
symbols $\gamma$ and $\phi$. Note that atomic constraints are closed
under negation, while constraint formulas are not. The set of
variables in a constraint formula $\gamma$ are denoted by
$Vars(\gamma)$.

\begin{Def}[Constraint Graph]
  \label{def:constraint-graph}
  The constraint graph for a constraint formula $\gamma$ is labeled
  undirected graph, whose nodes are variables and ground terms in
  $\gamma$.  Edges are labeled with ``$=$" and ``$\not=$" such that
  \begin{itemize}
  \item $T_1$ and $T_2$ are connected by an edge labeled ``$=$" if, and
    only if, $T_1 = T_2$ is entailed by $\gamma$.
  \item $T_1$ and $T_2$ are connected by an edge labeled ``$\not=$" if,
    and only if, $T_1 \not = T_2$ is entailed by $\gamma$, and at
    least one of $T_1, T_2$ is a variable.
   \end{itemize}
\end{Def}
Note that a constraint graph may have edges between two terms even
when there is no explicit constraint on the two terms in $\gamma$.

\begin{Def}[Ordering]
  \label{def:ordering}
  Based on an (arbitrary but fixed) total order, ``$\prec$'', among ground terms, we
  define an ordering on ground switch instance pairs $(s,i)$ and
  $(s',i')$ as follows:
  \begin{itemize}
  \item If $i \prec i'$ then
    $(s,i) \prec (s',i')$ for all ground terms $s$ and  $s'$.
  \item If $i=i' \land s \prec s'$ then
    $(s,i) \prec (s',i')$.
  \item If $i=i' \land s=s'$ then $(s,i)=(s',i')$.
  \end{itemize}
\end{Def}

\myparagraph{Canonical representation of constraint formulas.}  A
constraint formula is represented by its constraint graph which in
turn can be represented as a set of triples
$(source, destination, constraint)$ each of which represents an edge
in the constraint graph.  Recall that variables and ground terms can
be compared using total order $\prec$.  Assuming an order between the
two symbols ``$=$" and ``$\not=$", we can define a lexicographic order
over each edge triple, and consequently order the elements of the edge
set.  The sequence of edge triples following the above order is a
canonical representation of a constraint formula.  Using this
representation, we can define a total order, called the
\emph{canonical order}, among constraint formulas themselves given by
the lexicographic ordering defined over the edge sequences.

Given any constraint formula
$\gamma = \{\beta_1, \beta_2, \ldots, \beta_n\}$, its negation
$\neg \gamma$ is given by a set of constraint formulas
$\neg \gamma = \{\{\neg \beta_1\}, \{\beta_1,\neg \beta_2\}, \ldots,
\{\beta_1, \beta_2, \ldots, \beta_{n-1}, \neg \beta_n\}\}$.  The above
defines negation of a formula to be a set of constraint formulas which
are pairwise mutually exclusive and together represent the
negation.

The set of solutions of a constraint formula $\gamma$ is denoted
$\sem{\gamma}$ and their projection onto a variable
$X \in Vars(\gamma)$ is denoted $\sem{\gamma}_X$. The constraint
formula is unsatisfiable if $\sem{\gamma}=\emptyset$, and satisfiable
otherwise.  Note that substitutions can also be viewed as constraint
formulas.

% Two constraint formulas $\gamma$ and $\phi$ are said to be
% compatible if their conjunction is satisfiable (denoted
% $\gamma \nparallel \phi$).

\comment{
\myparagraph{PRISM.}  We briefly recall the syntax and semantics of
PRISM programs (see Appendix A for a more detailed overview).  PRISM
programs have Prolog-like syntax.  In a PRISM program the \texttt{msw}
relation (``multi-valued switch'') has a special meaning:
\texttt{msw(X,I,V)} says that \texttt{V} is the outcome of the
\texttt{I}-th instance from a family \texttt{X} of random processes
also called as \emph{switches}.  The set of variables
$\{\mathtt{V}_i \mid \mathtt{msw(}p, i, \mathtt{V}_i\mathtt{)}\}$ are
i.i.d. for a given random process $p$.  Note that the ternary
\texttt{msw} is used in the definition of the PRISM
language~\cite{sato2001parameter} but the PRISM system uses a binary
\texttt{msw} by omitting the instance parameter.

The meaning of a PRISM program is given in terms of a
\emph{distribution semantics}~\cite{sato1997prism,sato2001parameter}.
Inference in the PRISM system computes the semantics for a subset of
PRISM programs as an extension of tabled evaluation.  When the goal
selected at a step is of the form \texttt{msw(X,I,Y)}, then \texttt{Y}
is bound to a possible outcome of a random process \texttt{X}.
\emph{Thus in PRISM, derivations are constructed by enumerating the
  possible outcomes of each random variable.}  The derivation step is
associated with the probability of this outcome.  Under independence
and mutual exclusion assumptions, the probabilities can be computed
without materializing the derivations.
}


\myparagraph{OSDD.} We use OSDDs to materialize derivations in a
compact manner.  OSDDs share a number of features with Binary Decision
Diagrams (BDDs)~\cite{BDD} and Multivalued Decision Diagrams
(MDDs)~\cite{MDDs}.  BDDs are directed acyclic graphs representing
propositional boolean formulas, with leaves labeled from $\{0,1\}$ and
internal nodes labeled with propositions.  In a BDD, each node has two
outgoing edges labeled $0$ and $1$, representing a true and false
valuation, respectively, for the node's proposition.  An MDD
generalizes a BDD where internal nodes are labeled with finite-domain
variables, and the outgoing edges are labeled with the possible
valuations of that variable.  In an OSDD, internal nodes represent
switches, and the outgoing edges are labeled with constraints
on the outcomes of that node's switch.

\begin{Def}[Ordered Symbolic Derivation Diagram]
  \label{def:osdd}
  An ordered symbolic derivation diagram over a set of typed variables
  $V$ is a tree, where leaves are labeled from the set $\{0,1\}$ and
  internal nodes are labeled by triples of the form $(s, k, Y)$, where
  $s$ and $k$ are switch and instance respectively and $Y \in V$. We
  call $Y$ the output variable of the node.  The edges are labeled by
  constraint formulas over $V$.  We represent OSDDs by textual
  patterns $(s,k,Y)[\gamma_i:\psi_i]$ where $(s,k,Y)$ is the label of
  the root, and each sub-OSDD $\psi_i$ is connected to the root by an
  edge labeled $\gamma_i$.  OSDDs satisfy the following conditions:
  \begin{enumerate}
  \item{\textbf{Ordering:}} For internal nodes $n = (s,k,Y)$ and
    $n'= (s',k',Y')$, if $n$ is the parent of $n'$, then
    $(s,k)\prec(s',k')$. The edges are ordered by using the canonical
    ordering of the constraint formulas labeling them.
  \item{\textbf{Mutual Exclusion:}} The constraints labeling the
    outgoing edges from an internal node are pairwise mutually
    exclusive (i.e., $\forall i, j$ such that $i\not=j$, 
    $\sem{\gamma_i \land \gamma_j} = \emptyset$).
  \item{\textbf{Completeness:}} Let $(s, k, Y)[\gamma_i : \psi_i]$ be
    a sub-OSDD and let $\sigma$ be any substitution that satisfies all
    constraints on the path from root to the given sub-OSDD such that
    $\sigma(Y) \in \id{type}(Y)$.  Then there is an $i$ such that
    $\sigma$ satisfies $\gamma_i$.
  \item{\textbf{Urgency:}} Let $\mathcal{O}(n)$ be the set of output
    variables in the path from the root to node $n$ (including
    $n$). Then for every constraint formula $\gamma_i$ labeling an
    outgoing edge from $n$, it holds that
    $Vars(\gamma_i) \subseteq \mathcal{O}(n)$ and for every ancestor
    $n'$ of $n$, $Vars(\gamma_i) \not \subseteq \mathcal{O}(n')$.
  \item{\textbf{Explicit Constraints:}} If constraint formula
    $\gamma_i$ out of a node $n$ entails an implicit atomic constraint
    $\beta$ on variables in $\mathcal{O}(n)$, then $\beta$ occurs
    explicitly in the path from root to $n$.  A consequence of this
    condition is that, for every path, the conjunction of constraint formulas labeling
    edges in the path will be satisfiable.
  \end{enumerate}
\end{Def}
A tree which satisfies all conditions of an OSDD \emph{except}
conditions 4 and 5 is called an \emph{improper OSDD}.

\begin{Ex}[OSDD properties]
  We illustrate the definiton by using the OSDD shown in
  Fig. \ref{fig:osdd-intro-ex}(b). The OSDD is represented by the
  textual pattern $(b,1,X1)[\emptyset : \psi_1]$ where $\psi_1$ is the
  sub-tree rooted at the node labeled \texttt{msw(b,2,X2)}. This sub-tree, in turn, can
  be represented by the textual pattern
  $(b,2,X2)[\{X1=X2\}: 1, \{X1\neq X2\} : \psi_2]$ where $\psi_2$ is
  the sub-tree rooted at the node \texttt{msw(b,3,X3)}, and so on.  The
  internal nodes satisfy the total ordering based on the instances.  All outgoing edges from an internal node are pairwise
  mutually exclusive. For instance, for the outgoing edges of the node
  labeled \texttt{msw(b, 3, X3)}, $X1=X3$ is mutually exclusive w.r.t.
  $X1\neq X3, X2=X3$ and $X1\neq X3, X2 \neq X3$. Similarly,
  $X1\neq X3, X2=X3$ is mutually exclusive to $X1\neq X3, X2 \neq
  X3$. Consider the sub-OSDD rooted at \texttt{msw(b, 2, X2)} any
  substitution that grounds $X1, X2$ satisfies the (empty) constraints
  on the path from the root to that subtree. Further any such
  substitution will satisfy exactly one of the edge constraints
  $X1=X2$ or $X1\neq X2$. It is obvious from the example that urgency
  is satisfied. Finally consider the constraint formula
  $X1\neq X3, X2=X3$. This entails the implicit constraint
  $X1\neq X2$. However, this constraint is explicitly found in the
  path from the root to that subtree. Therefore the OSDD in
  Fig. \ref{fig:osdd-intro-ex}(b) is a proper OSDD.
\end{Ex}


OSDDs can be viewed as representing a set of explanations or
derivations where a node of the form $(s, k, Y)$ \emph{binds} $Y$.
This observation leads to the definition of bound and free variables:

\begin{Def}[Bound and Free variables]
  Given an OSDD $\psi=(s,k,Y)[\gamma_i :\psi_i]$ the bound variables
  of $\psi$, denoted $BV(\psi)$, are the output variables in $\psi$.
  The free variables of $\psi$, denoted $FV(\psi)$, are those
  variables which are not bound.
\end{Def}

Each OSDD corresponds to an MDD which can be constructed as follows. 

\begin{Def}[Grounding]\label{def:grounding}
  Given an OSDD $\psi=(s,k,Y)[\gamma_i:\psi_i]$, the MDD corresponding
  to it is denoted $\mathcal{G}(\psi)$ and is recursively defined as
  $\mathcal{G}(\psi)= (s,k,Y)
  [\alpha_j:\mathcal{G}(\psi_k[\alpha_j/Y])]$ where
  $\alpha_j \in type(Y)$ and $\psi_k$ is the sub-tree of $\psi$ such that
  $\gamma_k[\alpha_j/Y]$ is satisfiable.
\end{Def}

\begin{Ex}[Grounding]
  Consider the OSDD in Fig. \ref{fig:grounding}(a). In the first step
  of the grounding, all values satisfy the (empty) constraint of the
  outgoing edge. Therefore we get two subtrees which are identical
  except the substitution that is applied to the variable $X1$ (see
  Fig. \ref{fig:grounding}(b)). In the next step, the subtrees are
  ground. Consider the left subtree in Fig. \ref{fig:grounding}(b).
  The value ``a'' satisfies the left branch, while the value ``b''
  satisfies the right branch. In a similar fashion the right subtree
  is ground to yield the ground MDD in Fig. \ref{fig:grounding}(c).
\end{Ex}

\begin{figure}[h]
  \centering
  \begin{tabular}{c  c  c}
    \begin{minipage}[t]{0.15\textwidth}
      \begin{adjustbox}{scale=0.75}
        $\vcenter{
        \begin{tikzpicture}
          \node[vertex] (a) {\texttt{msw(flip, 1, X1)}};
          \node[vertex] (b) [below=of a] {\texttt{msw(flip, 2, X2)}};
          \node[leaf] (s) at ([shift={(-1,-2)}] b) {$1$};
          \node[leaf] (f) at ([shift={(1,-2)}] b) {$0$};
          \path[dir_edge] (a) -- (b);
          \path[dir_edge] (b) -- node[osddconstr, below left] {$\mathtt{X1}=\mathtt{X2}$} (s);
          \path[dir_edge] (b) -- node[osddconstr, below right] {$\mathtt{X1}\neq \mathtt{X2}$} (f);
        \end{tikzpicture}
        }$
      \end{adjustbox}
    \end{minipage}
    &
        \begin{minipage}{0.35\textwidth}
          \centering
          \begin{adjustbox}{scale=0.6}
            $\vcenter{
            \begin{tikzpicture}
              \node[vertex] (a) {\texttt{msw(flip, 1, X1)}};
              \node[vertex] (bl) at ([shift={(-2,-1)}] b) {\texttt{msw(flip, 2, X2)}};
              \node[vertex] (br) at ([shift={(2,-1)}] b) {\texttt{msw(flip, 2, X2)}};
              \node[leaf] (sl) at ([shift={(-1,-2)}] bl) {$1$};
              \node[leaf] (fl) at ([shift={(1,-2)}] bl) {$0$};
              \node[leaf] (sr) at ([shift={(-1,-2)}] br) {$1$};
              \node[leaf] (fr) at ([shift={(1,-2)}] br) {$0$};
              \path[dir_edge] (a) -- node[osddconstr] {$\mathtt{a}$} (bl);
              \path[dir_edge] (a) -- node[osddconstr] {$\mathtt{b}$} (br);
              \path[dir_edge] (bl) -- node[osddconstr, left] {$\mathtt{a}=\mathtt{X2}$} (sl);
              \path[dir_edge] (bl) -- node[osddconstr, right] {$\mathtt{a}\neq \mathtt{X2}$} (fl);
              \path[dir_edge] (br) -- node[osddconstr, left] {$\mathtt{b}=\mathtt{X2}$} (sr);
              \path[dir_edge] (br) -- node[osddconstr, right] {$\mathtt{b}\neq \mathtt{X2}$} (fr);
              
            \end{tikzpicture}
            }$
          \end{adjustbox}
        \end{minipage}
    &
        \begin{minipage}{0.35\textwidth}
          \centering
          \begin{adjustbox}{scale=0.6}
            $\vcenter{
            \begin{tikzpicture}
              \node[vertex] (a) {\texttt{msw(flip, 1, X1)}};
              \node[vertex] (bl) at ([shift={(-2,-1)}] b) {\texttt{msw(flip, 2, X2)}};
              \node[vertex] (br) at ([shift={(2,-1)}] b) {\texttt{msw(flip, 2, X2)}};
              \node[leaf] (sl) at ([shift={(-1,-2)}] bl) {$1$};
              \node[leaf] (fl) at ([shift={(1,-2)}] bl) {$0$};
              \node[leaf] (sr) at ([shift={(-1,-2)}] br) {$1$};
              \node[leaf] (fr) at ([shift={(1,-2)}] br) {$0$};
              \path[dir_edge] (a) -- node[osddconstr] {$\mathtt{a}$} (bl);
              \path[dir_edge] (a) -- node[osddconstr] {$\mathtt{b}$} (br);
              \path[dir_edge] (bl) -- node[osddconstr, left] {$\mathtt{a}$} (sl);
              \path[dir_edge] (bl) -- node[osddconstr, right] {$\mathtt{b}$} (fl);
              \path[dir_edge] (br) -- node[osddconstr, left] {$\mathtt{b}$} (sr);
              \path[dir_edge] (br) -- node[osddconstr, right] {$\mathtt{a}$} (fr);
              
            \end{tikzpicture}
            }$
          \end{adjustbox}
        \end{minipage}\\
    (a) OSDD & (b) Partial grounding & (c) Ground MDD
  \end{tabular}
  \caption{Example of grounding OSDD}
  \label{fig:grounding}
\end{figure}
\myparagraph{Canonical OSDD representation.}  Given a total order
among variables and terms, the order of nodes in an OSDD is fixed.  We
can further order the outgoing edges uniquely based on the total order
of constraints labeling them.  This yields a canonical representation
of OSDDs.  In the rest of the paper we assume that OSDDs are in
canonical form.


We now define common operations over OSDDs which are applied to construct OSDDs from primitives.


\begin{Def}[Conjunction/Disjunction]\label{def:conjunction-disjunction}
  Given OSDDs $\psi = (s, k, Y)[\gamma_i : \psi_i]$ and
  $\psi' = (s', k', Y')[\gamma'_j : \psi'_j]$, let $\oplus$ stand for
  either $\land$ or $\lor$ operation. Then $\psi \oplus \psi'$ is
  defined as follows.
  \begin{itemize}
  \item If $(s, k) \prec (s', k')$, then
    $\psi \oplus \psi' = (s, k, Y)[\gamma_i:\psi_i \oplus \psi']$
  \item If $(s', k') \prec (s, k)$ then
    $\psi \oplus \psi' = (s', k', Y')[\gamma'_j:\psi'_j
    \oplus \psi]$
  \item If $(s, k) = (s', k')$, first we apply the substitution
    $[Y/Y']$ to the second OSDD. Then
    $\psi\oplus\psi'=(s, k, Y)[\gamma_i\land\gamma'_j:\psi_i\oplus\psi'_j]$.
  \end{itemize}
\end{Def}

\begin{figure}
  \centering
  \begin{tabular}{c c c}
    \begin{minipage}[t]{0.25\textwidth}
      \begin{adjustbox}{scale=0.7}
        $\vcenter{
          \begin{tikzpicture}
            \node[vertex] (r1) {\texttt{msw(b,1,X1)}};
            \node[vertex] (c1) [below=of r1] {\texttt{msw(b,2,X2)}};
            \node[leaf] (s1) at ([shift={(-1,-2)}] c1) {$1$};
            \node[leaf] (f1) at ([shift={(1,-2)}] c1) {$0$};

            \path[dir_edge] (r1) -- (c1);
            \path[dir_edge] (c1) -- node[osddconstr,left] {$X1=X2$} (s1);
            \path[dir_edge] (c1) -- node[osddconstr,right] {$X1\neq X2$} (f1);
          \end{tikzpicture}
        }$
      \end{adjustbox}
    \end{minipage}
    &
      \begin{minipage}[t]{0.25\textwidth}
        \begin{adjustbox}{scale=0.7}
          $\vcenter{
            \begin{tikzpicture}
              \node[vertex] (r1) {\texttt{msw(b,1,X1)}};
              \node[vertex] (c1) [below=of r1] {\texttt{msw(b,3,X3)}};
              \node[leaf] (s1) at ([shift={(-1,-2)}] c1) {$1$};
              \node[leaf] (f1) at ([shift={(1,-2)}] c1) {$0$};
              
              \path[dir_edge] (r1) -- (c1);
              \path[dir_edge] (c1) -- node[osddconstr,left] {$X1=X3$} (s1);
              \path[dir_edge] (c1) -- node[osddconstr,right] {$X1\neq X3$} (f1);
            \end{tikzpicture}
          }$
        \end{adjustbox}
      \end{minipage}
    &
      \begin{minipage}[t]{0.5\textwidth}
        \begin{adjustbox}{scale=0.7}
          $\vcenter{
            \begin{tikzpicture}
              \node[vertex] (r1) {\texttt{msw(b,1,X1)}};
              \node[vertex] (c1) [below=of r1] {\texttt{msw(b,2,X2)}};
              \node[leaf] (s1) at ([shift={(-1,-2)}] c1) {$1$};
              \node[vertex] (c2) at ([shift={(1,-2)}] c1)
              {\texttt{msw(b,3,X3)}};
              \node[leaf] (s2) at ([shift={(-1,-2)}] c2) {$1$};
              \node[leaf] (f1) at ([shift={(1,-2)}] c2) {$0$};
              \path[dir_edge] (r1) -- (c1);
              \path[dir_edge] (c1) -- node[osddconstr,left] {$X1=X2$}
              (s1);
              \path[dir_edge] (c1) -- node[osddconstr,right] {$X1\neq X2$}
              (c2);
              \path[dir_edge] (c2) -- node[osddconstr,left] {$X1=X3$} (s2);
              \path[dir_edge] (c2) -- node[osddconstr,right] {$X1\neq X3$} (f1);
            \end{tikzpicture}
          }$
        \end{adjustbox}
      \end{minipage}\\
    \multicolumn{2}{c}{(a) Input OSDDs} & (b) Disjunction of input OSDDs
  \end{tabular}
  \caption{Disjunction of OSDDs}
  \label{fig:osdd-or}
\end{figure}

\begin{Ex}[Conjunction/Disjunction]
  Consider the input OSDDs in Fig. \ref{fig:osdd-or}(a). Their
  disjunction is shown in Fig. \ref{fig:osdd-or}(b). Disjunction of
  this OSDD with a third OSDD which is isomorphic to the input OSDDs
  but involving switch instance pairs $(b,2),
  (b,3)$ results in the OSDD shown in Fig. \ref{fig:osdd-intro-ex}(b).
\end{Ex}

\myparagraph{Transformation from improper to proper OSDDs.}
\begin{figure}[h]
	\centering
	\begin{tabular}{cp{0.0in}c}
		\begin{minipage}[t]{.35\textwidth}
			\begin{adjustbox}{scale=0.7}
				$\vcenter{
				\begin{tikzpicture}
				\node[vertex] (a) {\texttt{X}}; 
				\node[vertex] (b) [below=of a] {\texttt{Y}}; 
				\node[vertex] (c) [below=of b] {\texttt{Z}};
				\node[leaf] (d) [below left= 1.5cm and 3cm of c] {$\Psi_1$};
				\node[leaf] (e) [below left= 2.5cm and 1cm of c] {$\Psi_2$};
				\node[leaf] (f) [below left= 2.5cm and -1.75cm of c] {$\Psi_3$};
				\node[leaf] (fail1) [below left= 1.5cm and -3.5cm of c] {$0$};
				\path[dir_edge] (a) -- (b); 
				\path[dir_edge] (b) --  (c);
				\path[dir_edge] (c) -- node[osddconstr, below left= 0cm and 0cm] {$\mathtt{Z}=\mathtt{X} \land \mathtt{Z} = \mathtt{Y} $} (d);
				\path[dir_edge] (c) -- node[osddconstr, below left= .95cm and -.25cm] {$\mathtt{Z}=\mathtt{X} \land \mathtt{Z} \neq \mathtt{Y} $} (e);
				\path[dir_edge] (c) -- node[osddconstr, below right= .95cm and -.25cm] {$\mathtt{Z} \neq \mathtt{X} \land \mathtt{Z} = \mathtt{Y} $} (f);
				\path[dir_edge] (c) -- node[osddconstr, below right= 0cm and 0cm] {$\mathtt{Z} \neq \mathtt{X} \land \mathtt{Z} \neq \mathtt{Y} $} (fail1);
				\end{tikzpicture}
			}$
			\end{adjustbox}
		\end{minipage}
		& &
		\begin{minipage}{0.5\textwidth}
			\begin{adjustbox}{scale=0.75}
				$\vcenter{
				\begin{tikzpicture}
				\node[vertex] (a) {\texttt{X}}; 
				\node[vertex] (b) [below=of a] {\texttt{Y}}; 
				\node[vertex] (c) [below left= .75cm and 2cm of b] {\texttt{Z}};
				\node[vertex] (c2) [below right= .75cm and 2cm of b] {\texttt{Z}};
				
				\node[leaf] (d) [below left= 1cm and .5cm of c] {$\Psi_1$};
				\node[leaf] (fail1) [below right= 1cm and .5 cm of c] {$0$};
				
				\node[leaf] (e2) [below left= 1cm and 1cm of c2] {$\Psi_2$};
				\node[leaf] (f2) [below left= 2.5cm and -.5cm of c2] {$\Psi_3$};
				\node[leaf] (fail2) [below left= 1cm and -2cm of c2] {$0$};
				
				\path[dir_edge] (a) -- (b); 
				\path[dir_edge] (b) -- node[osddconstr, below left= 0cm and 0cm] {$\mathtt{X}=\mathtt{Y} $} (c);
				\path[dir_edge] (b) --  node[osddconstr, below right= 0cm and 0cm] {$\mathtt{X} \neq \mathtt{Y} $} (c2);
				
				\path[dir_edge] (c) -- node[osddconstr, below left= 0cm and -.15cm] {$\mathtt{Z}=\mathtt{X} \land \mathtt{Z} = \mathtt{Y} $} (d);
				\path[dir_edge] (c) -- node[osddconstr, below right= 0cm and -.35cm] {$\mathtt{Z} \neq \mathtt{X} \land \mathtt{Z} \neq \mathtt{Y} $} (fail1);
				
				\path[dir_edge] (c2) -- node[osddconstr, below left= 0cm and 0cm] {$\mathtt{Z}=\mathtt{X} \land \mathtt{Z} \neq \mathtt{Y} $} (e2);
				\path[dir_edge] (c2) -- node[osddconstr, below right = .95cm and -1cm] {$\mathtt{Z} \neq \mathtt{X} \land \mathtt{Z} = \mathtt{Y} $} (f2);
				\path[dir_edge] (c2) -- node[osddconstr, below right= 0cm and 0cm] {$\mathtt{Z} \neq \mathtt{X} \land \mathtt{Z} \neq \mathtt{Y} $} (fail2);
				\end{tikzpicture}
			}$
			\end{adjustbox}
		\end{minipage}\\
		(a) Improper OSDD && (b) Proper OSDD
	\end{tabular}
	\caption{Transformation example}
	\label{fig:osdd-improper-to-proper}
\end{figure}


When performing conjunction/disjunction operations over proper OSDDs, the resulting
OSDD may be improper.  For instance, consider one OSDD with variables
$X,Z$, and another with variables $Y,Z$.  Constraints between
$X$ and $Z$, and those between $Y$ and
$Z$ may imply constraints between $X$ and
$Y$ that may not be explicitly present in the resulting OSDD, thereby
violating the condition of explicit constraints
(Def. ~\ref{def:osdd}).

Fig.~\ref{fig:osdd-improper-to-proper}(a) shows an improper OSDD that
violates the explicit constraints condition.  For example, the edge
$(Z, \Psi_1)$, leading to the sub-OSDD $\Psi_1$, has edge constraints
which imply $X = Y$ while the edges leading to $\Psi_2$ and $\Psi_3$
imply $X \neq Y$.

An improper OSDD can be converted into a proper one by rewriting it
using a sequence of steps as follows.  First, we identify an implicit
constraint and where it may be explicitly added without violating the
urgency property.  In the example, we identify $X=Y$ as implicit, and
attempt to introduce it on the outgoing edges of node labeled $Y$.
This introduction splits the edge from $Y$ to $Z$ into two: one
labeled $X=Y$, and another labeled $X\neq Y$, the negation of the
identified constraint.  The original child rooted at $Z$ is now
replicated due to this split.  We process each child, eliminating
edges and corresponding sub-OSDDs whenever the constraints are
unsatisfiable.  In the example in
Fig.~\ref{fig:osdd-improper-to-proper}(b) we see that the edges
$(Z, \Psi_2)$ and $(Z, \Psi_3)$ have been removed from $\Psi_{Z_1}$
since their constraint formula are inconsistent with $X = Y$.  We
repeat this procedure until no implicit constraints exist in $\Psi$.


Although OSDDs have been defined as trees, we can turn them into DAGs
by combining equivalent subtrees.
%We define equivalence between OSDDs as follows.
\begin{Def}[Equivalence]
  \label{def:equivalence}
  All OSDD leaves which have the same node label are equivalent.  Two
  OSDDs $\psi = (s, k, Y)[\gamma_i : \psi_i]$ and $\psi' = (s, k,
  Y')[\gamma'_i : \psi'_i]$ are equivalent if $\forall i.\ \
  [\gamma_i:\psi_i] = [\gamma'_i:\psi'_i][Y/Y']$.
\end{Def}
It is easy to generalize the OSDD operations defined above to work directly over DAGs. 

\comment{ Similar to BDDs we can define \emph{reduced} OSDDs by
  eliminating nodes whose children are all equivalent; however, a node
  may be eliminated only if its output variable is not used in a
  constraint in some descendant subtree, as defined below:

\begin{Def}[Marginalization]\label{def:marginalization}
  Given an OSDD $\psi = (s, k, Y)[\gamma_i : \psi_i]$ such that
  $\forall i. \psi_i = \psi'$ and $Y \not \in FV(\psi')$, then $\psi =
  \psi'$
\end{Def}
}

% Note that this operation corresponds to the elimination of nodes
% from a BDD when the node has identical children. However, in OSDDs
% we need to check that the variable is not used in the subtree before
% the node can be safely eliminated.

\myparagraph{Constraint application.} Given an OSDD, the MDD
represented by it is altered by the application of new atomic
constraints. The operation which specializes an OSDD to satisfy an
atomic constraint is defined as follows.
\begin{Def}[Constraint application]\label{def:constraint-apply}
  Given an OSDD $\psi = (s,k,Y)[\gamma_i:\psi_i]$ and an atomic
  constraint $\beta$, the application of $\beta$ to $\psi$ results in a
  new OSDD $\psi'$ as follows:
  \begin{itemize}
  \item Application of $\beta$ to $0, 1$ yields $0, 1$ respectively.
  \item If $Vars(\beta) \subseteq \mathcal{O}(n)$ where $n$ is the root of
    $\psi$, then $\psi' = (s,k,Y)[\gamma_i \land \beta: \psi_i, \neg
    \beta: 0 ]$
  \item Else $\psi' = (s,k,Y)[\gamma_i : \psi'_i]$ where each
    $\psi'_i$ results from the application of $\beta$ to $\psi_i$.
  \end{itemize}
\end{Def}

\myparagraph{Properties.}  OSDDs and the operations defined above have
a number of properties necessary for their use in representing
explanations for query evaluation in PLPs.

% Proof of the following properties can be found in Appendix \ref{appendix:Proofs}.

\begin{Pro}[Closure]\label{pro:closure}
  OSDDs are closed under conjunction and disjunction
  operations.
\end{Pro}

The following shows that conjunction and disjunction operations over
OSDDs lift the meaning of these operations over ground MDDs.
\begin{Pro}[Compatibility with Grounding]
  Let $\psi = (s, k, Y)[\gamma_i : \psi_i]$ and
  $\psi' = (s', k', Y')[\gamma'_j : \psi'_j]$ be two OSDDs, then
  \begin{gather*}
    %\mathcal{G}(\neg \psi) = \neg \mathcal{G}(\psi)\\
    \mathcal{G}(\psi \oplus \psi') = \mathcal{G}(\psi) \oplus
    \mathcal{G}(\psi').
  \end{gather*}
\end{Pro}

%\myparagraph{Constraint propagation}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: