\documentstyle[jair,twoside,11pt,theapa]{article}
\input epsf %% at top of file

\jairheading{8}{1998}{165-222}{8/97}{6/98}
\ShortHeadings{Model-Based Diagnosis using Structured-System Descriptions}
{Darwiche}
\firstpageno{165}

\begin{document}


\title{Model-Based Diagnosis using Structured System Descriptions}

\author{\name Adnan Darwiche \email darwiche@aub.edu.lb \\
        \addr Department of Mathematics \\
              American University of Beirut \\
              PO Box 11-236 \\
              Beirut, Lebanon}

\maketitle 


\begin{abstract}
This paper presents a comprehensive approach for model-based diagnosis
which includes proposals for characterizing and computing preferred diagnoses,
assuming that the system description is augmented with a system structure (a 
directed graph explicating the interconnections between system components). 
Specifically, we first introduce the notion of a {\em consequence,} 
which is a syntactically unconstrained propositional sentence that 
characterizes all consistency-based diagnoses and show that standard 
characterizations of diagnoses, such as minimal conflicts, correspond to 
syntactic variations on a consequence. Second, we propose a new syntactic
variation on the consequence known as {\em negation normal form (NNF)} and 
discuss its merits compared to standard variations. Third, we introduce a 
basic algorithm for computing consequences in NNF given a structured system 
description. 
We show that if the system structure does not contain cycles, then there
is always a linear--size consequence in NNF which can be computed 
in linear time.
For arbitrary system structures, we show a precise connection between the 
complexity of computing consequences and the topology of the underlying 
system structure. Finally, we present an algorithm that enumerates the 
preferred diagnoses characterized by a consequence. The algorithm is shown to
take linear time in the size of the consequence if the preference
criterion satisfies some general conditions.
\end{abstract}


\input{/home/darwiche/latex/stdmacros.tex}

\input{/home/darwiche/latex/journals/JAIR/mbd/inputs/macros.tex}


\section{Introduction}

This paper presents a comprehensive approach for characterizing and computing
preferred diagnoses when the system description is augmented with a 
system structure \cite{darwicheIJCAI95}.
A system structure is a directed acyclic graph explicating the interconnections 
between system components. Adding a system structure to a classical system
description \cite{dekleer:characterizing-diagnoses}
leads to what we call a {\em structured system description,} 
examples of which are shown in Figures~\ref{fig:ssd-1} and~\ref{fig:ssd-2}.

The most common approach for characterizing (and computing) diagnoses has been 
the use of conflicts and their derivatives such as kernel diagnoses 
\cite{dekleer87,Reiter:Diagnosis,dekleer:characterizing-diagnoses}.
Moreover, the most common method for computing these characterizations 
has been the use of Assumption-Based Truth Maintenance Systems (ATMSs)
\cite{dekleer86a,reiter87,dekleerBOOK93}. We will first explain the difficulties
with such an approach and then describe the elements of our approach
that address these difficulties.

The major problem with standard characterizations of diagnoses is that
they tend to be exponential in size, which is largely due to their syntactic
nature. Specifically, standard characterizations of diagnoses correspond to
the prime implicants/implicates of some propositional sentence. 
And the number of 
such implicants/implicates tend to be exponential even for expressions
that correspond to simple diagnosis problems. Computationally, this problem 
manifests as an ATMS label that has an exponential number of 
environments \cite{dekleerBOOK93}. 

This difficulty has led to a body of research on ``focusing'' the ATMS, which 
attempts to control the size of ATMS labels 
\cite{provan96,dekleer91,FdK88,dressler-farquar90,Collins-decoste91}. 
Focusing is based on the following intuition. A label characterizes all 
diagnoses of a given problem, but one is rarely interested in all diagnoses;
therefore, one rarely needs a complete label. Most 
often, one is interested in diagnoses that satisfy some preference criterion, 
such as most-probable diagnoses. Therefore, one can use such a criterion 
to compute ``focused'' labels that are of reasonable size, yet are good
enough to characterize the diagnoses of interest. However, although a 
standard framework exists for computing ATMS labels 
\cite{dekleerBOOK93}, no such framework seems to exist for focusing.

Another issue with standard frameworks for computing diagnoses (based on 
minimizing propositional sentences) is that their computational complexity is 
not formally tied to properties of system descriptions that are easily 
accessible to engineers who would be constructing these descriptions. 
An example of such a property is the topology of a system structure 
(component interconnectivity).
Providing computational complexity guarantees in terms of such properties
can be extremely useful in practice, as our experience has shown. In real-world 
applications, one may have a choice of what failures to include in the scope 
of a diagnostic system, and therefore a choice of what aspects of a complex 
system to include in a system description. In such situations, it is 
very important to be able to assess the effectiveness of diagnosis algorithms 
by an intuitive examination of the resulting system description, such as examining
the topology of a structured system description.
The framework we shall develop in this paper addresses this particular point
and has proven very useful in helping us engineer system descriptions on which 
our diagnostic algorithms are guaranteed to be 
effective.

The approach we present in this paper is based on three main ideas, which 
address the problems mentioned above:

\begin{enumerate}
\item {\bf Characterizing diagnoses using negation normal forms:}
We propose the notion of a consequence which is a syntactically unconstrained 
propositional sentence that characterizes all consistency-based diagnoses
\cite{darwicheIJCAI95,darwicheAIJ-IND}. 
We show that standard characterizations of diagnoses correspond to syntactic
restrictions on a consequence. Specifically, minimal conflicts correspond
to the prime implicates of a consequence and kernel diagnoses correspond to 
its prime implicants. We adopt a less restrictive syntax of consequences 
known as {\em negation normal form (NNF)} of which prime implicants/implicates
are a special case \cite{Handbook.Math.Logic}. Although 
we do not guarantee that our NNF representation of consequences is the most
compact, we do offer some guarantees on this representation that cannot be 
offered with respect to standard representations. 


\item {\bf Utilizing system structure in computing consequences:}
We introduce a basic algorithm for computing consequences in NNF, 
the complexity of 
which is determined by the topology of the system structure. We show that 
for tree system structures (those containing no undirected cycles), 
there is always a consequence in NNF that is linear in the number of 
nodes and arcs in the structure.\footnote{Note, however, that the 
size of a consequence and the time to compute it is exponential in the 
size of families (each node and its parents in the device structure 
represent a family). In structure--based reasoning,
it is typically assumed that the size of a family is small enough to be
treated like a constant.} Moreover, a standard characterization of 
diagnoses using minimal conflicts can be exponential in size for some of 
these system structures.
For arbitrary system structures, we provide a precise relationship between 
the system structure, the size of a consequence, the time to compute it, 
and, hence, the difficulty of a diagnosis problem.


\item {\bf A mechanism for computing minimal diagnoses:}\footnote{In this
paper, we use ``minimal'' and ``preferred'' interchangeably when referring
to diagnoses.}
We show that if a consequence is in {\em decomposable} negation normal form,
then one can extract the minimal diagnoses it characterizes in time 
linear in its size, as long as the minimality criterion satisfies some 
general conditions. The algorithm we propose for computing consequences
is guaranteed to generate consequences in decomposable negation normal form. 
Moreover, the conditions on a minimality criterion do 
admit the common criterion of minimum cardinality.
\end{enumerate}

Therefore, we are providing a paradigm for diagnostic reasoning with
system structures, consequences, and minimality criteria as the key
components. By using this paradigm, one is guaranteed some complexity 
results that are determined by the topology of the system 
structure. As we shall see, this approach is similar to the 
network-paradigm in the probabilistic and constraint-satisfaction 
literature where system structure is the key aspect that decides the
difficulty of a reasoning problem. 

The literature contains a number of other proposals for importing this 
structure-based theme into model-based diagnosis 
\cite{dechterAIJ94,geffner87}. Although these approaches appeal to similar 
underlying principles and lead to similar complexity results, some key 
differences exist between our approach and the previous ones. 
First, our formulation is based on symbolic
logic, which is the tradition in model-based diagnosis, while the previous
proposals 
have been based on constraints among multivalued variables. Second, the 
complexity of our algorithm depends not only on the system structure but 
also on the system observation. The stronger the system observation is, 
the better the complexity of our algorithm, leading to linear complexity 
in the extreme case (independently of the system structure). Finally, we 
separate the computation of minimal diagnoses
into two phases: the characterization of 
all diagnoses using a consequence and then the extraction of 
minimal diagnoses from the consequence. This separation has a number of 
implications which are discussed in detail later in the paper.

This paper is structured as follows. We introduce the notion of a consequence 
in Section~\ref{sec:consequence}, proving that it characterizes all
consistency-based diagnoses, and showing its relation to some standard notions
in the literature on model-based diagnosis. We then introduce three key
theorems for constructing consequences in Section~\ref{sec:structure} and
formalize the role of system structure in determining the complexity of 
computing consequences. In Section~\ref{sec:algorithm}, we turn to an 
algorithm for computing consequences when the system description is 
augmented with a system structure. The computational complexity of the
presented algorithm is discussed at length in Section~\ref{sec:complexity}.
We then provide an algorithm in Section~\ref{sec:extraction} 
for extracting minimal diagnoses from a consequence. We finally close in 
Section~\ref{sec:conclusion} with some concluding remarks. 
Proofs of all theorems and lemmas are delegated to Appendix~\ref{app:proofs}.


\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\vspace{.5cm}
\begin{center}
\mbox{\epsfxsize=100mm \leavevmode \epsffile{ssd-1.eps}}
\end{center}

{\tiny
\begin{center}
\begin{tabular}{c|c|c|c}
\(\Delta_A, \Delta_B, \Delta_C\) & 
\(\Delta_D \) & \(\Delta_E\) & \(\Delta_F\) \\ \hline
& & & \\
\(\left\{\right\}\) & 
\(\left\{\begin{array}{rcl}
A \wedge \ok(X) & \imply & \neg D \\
\neg A \wedge \ok(X) & \imply & D
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
(B \wedge C) \wedge \ok(Y) & \imply & E \\
\neg (B \wedge C) \wedge \ok(Y) & \imply & \neg E
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
(D \vee E) \wedge \ok(Z) & \imply & F \\
\neg (D \vee E) \wedge \ok(Z) & \imply & \neg F
\end{array}\right\}\) 
\end{tabular}
\end{center}
}
\end{minipage}
}
\end{center}
\caption{A structured system description (SSD) of a digital circuit. 
An SSD has two parts: a directed acyclic graph and a set of component 
descriptions, each associated with a node in the graph. The formal
definition of an SSD is given in Section~\protect{\ref{sec:ssd}}.
\label{fig:ssd-1}}
\end{figure}



\section{Characterizing Diagnoses}  
\label{sec:consequence}

\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\vspace{.5cm}
\begin{center}
\mbox{\epsfxsize=80mm \leavevmode \epsffile{ssd-2.eps}}
\end{center}

{\tiny
\begin{center}
\begin{tabular}{c|c|c}
\(\Delta_A, \Delta_B\) & \(\Delta_C \) & \(\Delta_D\) \\ \hline
& & \\
\(\{\}\) &
\(\left\{\begin{array}{rcl}
A \wedge \ok(X) & \imply & \neg C \\
\neg A \wedge \ok(X) & \imply & C
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
(A \wedge B) \wedge \ok(Y) & \imply & D \\
\neg (A \wedge B) \wedge \ok(Y) & \imply & \neg D
\end{array}\right\}\)
\end{tabular}
\end{center}
}
\end{minipage}
}
\end{center}
\caption{A structured system description of a digital circuit. 
\label{fig:ssd-2}}
\end{figure}

We start in this section with a review of model-based diagnosis and
then lead into the notion of a consequence for characterizing diagnoses.
We show how standard characterizations of diagnoses, such as minimal
conflicts, can be viewed as syntactic variations on the consequence and 
then introduce a new syntactic variation known as negation normal form.
We also discuss our reasons for adopting this non-standard form for
characterizing diagnoses.

\subsection{Model-Based Diagnosis}

In model-based diagnosis, we use the term {\em system description} to denote 
a system model \cite{dekleer:characterizing-diagnoses,Reiter:Diagnosis}. 
Traditionally, a system description consists of a set of logical sentences
\(\Delta\) called a {\em database} and a set of distinguished symbols 
\(\cA = \{\ok(X), \ok(Y), \ldots\}\) called {\em assumables.} Assumables 
represent the health of components and are initially assumed to be true.
For example, in Figure~\ref{fig:ssd-2}, the assumables are 
\(\ok(X), \ok(Y)\) and the database \(\Delta\) contains the four 
propositional sentences shown in the figure.

A diagnosis problem emerges when assumables can no longer be justified.
Specifically, given some sentence \(\phi\) that represents an observed 
system behavior, the system is considered faulty if \(\phi\) is 
inconsistent with \(\Delta \cup \cA\). In this case, one needs to relax 
some of the assumables (that is, replace instances of \(\ok(.)\) 
with instances of  \(\neg \ok(.)\)) in order to restore consistency. A 
particular relaxation of these assumables is called a {\em diagnosis} as
long as it is consistent with the system description and observation.
The cardinality of a diagnosis is the number of faults contained in
the diagnosis. In Figure~\ref{fig:ssd-2}, a system observation
\(C \wedge D\) would indicate a failure. Moreover, there are three diagnoses
in this case: \(\ok(X) \wedge \neg \ok(Y), \neg \ok(X) \wedge \ok(Y),
\neg \ok(X) \wedge \neg \ok(Y)\), with cardinalities 1, 1 and 2, respectively.

We have the following formal definition of a system description, which
we adopt in the rest of this paper. The definition is a variation on the
standard one provided in \cite{Reiter:Diagnosis} and is preceded by some
preliminary definitions.


\begin{definition}
Let \(\S\) be a set of atomic propositions (atoms).
An \underline{\(\S\)--literal} is a literal whose atom is in \(\S\).
An \underline{\(\S\)--sentence} 
is a propositional sentence in which each literal is an \(\S\)--literal.
An \underline{\(\S\)--instantiation} is a conjunction of \(\S\)--literals, 
one literal for each atom in \(\S\). 
\end{definition}
For example, if \(\S = \{A,B,C\}\), then there are eight 
\(\S\)--instantiations: \(A \wedge B \wedge C\), \(A \wedge B \wedge \neg C\), 
\(\ldots\), \(\neg A \wedge \neg B \wedge \neg C\). 
Moreover, \(A \wedge \neg B \imply C\) and \(A \imply C\)
are \(\S\)--sentences, but \(A \imply D\) is not.



\begin{definition}[System Description] \label{def:sd}
A system description is a triple \(\sd\), where \(\cP\) and \(\cA\) are
sets of atomic propositions such that \(\cP \cap \cA = \emptyset\), and 
\(\Delta\) is a set of propositional sentences constructed from atoms in 
\(\cP\) and \(\cA\). Here, \(\cP\) is called the set of non-assumables;
\(\cA\) is called the set of assumables; \(\Delta\) is called a 
database. It is required that \(\Delta\) be consistent with every 
\(\A\)--instantiation.
\end{definition}

Given the notion of a system description, we can define the other
two key terms in model-based diagnosis \cite{dekleer:characterizing-diagnoses}:

\begin{definition}[Observation]
Given a system description \(\sd\), a system observation is a consistent
conjunction of \(\cP\)--literals.
\end{definition}

\begin{definition}[Diagnosis] \label{def:diagnosis}
Given a system description \(\sd\) and a system observation \(\phi\), a
diagnosis is an \(\A\)--instantiation that is consistent 
with \(\Delta \cup \{\phi\}\). 
\end{definition}

It is worth mentioning here that the condition we imposed on database 
\(\Delta\) in Definition~\ref{def:sd} is equivalent to saying that there 
are no diagnoses for the system observation \(\true\). That is, if we have 
no observation about the system, then we cannot conclude anything 
about the health of its components.\footnote{This condition is intuitive 
if we are not representing fault modes and are restricting ourselves
to using the \(\ok(.)\) assumables. However, if we use fault modes, such as
{\em stuck-at-0} and {\em stuck-at-1}, then the condition is not as 
intuitive and may even appear restrictive. 
Specifically, we may want to constrain these two assumables such that
\(\neg\) {\em stuck-at-0} \(\vee\) \(\neg\) {\em stuck-at-1} is true. But 
introducing such a constraint would violate the condition we are imposing
on \(\Delta\) in Definition~\ref{def:sd}. 
We will make two points regarding this issue. First, one can
represent constraints among assumables without violating the above 
condition; the details of this are explained in 
Appendix~\ref{app:variables}. However, a better solution to this problem
is to use multivalued variables instead of atomic propositions, which 
leads to a more convenient, but less standard framework, which is also
discussed in Appendix~\ref{app:variables}.}

\subsection{The Consequence}

An ultimate goal of diagnostic reasoning is to compute the minimal diagnoses 
(according to some criterion) for a given system description \(\sd\) and 
observation \(\phi\). Standard approaches to model-based diagnoses do this
in conceptually two steps. First, they characterize the set of diagnoses
using conflicts and then extract minimal diagnoses from this characterization.

We will follow the same approach except that we will not use conflicts to
characterize the set of diagnoses. Instead, we will adopt an equivalent but
syntactically different characterization of diagnoses known as negation
normal form \cite{Handbook.Math.Logic}. 
Before we discuss this alternate characterization of diagnoses,
however, we need to introduce the notion of a consequence which is very
useful in putting the different characterizations of diagnoses in perspective.

The consequence of an observation is defined formally below 
\cite{darwicheIJCAI95,darwicheAIJ-IND}:

\begin{definition}[Consequence] \label{def:consequence}
Given a system description \(\sd\), the consequence of system observation 
\(\phi\), written \(\dg^\Delta_\cA(\phi)\), is a sentence satisfying 
the following properties: 
\begin{enumerate}
\item \(\cons^\Delta_\A(\phi)\) is an \(\A\)-sentence;
\item \(\Delta \cup \{\phi\} \models \cons^\Delta_\A(\phi)\); 
\item For any \(\A\)-sentence \(\beta\), 
\(\Delta \cup \{\phi\} \models \beta\) only if 
\(\cons^\Delta_\A(\phi) \models \beta\).\footnote{The consequence of an 
observation is unique up to logical equivalence.}
\end{enumerate}
\end{definition}
That is, the consequence of observation \(\phi\) is the logically strongest
\(\A\)-sentence which is entailed by the system description
\(\Delta\) and observation \(\phi\).

When clear from the context, we drop the superscript \(\Delta\), the 
subscript \(\cA\), or both, from the notation \(\cons^\Delta_\cA\).

For example, if we observe that both \(C\) and \(D\) are true in the
circuit of Figure~\ref{fig:ssd-2}, we conclude that one of the gates
must be malfunctioning: under normal conditions, \(C\) being true 
implies that \(A\) is false, which further implies that \(D\) is false. 
Therefore, a conclusion one can make about assumables, having observed
\(C \wedge D\), is that \(\neg \ok(X) \vee \neg \ok(Y)\). Moreover,
this is the strongest conclusion that can be made given the system description
and observation at hand. Formally, this means that 
\(\neg \ok(X) \vee \neg \ok(Y)\) is the consequence of observation 
\(C \wedge D\), \(\cons^\Delta_\cA(C \wedge D)\).


That a consequence characterizes all consistency-based diagnoses is shown
formally below:
\begin{theorem}[Characterization] \label{theo:characterization}
Given a system description \(\sd\), an \(\A\)-instantiation \(\alpha\) is 
a diagnosis for system observation \(\phi\) according to 
Definition~\ref{def:diagnosis} iff \(\alpha \models \dg^\Delta_\cA(\phi)\).
\end{theorem}
For example, the consequence 
\(\neg \ok(X) \vee \neg \ok(Y)\) characterizes three diagnoses: 
\(\neg \ok(X) \wedge \neg \ok(Y)\), \(\ok(X) \wedge \neg \ok(Y)\) and
\(\neg \ok(X) \wedge \ok(Y)\). 


Standard characterizations of diagnoses can be viewed as syntactic 
restrictions on a consequence. Consider the following theorem first, 
which is a corollary of the results reported 
in \cite{dekleer:characterizing-diagnoses}:

\begin{theorem} \label{theo:connections}
Given a system description \(\sd\) and observation \(\phi\), we have 
the following:
\begin{description}
\item [-] A \underline{partial diagnosis} is any \(\A\)-sentence which 
is an implicant of \(\cons^\Delta_\cA(\phi)\).

\item [-] A \underline{kernel diagnosis} is any \(\A\)-sentence which 
is a prime implicant of \(\cons^\Delta_\cA(\phi)\).

\item [-] A \underline{conflict} is any \(\A\)-sentence which 
is an implicate of \(\cons^\Delta_\cA(\phi)\).

\item [-] A \underline{minimal conflict} is any \(\A\)-sentence which 
is a prime implicate of \(\cons^\Delta_\cA(\phi)\).
\end{description}
\end{theorem}
Prime implicates and implicants are standard notions but we include their
definitions here for completeness:
\begin{definition}
An \underline{implicant} \(\beta\) of a sentence \(\alpha\) is a satisfiable
conjunction of literals which entails \(\alpha\). We say
that \(\beta\) is a \underline{prime implicant} of \(\alpha\)
if no subset of its literals satisfies this condition.
An \underline{implicate} \(\beta\) of a sentence \(\alpha\) is a non-valid
disjunction of literals which is entailed by \(\alpha\).
We say that \(\beta\) is a \underline{prime implicate} of \(\alpha\)
if no subset of its literals satisfies this condition.
\end{definition}
Note that each 
sentence is equivalent to the conjunction of its prime implicates.
Therefore, the conjunction of minimal conflicts is nothing but a syntactic 
form of the consequence. Similarly, each 
sentence is equivalent to the disjunction
of its prime implicants. Therefore, the disjunction of kernel diagnoses is 
also a syntactic form of the consequence.\footnote{The notion of a consequence
as we define it in this paper seems to 
correspond to notions that have appeared previously in the diagnostic 
literature, but these notions did not prove to be computationally
influential. For example, Saraswat et al. define in \cite{saraswatDX90} 
a {\em maximally abstract diagnosis,} which corresponds to 
our notion of a consequence. They also prove that a maximally abstract 
diagnosis characterizes the set of consistency-based diagnoses in the 
sense of Theorem~\ref{theo:characterization} above. Similarly, 
Ayeb el al. define in \cite{ayeb93} a {\em deductive diagnosis,} 
which is closely related to a consequence --- the logically 
strongest deductive diagnosis is the consequence. In both cases, however,
the proposed notions are not utilized computationally as we shall utilize
consequences in the rest of this paper.}

\subsection{Negation Normal Form}

The minimal-conflict representation of a consequence is a minimized 
conjunctive normal form (CNF) and the kernel-diagnoses representation 
is a minimized disjunctive normal form (DNF). 
Both of these standard forms, however, are specials cases of negation normal
form (NNF) \cite{Handbook.Math.Logic}, which we adopt in this paper:

\begin{definition}[Negation Normal Form] \label{def:nnf}
A sentence \(\alpha\) is in negation normal form (NNF) if and only if
\(\alpha\) is either a literal; a disjunction \(\bigvee_i \alpha_i\); 
or a conjunction \(\bigwedge_i \alpha_i\) where each \(\alpha_i\) is in 
negation normal form.
\end{definition}
That is, in an NNF, the negation operator can only be applied to atoms ---
it cannot be applied to compound sentences. For example, 
\(\neg (A \wedge B)\) is not in NNF, but \(\neg A \vee \neg B\) is.
An NNF will typically have nested conjunctions of disjunctions and nested
disjunctions of conjunctions. 


The algorithm we present later will generate consequences in negation 
normal form. The generated consequences are not guaranteed to be the most
compact, but we shall offer some guarantees on their sizes that do not hold
with respect to consequences in standard forms.

The consequences we shall generate are not only in negation normal form but
are also decomposable:

\begin{definition}[Decomposable] \label{def:decomposable}
A sentence \(\alpha\) in NNF is decomposable if and only if
no atoms are shared by any conjuncts in \(\alpha\).\footnote{Every DNF is 
also a decomposable NNF. But this is not necessarily true for CNFs.}
\end{definition}
The sentence 
\(( (\neg A \vee \neg \ok(X)) \wedge (\neg C \vee \neg \ok(Y)) ) \vee 
  ( (\neg \ok(X) \vee A)      \wedge (\neg \ok(Y) \vee C) ) \) is in
decomposable negation normal form: the negation operator appears only 
next to atoms in the sentence; and there are no common atoms between the 
conjuncts \(\neg A \vee \neg \ok(X)\) and \(\neg C \vee \neg \ok(Y)\), 
neither there are any common atoms between the conjuncts 
\(\neg \ok(X) \vee A\) and \(\neg \ok(Y) \vee C\).


The decomposability property is quite strong because it allows one to 
decompose certain computations with respect to an NNF into smaller 
computations with respect to its subsentences.
In Section~\ref{sec:extraction}, 
we shall see how this decomposability property will allow us to extract
the minimal diagnoses characterized by a consequence by simply combining
the minimal diagnoses characterized by its subsentences.\footnote{To 
appreciate this decomposability property, consider testing satisfiability 
as an example. It is easy to verify that such a test can be performed in 
time which is linear in the size of an NNF if the NNF is decomposable. In 
particular:
\begin{enumerate}
\item if \(\alpha\) is a literal, then \(\alpha\) is satisfiable;
\item if \(\alpha = \alpha_1 \vee \ldots \vee \alpha_n\), then 
\(\alpha\) is satisfiable iff some \(\alpha_i\) is satisfiable;
\item if \(\alpha = \alpha_1 \wedge \ldots \wedge \alpha_n\), then
\(\alpha\) is satisfiable iff every \(\alpha_i\) is satisfiable.
\end{enumerate}
Case~3 above does not hold in general since each of two sentences may be 
satisfiable but their conjunction may not. However, if the two sentences 
do not share any atoms, then their satisfiability is enough to guarantee 
the satisfiability of their conjunction.}

Throughout the paper, we will be representing negation normal forms using
directed acyclic graphs. This representation is detailed in 
Appendix~\ref{app:nnfs} which also provides a number of operations for 
manipulating this graphical representation of negation normal forms. 
The operations defined in this appendix will be used in the pseudocode 
that we present later for generating consequences.

\section{Computing Consequences: Some Fundamental Theorems} 
\label{sec:structure}

Given some system observation \(\phi\) and some minimality criterion, our
goal is to compute all minimal diagnoses of \(\phi\) according to this 
criterion. We will do this in two steps. First, we will compute the 
consequence of \(\phi\) in NNF. Second, we will extract from the computed
consequence all the minimal diagnoses it characterizes.
The second step will be addressed in Section~\ref{sec:extraction}. 
In this and the following section, we focus on the first step.

Our strategy for computing consequences is to construct them from
component consequences. Intuitively, a component consequence is the strongest
conclusion one can draw about the health of a component given a particular
state of its {\em ports} (inputs and outputs). We shall present two theorems, 
Decomposition and Case-Analysis, which are sufficient to construct any 
consequence by logically combining component consequences. We start by 
discussing component consequences first and then present the mentioned 
theorems.

\subsection{Component Consequences} \label{sec:ccc}

We assume that the sentences in database \(\Delta\), of a system description 
\(\sd\), are grouped into sets, each representing the description of 
some component in the system. Consider the system in 
Figure~\ref{fig:ssd-2} for example, which has two components whose outputs
are denoted by \(C\) and \(D\). The database \(\Delta\) for this 
system is viewed as the union of two component descriptions 
\(\Delta_C\) and \(\Delta_D\) where
\[
\Delta_C = 
\left\{
\begin{array}{lcr}
A \wedge \ok(X) & \imply & \neg C \\
\neg A \wedge \ok(X) & \imply & C \\
\end{array}
\right\};
\]
and 
\[
\Delta_D = 
\left\{
\begin{array}{lcr}
A \wedge B \wedge \ok(Y) & \imply & D \\
\neg (A \wedge B) \wedge \ok(Y) & \imply & \neg D \\
\end{array}
\right\}.
\]
Without loss of generality, we assume that a system component has one 
output and we use this output to identify the component.\footnote{If we 
want to model a component with \(n\) outputs, we model it as a set of 
\(n\) components, each with one output.}

If \(\Delta_O\) is a component description, then \(\cons^{\Delta_O}_\A(\phi)\)
is called a {\em component consequence} whenever \(\phi\) is an 
instantiation of the ports of component \(O\). 
Following are some component consequences with respect to 
Figure~\ref{fig:ssd-2}:
\begin{eqnarray*}
\cons^{\Delta_C}(A \wedge C) & \equiv & \neg \ok(X), \\
\cons^{\Delta_C}(A \wedge \neg C) & \equiv & \true, \\
\cons^{\Delta_D}(A \wedge B \wedge D) & \equiv & \true, \\
\cons^{\Delta_D}(A \wedge \neg B \wedge D) & \equiv & \neg \ok(Y).
\end{eqnarray*}
Intuitively, a component consequence is a strongest conclusion that can
be made about the health of a component given an observation about
that component ports.

We will now provide a theorem that will be the basis for computing a 
component consequence in time linear in the number of clauses in the 
component description. But first, the following definition:

\begin{definition}[Projection] \label{def:projection}
The projection of an instantiation (clause) \(\alpha\) on a set of atoms 
\(\S\), written \(\alpha_\S\), 
is the conjunction (disjunction) of all \(\S\)--literals in \(\alpha\).
If \(\Delta\) is a database, then \(\alpha_\Delta\) is the projection
of \(\alpha\) on the atoms appearing in \(\Delta\).
\end{definition}
For example, the projection of \(\alpha = A \vee \neg B \vee C\) 
on atoms \(\{A,B\}\) is \(A \vee \neg B\). Moreover,
the projection of \(\alpha\) on database \(\Delta_C\) above is
\(A \vee C\).

\begin{theorem}[Component-Consequence]
\label{theo:cc}
Let \(O\) be a component with inputs \(\I\) and description \(\Delta_O\) 
(in clausal form). If \(\phi\) is an instantiation of atoms \(\I \cup \{O\}\), 
then
\[ \cons^{\Delta_O}_\A(\phi) \equiv 
\bigwedge_{\alpha \in \Delta_O,\:\: \phi \models \neg \alpha_\P} 
\alpha_\A. \]
\end{theorem}
Consider the component description \(\Delta_D\) in
Figure~\ref{fig:ssd-2}, which is shown in clausal form below:
\[
\Delta_D = 
\left\{
\begin{array}{c}
\neg A \vee \neg B \vee \neg \ok(Y) \vee D \\
A \vee \neg \ok(Y) \vee \neg D \\
B \vee \neg \ok(Y) \vee \neg D
\end{array}
\right\}.
\]
Consider also the observation \(\phi = A \wedge \neg B \wedge D\)
which represents a particular state of the component ports. 
For the first and second clauses \(\alpha\) in \(\Delta_D\), we 
have \(\phi \models \alpha_\P\). For the third clause \(\alpha\), we have
\(\phi \models \neg \alpha_\P\). Therefore, the component consequence 
in this case is \(\neg \ok(Y)\) which is the projection of third clause
in \(\Delta_D\) on the assumables.

Any consequence computed by Theorem~\ref{theo:cc} is guaranteed to be 
in CNF. By simply converting it to DNF, we would also be converting 
it to decomposable NNF since each DNF is a decomposable NNF. Note that
this conversion is exponential in the number of assumables appearing
in the consequence. However, the number of such assumables is typically 
small enough to justify viewing this conversion as taking constant time.

\subsection{Decomposition and Case-Analysis}


We now provide two theorems which are sufficient for constructing any system 
consequence from component consequences. 

\begin{theorem}[Decomposition] \label{theo:decomposition}
Let \((\P,\A,\Theta \cup \Gamma)\) be a system description and let 
\(\phi\) be a system observation. If the atoms shared by 
\(\Theta\) and \(\Gamma\) all appear in \(\phi\), then
\[ \cons^{\Theta \cup \Gamma}_\cA(\phi) \equiv
   \cons^\Theta_\cA(\phi_\Theta) \wedge  
   \cons^\Gamma_\cA(\phi_\Gamma). \]
\end{theorem}
The theorem is intuitively saying that we can decompose a consequence 
with respect to a database \(\Theta \cup \Gamma\) into two simpler 
consequences, one with respect to
database \(\Theta\) and the other with respect to database \(\Gamma\), as 
long the atoms shared by \(\Theta\) and \(\Gamma\) appear in the 
observation \(\phi\). 


Now, what if the observation \(\phi\) does not contain all atoms that are 
shared between \(\Theta\) and \(\Gamma\)? We can still decompose the 
computation of a consequence \(\cons^{\Theta \cup \Gamma}_\A(\phi)\) in 
such a case, but at the expense of performing a case analysis on the
shared atoms between \(\Theta\) and \(\Gamma\). For this
we need the following key theorem:

\begin{theorem}[Case-Analysis] \label{theo:case-analysis}
Let \((\P,\A,\Delta)\) be a system description, \(\phi\) be a system 
observation, and let \(\S\) be a subset of \(\P\). Then 
\[ \cons^\Delta_\cA(\phi) \equiv
   \bigvee_{\alpha} \cons^\Delta_\cA(\phi \wedge \alpha), \]
where \(\alpha\) ranges over all instantiations of atoms \(\S\) that 
are consistent with \(\phi\).
\end{theorem}
Case-Analysis is typically used to set the stage for Decomposition. 
That is, if the observation \(\phi\) does not contain all atoms that are
shared between \(\Theta\) and \(\Gamma\), we would perform a case analysis
on shared atoms not appearing in \(\phi\) and then apply Decomposition
to each of the resulting cases. The application of Case-Analysis followed
by Decomposition is summarized below:

\begin{corollary}[Intersection] \label{coro:intersection}
Let \((\P,\A,\Theta \cup \Gamma)\) be a system description, \(\phi\) be
a system observation, and let \(\S\) contain all atoms shared by \(\Theta\) 
and \(\Gamma\). If \(\S\) contains no assumables, then
\[ \cons^{\Theta \cup \Gamma}_\cA(\phi) 
\equiv \bigvee_{\alpha} 
\cons^\Theta_\cA(\alpha \wedge \phi_\Theta) \wedge 
\cons^\Gamma_\cA(\alpha \wedge \phi_\Gamma),
\]
where \(\alpha\) ranges over all instantiations of \(\S\) that are
consistent with \(\phi\).
\end{corollary}

Using Decomposition and Case-Analysis one can always construct a system 
consequence from component consequences as follows. We partition the component
descriptions in \(\Delta\) into two subsets, \(\Theta\) 
and \(\Gamma\). We identify the common atoms between \(\Theta\) 
and \(\Gamma\) and then apply the Intersection Corollary. This allows us
to decompose a consequence \(\cons^\Delta(.)\) into a number of 
smaller consequences of the form \(\cons^{\Theta}(.)\) and 
\(\cons^{\Gamma}(.)\), where each of \(\Theta\) and \(\Gamma\) are
smaller than \(\Delta\). We then apply the same procedure, recursively,
on each of \(\cons^{\Theta}(.)\) and  \(\cons^{\Gamma}(.)\) until
we reach component consequences which can be computed using the
Component-Consequence Theorem.

This procedure will always work. However, it does not guarantee the
size of the resulting consequence. Specifically, the procedure does 
not tell us how to partition a database \(\Delta\) into two databases 
\(\Theta\) and \(\Gamma\). Depending on this choice, the number of 
common atoms between the partitioned databases will vary; hence, leading to
a better or worse consequence size.\footnote{Realize that the expansion
suggested by Case-Analysis is exponential in the number of atoms on 
which we do the case analysis. Therefore, it is important to choose partitions
that will minimize the common atoms between the partitioned databases.}

As we shall see next, a system structure can play a key role in 
making this partitioning choice. A system structure is a directed acyclic graph 
that explicates the interconnections between system components. When a system
description is augmented with a system structure, we refer to the result
as a structured system description. Structured system descriptions are 
defined formally in the following section, but first the following example
on applying the Intersection Corollary. 

Consider Figure~\ref{fig:ssd-2} where \(\Delta = \Delta_C \cup \Delta_D\),
and let us compute the consequence of the system observation 
\(\phi = C \wedge D\), that is, \(\cons^\Delta(\phi)\). We need to 
construct this consequence from component consequences of the form 
\(\cons^{\Delta_C}(.)\) and \(\cons^{\Delta_D}(.)\). We cannot do this 
immediately, however, since the observation \(\phi\) does not mention 
atom \(A\) which is shared by \(\Delta_C\) and \(\Delta_D\). Therefore,
we can use the Intersection Corollary with \(\S = \{A\}\):
\[ 
\cons^\Delta(\phi) 
\equiv 
[\cons^{\Delta_C}(A \wedge \phi_{\Delta_C}) \wedge 
\cons^{\Delta_D}(A \wedge \phi_{\Delta_D})] \vee 
[\cons^{\Delta_C}(\neg A \wedge \phi_{\Delta_C}) \wedge 
\cons^{\Delta_D}(\neg A \wedge \phi_{\Delta_D})].
\]
Substituting for \(\phi_{\Delta_C} = C\) and \(\phi_{\Delta_D} = D\),
we get:
\[
\cons^\Delta(C \wedge D) 
\equiv 
 [\cons^{\Delta_C}(A \wedge C) \wedge  
  \cons^{\Delta_D}(A \wedge D)] \vee 
 [\cons^{\Delta_C}(\neg A \wedge C) \wedge  
      \cons^{\Delta_D}(\neg A \wedge D)].
\]
The resulting expression contains only component consequences, which we
assume are precomputed. Substituting for the values of these consequences
we get:
\[ \cons^\Delta(C \wedge D) 
   \equiv
   [\neg \ok(X) \wedge \true] \vee
   [\true \wedge \neg \ok(Y)] 
\equiv \neg \ok(X) \vee \neg \ok(Y).
\]

Note that the Intersection Corollary constructs only conjunctions and
disjunctions (no negations). Therefore, if component consequences are
in NNF, then any system consequence constructed using the corollary must
also be in NNF. Moreover, if we ensure that component descriptions do
not share assumables, then we are guaranteed that the resulting NNF
is also decomposable.\footnote{Assuming that component descriptions are
themselves decomposable.} This follows because the Intersection Corollary 
will apply the conjoin operator only to consequences which correspond
to disjoint subsystems, that is, collections of disjoint component
descriptions.

\subsection{Structured System Descriptions} \label{sec:ssd}

We now turn to the formal definition of a structured system description.
We start with the definition of a component description (with respect to 
some assumables \(\A\) and non--assumables \(\P\)).

\begin{definition}[Component Description] \label{def:component}
A component description is a triple \(\cd\) where
\(\I\) is a set of non--assumables;
\(O\) is a non--assumable such that \(O \not \in \I\);
and \(\Delta_O\) is a set of propositional sentences
satisfying the following conditions:
\begin{enumerate}
\item \(\Delta_O\) can only mention assumables in \(\A\) or 
non--assumables in \(\I \cup \{O\}\).

\item Every instantiation of \(\I \cup \A\) is consistent with \(\Delta_O\).
\end{enumerate}
\end{definition}
The second condition above prohibits a component description from specifying
a direct relationship between the inputs of a component and is typically
self imposed.

We are now ready to provide the formal definition of a structured system 
description. We use \(\dag_P\) to denote the parents of node \(P\) in a 
directed acyclic graph \(\dag\).

\begin{definition}[Structured System Description] \label{def:ssd}
A structured system description (SSD) is a tuple \(\ssd\), where 
\(\cP\) and \(\cA\) are sets of atomic propositions such that 
\(\P \cap \A = \emptyset\);
\(\dag\) is a directed acyclic graph over nodes \(\cP\);
\(\Delta\) is a function that maps each node \(P\) in \(\P\) 
into a set of propositional sentences \(\Delta_P\) such that
\((\dag_P,P,\Delta_P)\) is a component description.
Here, \(\cP\) is called the set of non--assumables;
\(\cA\) is called the set of assumables; 
\(\dag\) is called the system structure.
It is required that no assumables be shared between component descriptions.
\end{definition}
We shall overload the meaning of \(\Delta\) and use it 
to denote \(\bigcup_{P \in \P} \Delta_P\) (the union of all component 
descriptions).

The last requirement in Definition~\ref{def:ssd} ensures the decomposability
of generated consequences and does not limit the expressive power of 
structured system descriptions. Specifically, one can always ensure that 
component descriptions do not share assumables,
but at the expense of adding auxiliary nodes to the system structure.
See Appendix~\ref{app:sharing} for details.

Each structured system description \(\ssd\) induces a system
description \(\sd\) according to Definition~\ref{def:sd}:

\begin{theorem} \label{theo:sd-ssd}
If \(\ssd\) is a structured system description, then 
\(\sd\) is a system description.
\end{theorem}
That is, if \(\ssd\) is a structured system description, then
every \(\A\)--instantiation is consistent with database \(\Delta\).
This also means that the database of a structured system description
is guaranteed to be consistent by construction. Note that this global
consistency is guaranteed given only local conditions on component
descriptions. 

We close this section by noting that a structured system description as 
defined here is the diagnosis special-case of a {\em symbolic causal network} 
which we introduced elsewhere \cite{darwicheAAAI94}. 




\section{Structure-Based Computation of Consequences} 
\label{sec:algorithm}

A main message of the previous section is that composing a system consequence 
from component consequences is straightforward, as long as we are not concerned 
about the size of the resulting consequence. Specifically, given that component 
consequences are precomputed, one can compute a system consequence by successive 
applications of 
the Intersection Corollary. In practice, however, the size of the resulting 
consequence is a key concern because it affects the time needed to generate 
the consequence, the space needed to store it, and the time needed to extract 
from it the minimal diagnoses.

Therefore, we shall present in this section a method for
composing a system consequence from component consequences while 
trying to minimize the size of the resulting consequence. This method 
rests on partitioning component descriptions using a {\em jointree}: a tree
of hypernodes that results from graphically transforming the system structure.
In particular,
\begin{itemize}
\item[-] we present in Section~\ref{sec:jt} jointrees and show how they can
be used to partition component descriptions;
\item[-] we then present in Section~\ref{sec:cc} an algorithm for computing 
component consequences which are the building blocks of system consequences; and
\item[-] finally, we present in Section~\ref{sec:sc} an algorithm for computing 
system consequences using component consequences and a jointree.
\end{itemize}

\subsection{Partitioning Component Descriptions using Jointrees} 
\label{sec:jt}

\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\vspace{.5cm}
\begin{center}
\mbox{\epsfxsize=85mm \leavevmode \epsffile{ssd-3.eps}}
\end{center}

{\tiny
\begin{center}
\begin{tabular}{c|c|c|c}
\(\Delta_A, \Delta_B\) & \(\Delta_C \) & \(\Delta_D\) & \(\Delta_E\) \\ \hline
& & & \\
\(\{\}\) & 
\(\left\{\begin{array}{rcl}
A \wedge \ok(X) & \imply & \neg C \\
\neg A \wedge \ok(X) & \imply & C
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
(A \vee B) \wedge \ok(Y) & \imply & D \\
\neg (A \vee B) \wedge \ok(Y) & \imply & \neg D
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
(C \wedge D) \wedge \ok(Z) & \imply & E \\
\neg (C \wedge D) \wedge \ok(Z) & \imply & \neg E
\end{array}\right\}\) 
\end{tabular}
\end{center}
}
\end{minipage}
}
\end{center}
\caption{A structured system description of a digital circuit. 
\label{fig:ssd-3}}
\end{figure}

A jointree \(\tree\) is constructed for a given directed acyclic
graph \(\dag\). The nodes of a jointree are called {\em clusters} 
or {\em cliques} and they represent sets of nodes in the graph \(\dag\). 
Figure~\ref{fig:jt1} contains a jointree for the system structure 
(directed acyclic graph) in Figure~\ref{fig:ssd-3}. 
The {\em sepset} of any adjacent 
cliques \(\cluster_i\) and \(\cluster_j\) in a jointree is defined as their
intersection \(\cluster_i \cap \cluster_j\) and is denoted by 
\(\sepset_{ij}\). 

There are two conditions that must be satisfied by a jointree:
\begin{enumerate}
\item The ports of each component must belong to some clique 
in the jointree. 

\item If a node belongs to two cliques, it must also belong to every 
clique on the path between them. This is called the {\em jointree property.} 
\end{enumerate}

\begin{figure}
\begin{center}
\mbox{\epsfxsize=150mm \leavevmode \epsffile{trees.eps}}
\end{center}
\caption{(a) a tree \(\tree\); (b) a subtree \(\tree_{53}\); 
(c) the partitioning of \(\tree\) around clique \(\cluster_5\).
\label{fig:trees}}
\end{figure}

We partition component descriptions using a jointree by assigning 
each component to a clique that contains the ports of that component. 
We will use \(\comp(\cluster)\) to denote the components 
assigned to clique \(\cluster\) and refer to the function \(\comp\) as 
a {\em component assignment} for \((\dag,\tree)\). Note that a component 
assignment 
is not unique. The literature on probabilistic reasoning contains 
heuristics for choosing a component assignment, but they are outside 
the scope of this paper \cite{darwicheIJAR96,jensen90}.

To see how jointrees are used to generate consequences,
we need the following notation. Let \(\tree\) be a jointree and let 
\(\tree_{ij}\) denote the subtree that continues to include clique 
\(\cluster_i\) after deleting the arc \(\cluster_i \uarc \cluster_j\) 
from \(\tree\). For example, Figure~\ref{fig:trees}(a) depicts a jointree 
\(\tree\) and Figure~\ref{fig:trees}(b) depicts the subtree \(\tree_{53}\).

Now, each clique \(\clique_i\) in a jointree partitions the jointree into
clique \(\clique_i\) and a number of subtrees \(\tree_{ji}\) where 
\(\clique_j\) is a neighbor of \(\clique_i\). Moreover, by the jointree
property, clique \(\clique_i\) is guaranteed to contain all atoms that are 
shared by any two subtrees \(\tree_{ji}\). Therefore, each clique 
\(\clique_i\) can be viewed as partitioning components into those assigned 
to \(\clique_i\) and those assigned to subtrees \(\tree_{ji}\). For example, 
one can partition the jointree in Figure~\ref{fig:trees}(a) into 
clique \(\cluster_5\) and the subtrees \(\tree_{35}\), \(\tree_{45}\), 
\(\tree_{65}\) and \(\tree_{75}\) as shown in Figure~\ref{fig:trees}(c).
Moreover, any atom that is shared by two subtrees \(\tree_{x5}\) and 
\(\tree_{y5}\) must belong to clique \(\cluster_5\). Therefore, the atoms of 
this clique make a very good candidate for being the set \(\S\) in 
the Intersection Corollary; that is, the atoms on which to perform
case analysis. If we apply the Intersection Corollary with this choice
of \(\S\), we will decompose a system consequence (one with respect to
the components of \(\tree\)) into a number of consequences some of which 
are with respect to the components assigned to clique \(\clique_5\), the 
others are with respect to the components assigned to subtrees 
\(\tree_{35}\), \(\tree_{45}\), \(\tree_{65}\) and \(\tree_{75}\). 
Each one of the resulting consequences is with respect to a smaller
system, and the decomposition process can continue recursively until we
reach boundary conditions, where each consequence is with respect to
the components assigned to a clique. 
Clique consequences can be computed easily from the consequences
of components assigned to them. More details on this will be given in 
Section~\ref{sec:sc} where we provide the pseudocode for an algorithm
based on this decomposition process.

We shall close this section by explaining why the partition induced 
by a jointree is better than an arbitrary one. The answer is simple: the 
optimization criterion for constructing jointrees attempts to minimize the 
size of cliques. Therefore, the optimization criterion for constructing 
jointrees attempts to minimize the atoms on which to perform case analysis
when applying the Intersection Corollary, therefore, attempting to 
minimize the size of the resulting consequence. For a detailed, 
self--contained discussion on the construction of jointrees, the reader is 
referred to \cite{darwicheIJAR96}.

\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\vspace{.5cm}
\begin{center}
\mbox{\epsfxsize=70mm \leavevmode \epsffile{jt1.eps}}
\end{center}
{\tiny
\begin{center}
\begin{tabular}{c|c|c}
\(\Delta_1 = \Delta_A \cup \Delta_B \cup \Delta_D\) & 
\(\Delta_2 = \Delta_C\) & \(\Delta_3 = \Delta_E\) \\ \hline
& & \\
\(\left\{\begin{array}{rcl}
(A \vee B) \wedge \ok(Y) & \imply & D \\
\neg (A \vee B) \wedge \ok(Y) & \imply & \neg D
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
A \wedge \ok(X) & \imply & \neg C \\
\neg A \wedge \ok(X) & \imply & C
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
(C \wedge D) \wedge \ok(Z) & \imply & E \\
\neg (C \wedge D) \wedge \ok(Z) & \imply & \neg E
\end{array}\right\}\) 
\end{tabular}
\end{center}
}
{\footnotesize
\(\comp(\clique_1) = \{A,B,D\}\); 
\(\comp(\clique_2) = \{C\}\); and
\(\comp(\clique_3) = \{E\}\).
}
\end{minipage}
}
\end{center}
\caption{On the left, a jointree for the structured system description 
of Figure~\protect{\ref{fig:ssd-3}}. On the right, the same jointree
with sepsets shown on each arc. The table shows the component descriptions,
\(\Delta_i\), that are assigned to clique \(\clique_i\).
\label{fig:jt1}}
\end{figure}


\subsection{Computing Component Consequences} \label{sec:cc}

In addition to constructing a jointree and a component assignment,
we must compute component consequences before we can compute
system consequences. In particular, for a given component description
\(\cd\), we need to compute \(\cons^{\Delta_O}_\A(\gamma)\) for every 
instantiation \(\gamma\) of the atoms \(\I \cup \{O\}\). That is, for every
possible state \(\gamma\) of the component ports, \(\I \cup \{O\}\), 
we must compute and store the strongest conclusion,
\(\cons^{\Delta_O}_\A(\gamma)\), 
we can draw about the health of that component.

This is accomplished by the algorithm in Figure~\ref{fig:cc} which is a 
direct implementation of the Component-Consequence Theorem in
Section~\ref{sec:ccc}. The algorithm assumes that each clause \(\alpha\) in 
the component description \(\Delta_O\) is decomposed into two parts, one 
containing only assumables, \(\alpha_\A\), and another containing only 
non--assumables, \(\alpha_\P\). It returns an array whose indices correspond
to instantiations of the atoms \(\I \cup \{O\}\) and whose entries are
component consequences. 

Please note that we use integers to represent instantiations, a technique
that we detail in Appendix~\ref{app:insts}. This appendix provides two key 
functions, one for computing a unique index for each instantiation and 
another for generating all instantiations of a given set of atoms. 
These functions are used in the pseudocode of Figure~\ref{fig:cc}.

\begin{figure}[tb]
{\small
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\begin{center}
\underline{{\bf Computing Component Consequences}}
\end{center}
\vspace{.25cm}
{\bf Input:} A component description \(\cd\). 
The database \(\Delta_O\) consists of pairs \((\alpha_\P,\alpha_\A)\) where 
\(\alpha_\P\) is a set of \(\P\)-literals and \(\alpha_\A\) is a set of 
\(\A\)--literals. The pair \((\alpha_\P,\alpha_\A)\) represents the 
disjunction of literals in \(\alpha_\P \cup \alpha_\A\).
\vspace{.5cm}

{\bf Output:} An array whose indices are \(0, \ldots, 2^{\mid \I \mid +1}-1\) 
and whose elements are nodes in an NNF-graph.

\vspace{.5cm}
{\bf Pseudocode:} 
\begin{tabbing}
{\sc co}\={\sc mponent-consequence} \\
   \>01.  fo\=r every \(\gamma\) in \(\ginstantiations(\I \cup \{O\})\) do \\
   \>02.  \>{\sc as}\={\sc sert}\((\gamma)\) \\
   \>03.  \>\>\(l \set \vindex(\I \cup \{O\})\) \\
   \>04.  \>\>\(\ccons_O[l] \set \ganode\) \\
   \>05.  \>\> fo\=r every pair \((\alpha_{\P},\alpha_{\A})\) in \(\Delta_O\) do \\
   \>06.  \>\>  \>wh\=en \(\empty(\alpha_{\P} \cap \gamma)\) do     {\em \{the clause 
\(\alpha_\P\) is inconsistent with the instantiation \(\gamma\)\}} \\
   \>07.  \>\>  \> \>\(\addchild(\ccons_O[l],\cdisj(\alpha_{\A}))\) \\
   \>08.  \>\(\retract(\gamma)\) \\
   \>09. return \(\ccons_O\)
\end{tabbing}
\begin{tabbing}
{\sc cr}\={\sc eat\_disjunction}(\(\L\)) \\
   \>01. \(\resa \set \gonode\) \\
   \>02. fo\=r every literal \((V,v)\) in \(\L\) do \\
   \>03.   \>\(\addchild(\resa,\glnode(V,v))\) \\
   \>04. return \(\resa\)
\end{tabbing}

\end{minipage}
}
\end{center}
}
\caption{An algorithm for computing component consequences. 
\label{fig:cc}}
\end{figure}


The soundness of the algorithm in Figure~\ref{fig:cc} is given below:

\begin{theorem} \label{theo:cc-sound}
The array \(\ccons_O\) computed in Figure~\ref{fig:cc} satisfies the
following property:
\[ 
\ccons_O[l] \equiv \cons^{\Delta_O}_{\A}(\gamma)
\]
for every instantiation \(\gamma\) of \(\I \cup \{O\}\) and
its corresponding index \(l\).
\end{theorem}

Figure~\ref{fig:example-cc} provides a detailed example showing 
how the algorithm of Figure~\ref{fig:cc} is used to compute the 
consequences of a 2-input or-gate. The number of computed consequences
in this example is eight, which is \(2^{2+1}\), since the component
has two inputs and one output. Each component consequence,
\(\cons^{\Delta_D}_\A(\gamma)\), in this example is equivalent to either 
\(\true\) or \(\neg \ok(Y)\) depending on whether the instantiation 
\(\gamma\) of atoms \(\{A,B,D\}\) is consistent with the expected behavior 
of the or-gate.

The following theorem shows that computing component
consequences is exponential in the number of component ports,
but is linear in the number of clauses in its description.

\begin{theorem} \label{theo:cc-complexity}
The time and space complexity of \compcons\ is \(O(s n 2^n)\) 
where \(s\) is the number of pairs in database \(\Delta_O\) and \(n\) 
is the number of atoms in \(\I \cup \{O\}\).
\end{theorem}
Therefore, as long as the number of inputs to a component is small enough,
computing component consequences can be considered to take constant time.
Given this complexity result, one should attempt to minimize the number of
inputs per component. Bear in mind that components are conceptual
constructs and need not strictly correspond to physical components in the 
system. For example, one may opt to view an \(n\)-input and-gate as a number 
of cascaded
2-input and-gates. This will reduce the complexity of computing component
consequences from \(O(s n 2^n)\) to \(O(s)\); a significant
improvement.\footnote{In such a case, however, the technique that we 
discuss in Appendix~\ref{app:sharing} must be used to ensure that the 
descriptions of these 2-input components do not share assumables.}


\begin{figure}
{\footnotesize
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\begin{center}
\underline{{\bf An Example of Algorithm \compcons}}
\end{center}
\vspace{.4cm}
Consider the following component description, \((\{A,B\},D,\Delta_D)\),
of a 2-input or-gate where 
\[
\Delta_D = 
\left\{
\begin{array}{c}
\neg A \wedge \neg B \wedge \ok(Y) \imply \neg D \\
A \wedge \ok(Y) \imply D \\
B \wedge \ok(Y) \imply D
\end{array} 
\right\}.
\]
Algorithm \compcons\ requires the following representation of \(\Delta_D\):
\[
\left\{
\begin{array}{c}
(\:\{\:(A,1), (B,1), (D,0)\:\},\:\{\:(\ok(Y),0)\:\}\:) \\
(\:\{\:(A,0), (D,1)\:\},\:\{\:(\ok(Y),0)\:\}\:) \\
(\:\{\:(B,0), (D,1)\:\},\:\{\:(\ok(Y),0)\:\}\:) 
\end{array} 
\right\},
\]
where each clause is represented as a pair of clauses, one containing 
only non-assumables and the other containing only assumables.
Calling \compcons\ on this component description returns the 
following array (first two columns):
\begin{center}
\begin{tabular}{|c|c|||c|c|}
\hline
index & \(\ccons_D\) & \(\gamma\) & \(\cons^{\Delta_D}_\A(\gamma)\)\\ 
\hline \hline
& & & \\
0 & 
\mbox{\epsfxsize=20mm 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/true.eps}} &
\(\neg A \wedge \neg B \wedge \neg D\) & \(\true\) \\ 
1 & 
\mbox{\epsfxsize=20mm 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/oky.eps}} &
\(A \wedge \neg B \wedge \neg D\) & \(\neg \ok(Y)\) \\
2 & 
\mbox{\epsfxsize=20mm 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/oky.eps}} &
\(\neg A \wedge B \wedge \neg D\) & \(\neg \ok(Y)\) \\
3 & 
\mbox{\epsfxsize=30mm 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/okyy.eps}} &
\(A \wedge B \wedge \neg D\) & \(\neg \ok(Y)\) \\
4 &
\mbox{\epsfxsize=20mm 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/oky.eps}} &
\(\neg A \wedge \neg B \wedge D\) & \(\neg \ok(Y)\) \\
5 & 
\mbox{\epsfxsize=20mm 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/true.eps}} &
\(A \wedge \neg B \wedge D\) & \(\true\) \\
6 & 
\mbox{\epsfxsize=20mm 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/true.eps}} &
\(\neg A \wedge B \wedge D\) & \(\true\) \\
7 & 
\mbox{\epsfxsize=20mm 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/true.eps}} &
\(A \wedge B \wedge D\) & \(\true\) \\
\hline
\end{tabular}
\end{center}
\end{minipage}
}
\end{center}
}
\caption{Computing consequenes of an or-gate with inputs 
\(\{A,B\}\) and output \(D\).
\label{fig:example-cc}}
\end{figure}



\subsection{Computing System Consequences} \label{sec:sc}


\begin{figure}[ph]
{\small
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\begin{center}
\underline{{\bf Computing System Consequences}}
\end{center}
\vspace{.5cm}

{\bf Input:} 
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item [-] \(\ssd\): a structured system description;
\item [-] \(\phi\): an instantiation of some atoms \(\E \subseteq \P\);
\item [-] \(\tree\): a join tree for system structure \(\dag\);
\item [-] \(\comp\): a component assignment for \((\dag,\tree)\);
\item [-] \(\ccons_O\): a component consequence array for each component 
\(O\) --- computed using the algorithm in Figure~\ref{fig:cc};
\item [-] \(\cluster_z\): an arbitrary cluster in the tree \(\tree\) 
(pivot cluster).
\end{list}
\vspace{.5cm}
{\bf Output:} An NNF-graph over assumables \(\A\).
\vspace{.5cm}

{\bf Data Structures:} For each neighboring clusters 
\((\cluster_x,\cluster_y)\) in the join tree \(\tree\):
\begin{enumerate}
\item[-] a sepset \(\sepset_{xy} = \cluster_x \cap \cluster_y\); and
\item[-] a hash table \(\cache_{xy}\) which contains NNF-graph nodes.
\end{enumerate}
The keys of \(\cache_{xy}\) are \(0, \ldots, 2^{\mid \sepset_{xy} \mid}-1\).
\(\cache_{xy}[l]\) is the element having \(l\) as a key.

\vspace{.5cm}


{\bf Pseudocode:} 
\begin{tabbing}
{\sc sy}\={\sc stem\_consequence} \\
    \>01. add cluster \(\cluster_{0} = \emptyset\) as a
            neighbor of \(\cluster_z\) \\
    \>02. \(\assert(\phi)\) \\
    \>03. \(\strcons(\cluster_z,\cluster_{0})\)
\end{tabbing}
\begin{tabbing}
{\sc su}\={\sc btree\_consequence}(\(\cluster_i,\cluster_j\)) \\ 
    \>00. \(l \set \vindex(\sepset_{ij})\) \\
    \>01. \(\mu \set \cache_{ij}[l]\); if \(\mu \neq {\sc nil}\) then return \(\mu\) \\
   \>02.  \(\resa \set \gonode\) \\
   \>03.  fo\=r every \(\alpha\) in \(\ginstantiations(\cluster_i)\) do \\
   \>04.  \>{\sc as}\={\sc sert}\((\alpha)\) \\   
   \>05.  \>\>\(\resb \set \ganode\) \\
   \>06.  \>\> \(\addchild(\resb, \clscons(\cluster_i))\) \\
   \>07.  \>\>fo\=r every neighboring cluster \(\cluster_k\) of \(\cluster_i\) where \(k \neq j\) do \\
   \>08.  \>\>\>\(\addchild(\resb, \strcons(\cluster_k,\cluster_i))\) \\
   \>09.  \>\>\(\addchild(\resa, \resb)\) \\
   \>10.  \>\(\retract(\alpha)\) \\
   \>11.  \(\cache_{ij}[l] \set \resa\); return \(\resa\) 
\end{tabbing}
\begin{tabbing}
{\sc cl}\={\sc uster\_consequence}(\(\cluster_i\)) \\
   \>01. \(\resb \set \ganode\) \\
   \>02. fo\=r every component \(O\) (with inputs \(\I\)) in \(\comp(\cluster_i)\) do\\
   \>03. \>\(\addchild(\resb, \ccons_O[\vindex(\I \cup \{O\})])\) \\
   \>04. return \(\resb\)
\end{tabbing}
\end{minipage}
}
\end{center}
}
\caption{An algorithm for computing a system consequence given a 
system observation.
\label{fig:sc}}
\end{figure}


Given that we have
\begin{enumerate}
\item [-] constructed a jointree;
\item [-] chosen a component assignment;
\item [-] computed component consequences;
\end{enumerate}
we are now ready to compute system consequences. All we need is to
apply the Intersection Corollary successively until we decompose
the system consequence into a number of component consequences which
can be simply looked-up from the arrays that are computed by the
algorithm of Figure~\ref{fig:cc}.

To apply the Intersection Corollary, we need a pivot clique which
is given as input to the algorithm in Figure~\ref{fig:sc}.
The algorithm has two main functions, one for computing a consequence with 
respect to the components assigned to a clique and another for 
computing a consequence with respect to the components assigned 
to a subtree. Let us consider the function for computing clique 
consequences first:

\begin{lemma} \label{lem:sc-a}
When \(\clscons(\clique_i)\) is called, atoms \(\clique_i\) are 
guaranteed to be instantiated to some \(\alpha\) and the call returns a 
sentence equivalent to \(\cons^{\Delta_i}_{\A}(\phi_i \wedge \alpha)\) where 
\begin{itemize}
\item[-] \(\Delta_i\) is the union of all component descriptions assigned 
to clique \(\clique_i\); and
\item[-] \(\phi_i\) is the projection of system 
observation \(\phi\) on the atoms in clique \(\clique_i\).
\end{itemize}
\end{lemma}
This function is simple; it directly applies the Decomposition theorem to
decompose a clique consequence into the conjunction of component consequences
(which are provided as input to the algorithm). 

The second function of the algorithm computes a consequence with respect
to the components assigned to a subtree \(\tree_{ij}\):
\begin{lemma} \label{lem:sc-b}
When \(\strcons(\clique_i,\clique_j)\) is called, atoms \(\sepset_{ij}\)
are guaranteed to be instantiated to some \(\beta\) and the call returns a 
sentence equivalent to \(\cons^{\Delta_{ij}}_{\A}(\phi_{ij} \wedge \beta)\) 
where 
\begin{itemize}
\item[-] \(\Delta_{ij}\) is the union of all component descriptions assigned to
cliques in subtree \(\tree_{ij}\); and
\item[-] \(\phi_{ij}\) is the projection of system observation \(\phi\) on 
the atoms in subtree \(\tree_{ij}\).
\end{itemize}
\end{lemma}
This function is more involved since it calls \clscons\ and itself 
recursively. 

Note that the results returned by this function are cached since the function
may be called more than once with the same arguments and the same 
instantiation of sepset \(\sepset_{ij}\).\footnote{This is because the same
instantiation of a sepset \(\sepset_{ij}\) may appear as part of many
instantiations of clique \(\clique_i\).} In such a case, the result
is looked up from the cache instead of being recomputed. This caching of 
results explains why the generated consequence has the form of a
directed acyclic graph instead of a tree.

Given the function \strcons, one can compute the
system consequence by adding a dummy clique \(\clique_{0} = \emptyset\) 
as a neighbor to the pivot clique \(\clique_z\) to generate an extended
jointree \(\tree'\). The subtree \(\tree'_{z0}\) of this extended tree
\(\tree'\) will be nothing but the original jointree \(\tree\). The call to 
\(\strcons\) on line~03 of \(\syscons\) will then return the system 
consequence.
This is stated more explicitly by the following theorem:

\begin{theorem} \label{theo:sc-sound}
The function \syscons\ in Figure~\ref{fig:sc} will always terminate returning
a sentence which is equivalent to \(\cons^{\Delta}_{\A}(\phi)\).
\end{theorem}

Figure~\ref{fig:example-sc} contains a detailed example showing how
the algorithm in Figure~\ref{fig:sc} is used to generate a system
consequence for a given observation and structured system description.
Note that the computed consequence in this example is equivalent to 
\(\neg \ok(X) \vee \neg \ok(Z)\).


\begin{figure}[ph]
{\small
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\begin{center}
\underline{{\bf An Example of Algorithm \syscons}}
\end{center}
\vspace{.25cm}
Consider the jointree and component assignment given in Figure~\ref{fig:jt1}.
Consider also the following component consequence arrays:
\begin{center}
{\tiny
\begin{tabular}{|c||c|c|}
\hline
\(\gamma\) & & \(\ccons_C\) \\ \hline \hline
\(\neg A \wedge \neg C\) & 0 & \((\ok(X),0)\) \\
\(A \wedge \neg C\) & 1 & \(\true\) \\
\(\neg A \wedge C\) & 2 & \(\true\) \\
\(A \wedge C\) & 3 & \((\ok(X),0)\) \\
\hline
\end{tabular}
\begin{tabular}{|c||c|c|}
\hline
\(\gamma\) & & \(\ccons_D\) \\ \hline \hline
\(\neg A \wedge \neg B \wedge \neg D\) & 0 & \(\true\) \\
\(A \wedge \neg B \wedge \neg D\) & 1 & \((\ok(Y),0)\) \\
\(\neg A \wedge B \wedge \neg D\) & 2 & \((\ok(Y),0)\) \\
\(A \wedge B \wedge \neg D\) & 3 & \((\ok(Y),0)\) \\
\(\neg A \wedge \neg B \wedge D\) & 4 & \((\ok(Y),0)\) \\
\(A \wedge \neg B \wedge D\) & 5 & \(\true\) \\
\(\neg A \wedge B \wedge D\) & 6 & \(\true\) \\
\(A \wedge B \wedge D\) & 7 & \(\true\) \\
\hline
\end{tabular} 
\begin{tabular}{|c||c|c|}
\hline
\(\gamma\) & & \(\ccons_E\) \\ \hline \hline
\(\neg C \wedge \neg D \wedge \neg E\) & 0 & \(\true\) \\
\(C \wedge \neg D \wedge \neg E\) & 1 & \(\true\) \\
\(\neg C \wedge D \wedge \neg E\) & 2 & \(\true\) \\
\(C \wedge D \wedge \neg E\) & 3 & \((\ok(Z),0)\) \\
\(\neg C \wedge \neg D \wedge E\) & 4 & \((\ok(Z),0)\) \\
\(C \wedge \neg D \wedge E\) & 5 & \((\ok(Z),0)\) \\
\(\neg C \wedge D \wedge E\) & 6 & \((\ok(Z),0)\) \\
\(C \wedge D \wedge E\) & 7 & \(\true\) \\
\hline
\end{tabular}
}
\end{center}
Calling \syscons\ with the observation \(\phi\) as \(\{(A,1), (E,1)\}\) and 
the pivot cluster as \(\cluster_1\), we get the following consequence
(in decomposable negation normal form):
\begin{center}
\mbox{\epsfxsize=120mm \leavevmode 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/ssd-3-ae.eps}}
\end{center}
The resulting consequence can be simplified significantly and easily.
One way to realize this simplification is to use an optimized version of
{\sc add-child} in Appendix~\ref{app:nnfs} which performs the necessary 
simplifications as it adds a child to a node.
\end{minipage}
}
\end{center}
}
\caption{An example showing the application of algorithm~\syscons. We have
numbered or-nodes in the consequence to facilitate the depiction of 
structure sharing without having to draw cross arcs.
\label{fig:example-sc}}
\end{figure}


The consequences computed by the algorithm in Figure~\ref{fig:sc} are
guaranteed to be in decomposable negation normal form as long as
component consequences are in that form.

\begin{theorem}\label{theo:sc-form}
In Figure~\ref{fig:sc}, if each component consequence \(\ccons_O[.]\) 
is in decomposable NNF, the sentence returned by the function 
\syscons\ will be in decomposable NNF.
\end{theorem}
Note that the 
consequences computed by \compcons\ in Figure~\ref{fig:cc} are not
guaranteed to be in decomposable NNF. However, they are guaranteed to be
in CNF. We can simply transform them into DNF and, hence, into 
decomposable NNF.

\section{The Complexity of Computing Consequences}
\label{sec:complexity}

We now turn to the discussion of computational complexity:

\begin{theorem} \label{theo:sc-complexity}
Consider the algorithm \syscons\ in Figure~\ref{fig:sc}. The time and space 
complexity of this algorithm is 
\[ O(\sum_{\clique \in \tree} 
\mid \clique \mid 2^{\mid \clique \setminus \E\mid}),\]
where \(\clique\) denotes a clique in the jointree \(\tree\).
\end{theorem}
The complexity is then linear in the number of cliques, but exponential
in their sizes.

Consider all jointrees of a given graph \(\dag\), and select the tree 
\(\tree\) with the smallest maximal clique. The size of the maximal clique 
in such a tree minus one is known as the width \(w^*\) of graph \(\dag\)
\cite{dechter92,dechter89}. Theorem~\ref{theo:sc-complexity} is then saying 
that the computational complexity of a consequence is exponential in the 
width \(w^*\) of the given system structure \(\dag\).
But this complexity result is for the worst case --- the best and average 
cases are different.

\subsection{The Effect of Observations}

According to Theorem~\ref{theo:sc-complexity}, the time and space
complexity are exponential not in the size of cliques, but in the size
of cliques after we have removed from them atoms \(\E\) that appear in the
observation \(\phi\). At one extreme, the observation \(\phi\) is 
\(\true\) (\(\E = \emptyset\)) in which case the algorithm is exponential 
in the size of the 
maximal clique. At another extreme, the observation \(\phi\) is an 
instantiation of all non--assumables (\(\E = \P\)). 
In such a case, the algorithm does not depend on the size of cliques and
is only linear in the number of such cliques. This can be seen
by observing line~02 of algorithm
\syscons\ where all atoms in the system structure
are instantiated. This means that the result of any call to 
\(\ginstantiations\) will return a singleton. Hence, every constructed 
or-node on line~02 of \(\strcons\) will
have exactly one child. Moreover, the number of calls to \strcons\ will
be exactly the number of edges in the jointree and the number of calls 
to \clscons\ will be exactly the number of cliques in the jointree.


\begin{figure}[tbp]
\begin{center}
\mbox{\epsfxsize=75mm \leavevmode 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/ssd-3-ae.eps}}
\mbox{\epsfxsize=75mm \leavevmode 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/ssd-3-abe.eps}}

\mbox{\epsfxsize=75mm \leavevmode 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/ssd-3-abce.eps}}
\mbox{\epsfxsize=75mm \leavevmode 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/ssd-3-abcde.eps}}
\end{center}
\caption{Four consequences corresponding to four different observations.
\label{fig:obs}}
\end{figure}

The effect of observations on the computational complexity of consequences
is illustrated in Figure~\ref{fig:obs} which depicts four consequences
with respect to the system in Figure~\ref{fig:ssd-3}. The consequences
correspond to the following observations:
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item [-] \(\phi_1 = A \wedge E\);
\item [-] \(\phi_2 = A \wedge B \wedge E\);
\item [-] \(\phi_3 = A \wedge B \wedge C \wedge E\); and
\item [-] \(\phi_4 = A \wedge B \wedge C \wedge \neg D \wedge E\).
\end{list}
Clearly, observation \(\phi_i\) is stronger than observation \(\phi_{i-1}\).
Interestingly enough, 
the consequence of \(\phi_i\) is a subset of the consequence 
of \(\phi_{i-1}\). Moreover, the subset is obtained by eliminating some 
children of or-nodes, which corresponds to considering fewer cases when 
applying Case-Analysis.\footnote{This observation is the basis of an
approach for compiling devices into parameterized NNFs, which is described
in \cite{darwicheKR98}.}

Because of this dependence on observations, the presented algorithm for 
generating consequences will do very well in applications where the system 
is strongly observed. We have experienced this ourselves when we applied
this framework to discrete event systems which are typically strongly
observed \cite{darwicheDX96,darwicheAAAI97}. Even when the system is
not strongly observed, Theorem~\ref{theo:sc-complexity} is useful in
deciding which observations would be most rewarding computationally. 

A more dramatic effect of the system observation on complexity is obtained
by cutting outgoing arcs of observed nodes from the system structure. This
technique may actually reduce the \(w^*\) of the given system structure 
and is illustrated in Appendix~\ref{app:arcs}, together with some
experimental results that show its effectiveness.


\subsection{Tree System Structures} \label{sec:trees}

An important special case of the presented algorithm is when the system 
structure \(\dag\) that we start with is already a tree --- that is, only 
one undirected path exists between any two nodes in \(\dag\) 
(see Figure~\ref{fig:jt-for-tree}). 
In this case, one can always 
construct a jointree in which 
(a) each clique contains only a node and its parents in \(\dag\); and 
(b) each sepset contains only one node.
In particular, for each node \(N\) in the system structure \(\dag\), we 
construct a clique which contains the family of \(N\) (that is, 
\(\{N\}\cup\dag_N\)). We then connect the clique corresponding to \(N\) 
with the cliques corresponding its neighbors, eliminating any cliques that
are contained in their neighbors. The
result is guaranteed to be a jointree. Figure~\ref{fig:jt-for-tree} 
contains a jointree of a tree system structure.
More details on this construction can be found in \cite{shachter94}. 

\begin{figure}[tb]
\begin{center}
\mbox{\epsfxsize=100mm \leavevmode \epsffile{jt-for-tree.eps}}
\end{center}
\caption{On the left, a system structure with no cycles. On the right, a 
corresponding jointree.
\label{fig:jt-for-tree}}
\end{figure}

Therefore, when the system structure is a tree, the time and space complexity 
of computing a consequence are exponential only in the size of a family. 
Because of this result, one should attempt to construct tree system structures 
whenever possible. Moreover, special care must be exercised to 
avoid large families in such structures. For example, one should model 
\(n\)-input gates 
as a cascaded set of 2-input gates whenever possible. If a tree system structure is 
not possible, one should attempt to engineer the structure so as to minimize the 
size of cliques in its corresponding jointrees.

Although tree system structures are computationally easy, non-tree structures 
are not necessarily hard \cite{fattah-10}. In fact, it is possible to obtain a linear 
complexity even if the system structure is not a tree. Consider for example \(n\)-bit
adders which are constructed form cascading full adders. These adders have
non-tree structures, but it is shown in \cite{fattah-10} that they have jointrees
which grow linearly in the number of bits \(n\). Therefore, the consequences
corresponding to these systems grow linearly in the number of bits \(n\).


\section{Extracting Minimal Diagnoses} 
\label{sec:extraction}

In this section, we present a method for extracting the minimal diagnoses 
characterized by a consequence. In particular, if the consequence is in 
decomposable NNF, and if the minimality criterion satisfies some general 
conditions, the algorithm we shall present will extract minimal diagnoses 
in time linear in the size of the consequence. 

We start first by stating the required conditions on a minimality criterion
and then introduce the algorithm with some examples. We finally state the
algorithm formally, prove its soundness, and its linear computational
complexity.

\subsection{Cost Functions}

Intuitively, minimal diagnoses are those diagnoses which are 
considered most plausible. One may have many instantiations of assumables 
that are consistent with the system description and observation, but only 
a few of these may be considered most plausible. A common minimality 
criterion is the one based on diagnosis cardinality. 
That is, we simply count the number of \(\neg \ok(.)\)
literals in a diagnosis (cardinality of a diagnosis) and consider the
diagnoses with minimal cardinality to be the most plausible.

We adopt the view that each diagnosis has a cost, and minimal diagnoses
are those with a minimal cost. Moreover, we assume that the cost of 
a diagnosis is obtained by adding up the costs of its literals. This is 
all captured by the following notion of a cost function, which assigns 
costs to literals and instantiations.

\begin{definition} \label{def:costf}
A \underline{cost function} is a tuple \(\pc\) where
\begin{itemize}
\item \(\A\) is a set of atoms;
\item \(\costs\) is a set of costs;

\item \(\oplus\) is a binary operation (addition)
on \(\costs\) which satisfies the following properties:
\begin{enumerate}
\item \(\oplus\) is commutative, associative, and has a zero element 0.
\item For all \(a\) and \(b\) in \(\costs\), either \(a \oplus c = b\) or 
\(b \oplus c = a\) for some unique \(c\).
\item \(a \oplus b = 0\) implies \(a = 0\) and \(b = 0\).
\end{enumerate}
\item \(\cf\) maps each \(\A\)-literal into a cost in \(\costs\), where each 
literal or its negation has cost 0.
\end{itemize}
\end{definition}
The function \(\cf\) is extended to instantiations as follows:
\[ \cf(l_1 \wedge \ldots \wedge l_n) = 
\cf(l_1) \oplus \ldots \oplus \cf(l_n). \]
The conditions we impose on the cost addition function are justified 
as follows. The first condition is to be expected of addition operations.
The second condition ensures that costs are totally ordered; that is,
for any two costs, one can be obtained from the other by adding some cost
to it. The third condition ensures that there are no negative costs so
that we cannot reduce the cost of an instantiation by adding more literals.

A cost function induces an ordering on costs as follows:
\begin{definition}
The ordering relation \(\co\) induced by a cost function \(\pc\) 
is defined as follows: \(a \co b\) iff \(a \oplus c = b\) for some \(c\).
If \(a \co b\) and \(a \neq b\), we write \(a \sco b\).
\end{definition}
That is, if \(b\) is obtained by adding some cost to \(a\), then
\(b\) is greater than or equal to \(a\). Moreover, this induced 
ordering is guaranteed to be a total ordering by virtue of the 
properties we imposed on cost addition:
\begin{theorem} \label{theo:order}
The relation \(\co\) induced by a cost function \(\pc\) is 
a total ordering on \(\costs\).
\end{theorem}

An example of a cost function satisfying the above conditions is 
\((\{0,1,2,\ldots\},+,\kappa)\), where the cost of a literal \(l\),
\(\kappa(l)\), is the order-of-magnitude of its probability.\footnote{The 
order-of-magnitude of a probability \(p\), written \(\omp(p)\), is an 
integer such that \(p / \e^{\omp(p)}\) is finite but not infinitesimal 
for an infinitesimal \(\e\) \cite{darwicheUAI94b,goldszmidt92b,spohn87}. 
That is, \(\e^{\omp(p)+1} < p \leq \e^{\omp(p)}\). Note that if \(a\) 
and \(b\) are probabilistically independent, then 
\(\omp(\pr(a b)) = \omp(\pr(a)) + \omp(\pr(b))\).}

Another example of a cost function is the minimum cardinality criterion,
which is widely used in the diagnosis literature. The criterion is specified 
by \((\{0,1,2,\ldots\},+,\mcard)\), where \(\mcard(l) = 1\) if the 
literal \(l\) designate a fault and \(\mcard(l) = 0\) otherwise. 

Note that the triple \(([0,1],*,\pr)\), where the cost of a literal is 
its probability, is not a legitimate cost function according to the
conditions stated above. The cost addition function \(*\) has 1 as its zero 
element in this case. Therefore, the condition \(\pr(l) = 1\) or 
\(\pr(\neg l) = 1\) does not necessarily hold for each 
literal \(l\). Note also that the set-inclusion version of diagnosis 
minimality is not covered by our definition of cost functions; this notion,
however, is problematic when fault models are included 
\cite{dekleer:characterizing-diagnoses}.

The reason we require each literal or its negation to have cost 0
is to be able to characterize minimal diagnoses using minimal partial
diagnoses, a property which is not possible in general. For example,
let \(\alpha = \alpha_1 \vee \ldots \vee \alpha_n\) be a disjunction of
partial diagnoses and let \(\alpha'\) be the result of removing
from \(\alpha\) all partial diagnoses that do not have minimal cost. The
above requirement guarantees that \(\alpha\) and \(\alpha'\) characterize 
the same set of minimal diagnoses.\footnote{Consider the following 
counterexample 
with respect to the triple \(([0,1],*,\pr)\) which does not satisfy the above
requirement. Suppose that the assumables are \(\ok(X), \ok(Y), \ok(Z)\) 
and \(\ok(W)\) and their probabilities are \(.9\), \(.9\), \(.7\) and \(.9\), 
respectively. Suppose further that 
\(\alpha = \ok(X) \wedge \ok(Y) \wedge \neg \ok(W) \vee 
\neg \ok(Y) \wedge \ok(Z)\). The first partial diagnosis is less probable
than the second and, therefore, pruning gives
\(\alpha' = \neg \ok(Y) \wedge \ok(Z)\). Note, however, that 
\(\alpha\) characterizes six diagnoses, two of which
\(\ok(X) \wedge \ok(Y) \wedge \ok(Z) \wedge \neg \ok(W)\) and
\(\ok(X) \wedge \neg \ok(Y) \wedge \ok(Z) \wedge \ok(W)\)
are most probable. On the other hand, \(\alpha'\) characterizes four
diagnoses, only one of which 
\(\ok(X) \wedge \neg \ok(Y) \wedge \ok(Z) \wedge \ok(W)\)
is most probable. Therefore, \(\alpha\) and \(\alpha'\) do not characterize
the same set of most probable diagnoses.}


\subsection{The Extraction Algorithm}

The goal of the algorithm that we shall present next is to compute 
diagnoses that are characterized by a consequence \(\tau\) and that have 
a minimal cost compared to other diagnoses characterized by \(\tau\). 

\begin{definition}[Minimal Instantiations]
Let \(\pc\) be a cost function and let \(\tau\) be an \(\A\)-sentence. 
A minimal instantiation of \(\tau\) with respect to \(\pc\) is an
\(\A\)-instantiation \(\alpha\) such that 
\begin{enumerate}
\item \(\alpha \models \tau\); and
\item if \(\beta\) is an \(\A\)-instantiation such that 
\(\beta \models \tau\), then \(\cf(\alpha) \leq_\oplus \cf(\beta)\).
\end{enumerate}
The minimal instantiations of \(\tau\) are denoted by \(\mpi(\tau)\).
\end{definition}

Consider the consequence \(\tau\) in Figure~\ref{fig:example-sc} for an 
example. This consequence is equivalent to \(\neg \ok(X) \vee \neg \ok(Z)\) 
and, therefore, characterizes six diagnoses:
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item[1.] \(\ok(X) \wedge \ok(Y) \wedge \neg \ok(Z)\)
\item[2.] \(\ok(X) \wedge \neg \ok(Y) \wedge \neg \ok(Z)\)
\item[3.] \(\neg \ok(X) \wedge \ok(Y) \wedge \ok(Z)\)
\item[4.] \(\neg \ok(X) \wedge \ok(Y) \wedge \neg \ok(Z)\)
\item[5.] \(\neg \ok(X) \wedge \neg \ok(Y) \wedge \ok(Z)\)
\item[6.] \(\neg \ok(X) \wedge \neg \ok(Y) \wedge \neg \ok(Z)\).
\end{list}
According to the minimum-cardinality cost function where
\(\A = \{\ok(X),\ok(Y),\ok(Z)\}\), the costs of these diagnoses 
are 1, 2, 1, 2, 2, 3, respectively. Therefore, the consequence
characterizes only two minimal diagnoses:
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item[1.] \(\ok(X) \wedge \ok(Y) \wedge \neg \ok(Z)\)
\item[3.] \(\neg \ok(X) \wedge \ok(Y) \wedge \ok(Z)\).
\end{list}
Hence,
\[ \mpi(\tau) = \{\ok(X) \wedge \ok(Y) \wedge \neg \ok(Z),
\neg \ok(X) \wedge \ok(Y) \wedge \ok(Z)\}. \]
The purpose of our algorithm is to compute this set of diagnoses 
given consequence \(\tau\). 


\begin{figure}
{\small
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\begin{center}
\underline{{\bf Computing Minimal Instantiations}}
\end{center}
{\bf Input:}
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item [-] \(\pc\): a cost function;
\item [-] \(\tau\): a decomposable NNF over assumables \(\A\).
\item [-] \(\atoms(\mu,\nu)\): atoms that appear in \(\mu\) but not 
in \(\nu\) for each or-node \(\mu\) and its child \(\nu\).
\end{list}

{\bf Output:} A set of \(\A\)-instantiations.
\vspace{.2cm}

{\bf Data Structures:} For each node \(\mu\) in \(\tau\), two
fields \(\ct(\mu)\) and \(\terms(\mu)\) initialized to {\sc nil.}
\vspace{.2cm}

{\bf Pseudocode:}
\begin{tabbing}
{\sc mi}\={\sc nimal\_instantiations}(\(\tau\)) \\
   \>01. \prune(\(\tau\)) \\
   \>02. \insts(\(\tau\))
\end{tabbing}
\begin{tabbing}
{\sc pr}\={\sc une}(\(\tau\)) \\
   \>01. wh\=en \(\ct(\tau) =\) {\sc nil} do\\
   \>02. \>for each \(\mu \in \children(\tau)\) do \prune(\(\mu\)) \\
   \>03. \>case \=\(\lnode(\tau)\)\=: \(\ct(\tau) \set \cf(\lit(\tau))\) \\
   \>04  \>     \> \(\anode(\tau)\)\>: \(\displaystyle \ct(\tau) \set \bigoplus_{\mu \in \children(\tau)} \ct(\mu)\) \\
   \>05. \>     \> \(\onode(\tau)\)\>: \= \(\displaystyle \ct(\tau) \set \min_{\mu \in \children(\tau)} \ct(\mu)\)\footnote{\(\min\) is defined with respect to the total 
order \(\co\). When applied to an empty set, \(\min\) returns the special symbol \(\infty\) which is bigger than any cost in \(\Sigma\).} \\
   \> \>     \>                   \> \>\(\children(\tau) \set \{\mu : \mu \in \children(\tau) \mbox{ and } \ct(\mu) = \ct(\tau)\}\)
\end{tabbing}
\begin{tabbing}
{\sc in}\={\sc stantiations}(\(\tau\)) \\
   \>01. wh\=en \(\terms(\tau) =\) {\sc nil} do \\
   \>02. \>if \(\ct(\tau)=\infty\), \(\terms(\tau) \set \{\}\); return \\
   \>03. \>for each \(\mu \in \children(\tau)\) do \insts(\(\mu\)) \\
   \>04. \>case \=\(\lnode(\tau)\)\=: 
                         \(\terms(\tau) \set \{\{\lit(\tau)\}\}\) \\
   \>05. \>     \> \(\anode(\tau)\)\>: 
                         \(\displaystyle \terms(\tau) \set \bigcap_{\mu \in \children(\tau)} \terms(\mu)\)\footnote{\(\{\alpha_1, \alpha_2, \ldots, \alpha_n\} \cap \{\beta_1, \beta_2, \ldots, \beta_m\} = \bigcup_{i=1}^n \bigcup_{j=1}^m \{\alpha_i \cup \beta_j\} \).} \\
   \>06  \>     \> \(\onode(\tau)\) \>: \= \(\terms(\tau) \set\) 
      \(\displaystyle \bigcup_{\mu \in \children(\tau)} 
             \extend(\terms(\mu),\atoms(\tau,\mu))\)
\end{tabbing}
\begin{tabbing}
{\sc ex}\={\sc tend}\((\T,\S)\) \\
   \>01. i\=f \(\S = \{\}\) \\
   \>02. \>then return \(\T\) \\
   \>03. \>else \= \(V \set \head(\S)\) \\
   \>04. \> \>\(\displaystyle \Z \set \{ \{(V,v)\}: \:\: \cf((V,v))=0\}\) \\
   \>05. \> \>\(\extend(\T \cap \Z, \rest(\S))\) 
\end{tabbing}
\end{minipage}
}
\end{center}
}
\caption{An algorithm for extracting minimal diagnoses from a decomposable NNF.
\label{fig:extraction}}
\end{figure}

As it turns out, extracting minimal diagnoses from a decomposable negation
normal form is quite simple 
and can be carried out in two steps. In the first step, the consequence is 
pruned to result in a sentence that characterizes the minimal diagnoses only.
In the second step, all instantiations of the pruned consequence are generated,
each of which will then be a minimal diagnosis. 
The algorithm for extracting minimal diagnoses is given in 
Figure~\ref{fig:extraction} and is explained in more detail below:

\subsection*{Phase I: Cost Propagation and Pruning}
Each node in the NNF is assigned a cost as follows:
\begin{enumerate}
\item The cost of a literal is given by the cost function;
\item The cost of a conjunction is the \(\oplus\)-sum of costs assigned to its 
conjuncts;
\item The cost of a disjunction is the minimum of costs assigned to its
disjuncts.
\end{enumerate}
It is shown by Lemma~\ref{lem:pi-sound} in Appendix~\ref{app:proofs} that 
the cost assigned to node \(\mu\) is nothing but the cost of the minimal 
instantiations it characterizes.

In addition to this cost propagation, some pruning takes place in this
phase. In particular, if a disjunction \(\mu\) has a disjunct \(\nu\) 
with a higher cost than \(\mu\), the disjunct \(\nu\) is removed from 
\(\mu\).\footnote{This is achieved by deleting the link between \(\mu\) and 
\(\nu\) in the NNF-graph.}
The intuition here is that \(\nu\) will be contributing partial diagnoses 
that are not minimal when compared to the partial diagnoses contributed by 
its siblings. Moreover, all completions of these partial diagnoses 
will be more costly than some completion of a partial diagnosis contributed 
by a sibling.

\subsection*{Phase II: Computing Instantiations}
The result of Phase I is a negation normal form that characterizes
minimal diagnoses only. To extract the minimal diagnoses, all we need 
then is to compute the instantiations of this pruned negation normal form, 
that is, compute its sum-of-product representation. This can be done 
recursively as follows:
\begin{enumerate}
\item The instantiations of a literal \(\mu\) are \(\{\mu\}\).
\item The instantiations of a conjunction are the Cartesian product
of the instantiations of its conjuncts.\footnote{This step will not be
sound unless the NNF is decomposable, that is, no atoms are 
shared between conjuncts.}
\item The instantiations of a disjunction are the union of the 
{\em extended} instantiations of its disjuncts. To understand this
extension process, consider a disjunction \(\mu\) and one of its
disjuncts \(\nu\). Just before the instantiations of \(\nu\)
are unioned with the instantiations of its siblings, they are extended
by adding zero-cost literals to them. The goal of this extension process is 
to make sure that each extended instantiation of \(\nu\) mentions all
atoms that appear in \(\mu\). This step would not be
necessary if we were computing the DNF of \(\mu\). Note, however, that
are computing the sum-of-product representation of \(\mu\) instead,
which means that each product in the sum must mention all atoms that 
appear in \(\mu\).
\end{enumerate}

The soundness of the algorithm is given below:
\begin{theorem} \label{theo:pi-sound}
After the termination of \(\mininsts\) in Figure~\ref{fig:extraction}, 
\(\terms(\mu) = \mpi(\mu)\) for every node \(\mu\) in the NNF-graph \(\tau\).
\end{theorem}

A detailed example of the algorithm is given in Figure~\ref{fig:example-mpi}
where cost propagation, pruning, and the computation of instantiations
are all explicated. 

\begin{figure}
{\small
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\begin{center}
\underline{{\bf An Example of Computing Minimal Instantiations}}
\end{center}
Consider the consequence in Figure~\ref{fig:example-sc} and the minimal cardinality
cost function. Calling \prune\ on the consequence leads to the following pruned NNF:
\begin{center}
\mbox{\epsfxsize=75mm \leavevmode \epsffile{/home/darwiche/latex/journals/JAIR/mbd/ssd-3-ae-pruned.eps}}
\end{center}
The cost of each node is shown next to it. The dotted links represent pruned 
parent-child links. Calling \insts\ on this result leads to the following:
\begin{center}
\mbox{\epsfxsize=85mm \leavevmode \epsffile{/home/darwiche/latex/journals/JAIR/mbd/ssd-3-ae-inst.eps}}
\end{center}
\(\atoms(\mu,\nu)\) is shown on the arc between \(\mu\) and \(\nu\).
\(\terms(\mu)\) is shown next to node \(\mu\). The final result is two
minimal instantiations \(\neg \ok(X) \wedge \ok(Y) \wedge \ok(Z)\) and 
\(\ok(X) \wedge \ok(Y) \wedge \neg \ok(Z)\).
\end{minipage}
}
\end{center}
}
\caption{An example illustrating the computation of minimal instantiations.
\label{fig:example-mpi}}
\end{figure}

The computational complexity of the presented algorithm is given next:
\begin{theorem}
\label{theo:pi-complexity}
Consider the algorithm \mininsts\ in Figure~\ref{fig:extraction}.
The time complexity of this algorithm is \(O(c E)\) where \(E\) is 
the number of edges in the NNF-graph \(\tau\) and 
\(c\) is square the number of instantiations returned by the algorithm
(that is, \(c = {\mid \mpi(\tau) \mid}^2\)).
\end{theorem}
We have two points to stress about the above result.

First, if the number of minimal diagnoses is small enough, the factor \(c\) 
is a constant, and the time and space complexity of \mininsts\ becomes 
\(O(E)\) which is linear in the size of \(\tau\). However, if
the number of minimal diagnoses cannot be regarded as a constant, 
then one cannot claim linear complexity. Needless to say, however, that 
one can never do better than the size of the answer that one is trying to 
compute. For example, if the number of minimal diagnoses is exponential in the 
size of \(\tau\), then no extraction algorithm can do better than exponential 
since the answer it has to return is exponential.

Second, the size of the consequence generated by \(\syscons\)
of Figure~\ref{fig:sc} is decided by the jointree \(\tree\) and the 
set of observed atoms \(\E\) --- it is independent of the specific 
instantiation \(\phi\) of \(\E\).\footnote{Component consequences will
depend on \(\phi\), but not the number of and/or nodes which are
added by \(\syscons\).} However, the number of minimal diagnoses extracted 
by \(\mininsts\) in Figure~\ref{fig:extraction} is very much dependent on the specific
observation \(\phi\). Therefore, if two observations \(\phi_1\) and \(\phi_2\) 
refer to the same set of atoms \(\E\), the cost of generating their 
consequences will be the same. However, 
the cost of extracting their minimal diagnoses may be different.

For a concrete example of this last point, consider an \(n\)-bit adder and 
the following observations:
\begin{enumerate}
\item [-] \(\phi_1\): 
All input/output bits are low except for the first sum bit.

\item [-] \(\phi_2\): 
All input/output bits are low except for all sum bits.
\end{enumerate}
The corresponding consequences of these observations will be both linear in 
\(n\). However, the first observation leads to two minimal diagnoses --- 
the first full adder has a broken xor-gate ---
while the second observation leads to \(2^n\) minimal diagnoses --- 
each of the full adders has a broken xor-gate. 
Therefore, computing the minimal diagnoses of \(\phi_1\) is linear in \(n\), 
but computing the minimal diagnoses of \(\phi_2\) is exponential in \(n\).

The last few observations reveal a merit of splitting the computation of
minimal diagnoses into two steps: characterization of all diagnoses and then
extraction of minimal ones. This is contrary to common practice in 
structure-based reasoning, but it allows one to make more refined 
statements on the complexity of model-based diagnosis.


\section{Conclusion and Related Work}
\label{sec:conclusion}

We have presented a comprehensive approach for characterizing and 
computing minimal diagnoses given a structured system description.
What is most important about our approach is that it ties the
computational complexity of diagnostic reasoning to a very 
meaningful aspect of systems: the topology of their system structures. 
Thus, it provides diagnostic practitioners with more flexibility in 
engineering the response time of their applications. This emphasis on 
structure has been the central theme in probabilistic reasoning lately
and there are a number of other algorithms for importing this theme into 
model-based diagnosis \cite{dechterAIJ94,geffner87}.
There are some key differences, however, between our proposal and the 
previous ones:
\begin{enumerate}
\item [-] Given consequences and the theorems to manipulate them, our proposal
can be viewed as a framework for structure-based diagnosis instead of
simply an algorithm. We did propose a specific algorithm which utilizes 
jointrees, but our framework can accommodate other structure-based algorithms 
(that do not necessarily utilize jointrees) as long as they provide a 
mechanism for applying the Intersection 
Corrollary efficiently (see \cite{darwicheDX98} for an example).

\item [-] We have decomposed the computation of minimal diagnoses into two 
independent stages: characterization of diagnoses using consequences 
and then choosing
a minimal subset of them. This separation has at least three advantages.
First, it allowed us to offer guarantees on the size of a consequence which 
are independent of the number of (minimal) diagnoses that it characterizes. 
Next, it allowed us to incorporate different minimality criteria without 
having to alter the characterization algorithm. Finally, it inspired a 
device compilation technique which is discussed in \cite{darwicheKR98}.

\item [-] The time and space complexity of our algorithm depends not only on 
the system topology but also on the system observables. In particular, we 
have shown that the more observables we have, the easier it is to diagnose 
a system using our algorithm. We have also provided a refined complexity
result which explicates precisely the effect of system observables on the 
complexity of structure-based diagnosis.

\item [-] Finally, 
previous algorithms have rested on the language of constraints 
among multivalued variables. Our approach uses a purely logical setting, 
which allows computation directly on Boolean syntax. This bridges the gap 
even further between structure--based reasoning and model--based diagnosis.
\end{enumerate}

\acks{The author would like to thank Yousri El Fattah and Gregory Provan
for providing useful comments on an earlier version of this paper.}

\newpage
\appendix


\newpage
\section{Representing Negation Normal Forms}
\label{app:nnfs}

This appendix describes our representation of negation normal forms
using directed acyclic graphs. It also provides a number of operations on
the suggested representation and some associated conventions. The material
in this appendix is necessary to understand the pseudocode provided 
throughout the paper.

\para{Representation:}

An {\em NNF-graph} over atoms \(\V\) is a rooted, directed acyclic graph
with three types of nodes: literal-nodes, and-nodes and or-nodes. 
For each literal node \(\mu\), \(\lit(\mu) = (V,v)\) where \(V \in \V\) 
and \(v \in \{0,1\}\). 
Each node \(\mu\) in an NNF-graph represents a Boolean sentence as follows:
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item [-] If \(\mu\) is a literal-node and \(\lit(\mu) = (V,v)\), then 
\(\mu\) represents 
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item [-] the positive literal \(V\) when \(v=1\)
\item [-] the negative literal \(\neg V\) when \(v=0\).
\end{list}

\item [-] If \(\mu\) is an and-node and the \(i^{\it th}\) child of \(\mu\)
represents sentence \(\alpha_i\), then \(\mu\) represents the
conjunction \(\wedge_i \alpha_i\).

\item [-] If \(\mu\) is an or-node and the \(i^{\it th}\) child of \(\mu\)
represents sentence \(\alpha_i\), then \(\mu\) represents the
disjunction \(\vee_i \alpha_i\).
\end{list}
The sentence represented by an NNF-graph is the sentence represented by 
its root node.

\para{Operations:} 

We have the following operations to manipulate NNF-graphs:
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item [-] \(\lnode(\mu)\), \(\anode(\mu)\), \(\onode(\mu)\): type predicates for nodes.
\item [-] \(\glnode(V,v)\): creates and returns a new literal-node 
labeled with \((V,v)\).
\item [-] \(\ganode\): creates and returns a new and-node (with no children).
\item [-] \(\gonode\): creates and returns a new or-node (with no children).
\item [-] \(\addchild(\nu,\mu)\): adds node \(\mu\) to the children of 
node \(\nu\).
\item [-] \(\children(\nu)\): returns the children of node \(\nu\). 
\end{list}

\para{Conventions:} 

We adopt the following conventions with respect to
NNF-graphs:
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item[-] If \(\tau\) is an NNF-graph, then \(\tau\) will also be used to
denote the root of \(\tau\).
\item[-] We use \(\true\) to denote an and-node with no children and
\(\false\) to denote an or-node with no children. 
\item[-] We do not show the directions of arcs assuming that they
point downwards.
\item[-] The NNF-graph rooted at some node is formed from that node and 
all its descendants.
\item[-] A node and the sentence it represents will be used exchangeably.
\end{list}

\newpage
\para{Example:} 

Consider the following NNF-graph:
\begin{center}
\mbox{\epsfxsize=90mm \leavevmode 
\epsffile{/home/darwiche/latex/journals/JAIR/mbd/nnf-cons.eps}}
\end{center}

This graph represents the following sentence 
\((\neg \ok(X) \wedge (\neg \ok(Z) \vee \false) ) \vee 
((\neg \ok(Z) \vee \false) \wedge \true)\). 
It can be created using the following sequence of calls:

\begin{center}
\begin{tabular}{l}
\(n_1 \set \glnode(\ok(Z),0)\) \\
\(n_2 \set \gonode\) \\ 
\(n_3 \set \gonode\)  \\
\(\addchild(n_3,n_1)\) \\
\(\addchild(n_3,n_2)\) \\
\(n_4 \set \glnode(\ok(X),0)\) \\
\(n_5 \set \ganode\) \\
\(\addchild(n_5,n_3)\)
\end{tabular}
\begin{tabular}{l}
\(\addchild(n_5,n_4)\) \\
\(n_6 \set \ganode\) \\ 
\(n_7 \set \ganode\) \\
\(\addchild(n_7,n_3)\) \\
\(\addchild(n_7,n_6)\) \\
\(n_8 \set \gonode\) \\
\(\addchild(n_8,n_5)\) \\
\(\addchild(n_8,n_7)\).
\end{tabular}
\end{center}







\newpage
\section{Representing Literals and Instantiations}
\label{app:insts}

This appendix discusses our representation of literals and instantiations and
provides some operations on these representations. The material
in this appendix is necessary to understanding the pseudocode which
is provided throught the paper.

\para{Representation:} 

An instantiation is represented by a set of pairs \((V,v)\) 
where \(V\) is an atom and \(v \in \avalues(V) = \{0,1\}\).

\para{Operations:} 

An instantiation \(\L\) can be asserted or retracted using
\(\assert(\L)\) and \(\retract(\L)\). After asserting an instantiation
\(\L\), we have the following for every pair \((V,v)\) in \(\L\):
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item [-] \(\instantiated(V)\) is true;
\item [-] \(\ivalue(V)\) equals \(v\).
\end{list}
We assume that sets of atoms are \underline{ordered}, say alphabetically,
where \(\head(\V)\) returns the first element of the set and \(\rest(\V)\) 
returns the tail of the set. Two operations are defined on ordered sets
of atoms:
\begin{itemize}
\item [-] A function to compute a unique index for the instantiated 
values of set \(\V\):\footnote{The ordering of \(\V\) is essential for
this function to return the same index for each instantiation of \(\V\).}
\begin{tabbing} 
{\sc in}\={\sc dex}(\V) {\em \{atoms in \(\V\) must be instantiated\}} \\
   \>01.  i\=f \(\V = \{\}\) \\
   \>02.  \>then return 0 \\
   \>03.  \>else return \(\ivalue(\head(\V)) + 2*\vindex(\rest(\V))\)
\end{tabbing}
\item [-] A function to compute all instantiations of the uninstantiated 
atoms in \(\V\):
\begin{tabbing}
{\sc ge}\={\sc nerate\_instantiations}(\(\V\)) 
{\em \{some atoms in \(\V\) may be instantiated\}} \\
   \>01. i\=f \(\V = \{\}\) \\
   \>02. \>then return \(\{\{\}\}\) \\
   \>03. \>else \=\(V \set \head(\V)\) \\
   \>04. \>     \>\(\R \set \ginstantiations(\rest(\V))\) \\
   \>05. \>     \>i\=f \(\instantiated(V)\) then return \(\R\) \\
   \>06. \>     \>\>else return 
           \(\displaystyle \bigcup_{v \in \avalues(V)} 
                             \{\{(V,v)\} \cup \alpha:\:\: \alpha \in \R\}\)
\end{tabbing}
\end{itemize}

\para{Examples:} 

Consider the instantiation \(\alpha = A \wedge \neg B \wedge D\).
This is represented as \(\L = \{(A,1), (B,0), (D,1)\}\). Suppose now that we
call \(\assert(\L)\). Then \(\instantiated(A)\) is true and \(\ivalue(B) = 0\).
Moreover, \(\vindex(\{A,B,D\}) = 5\) and we have 
\(\ginstantiations(\{C,D,E\}) =\)
\(\{\{(C,1), (E,1)\},\)\(\{(C,0), (E,1)\},\)\(\{(C,1), (E,0)\},\)
\(\{(C,0), (E,0)\}\}\).




\newpage
\section{Avoiding the Sharing of Assumables in Component Descriptions}
\label{app:sharing}

Consider the following figure which contains a structured system 
description where component descriptions \(\Delta_C\) and \(\Delta_D\)
share the assumable \(\power\):
\begin{figure}[h]
\begin{center}
\mbox{\epsfxsize=75mm \leavevmode \epsffile{ssd-2a.eps}}
\end{center}
{\tiny
\begin{center}
\begin{tabular}{c|c|c}
\(\Delta_A, \Delta_B\) & \(\Delta_C \) & \(\Delta_D\) \\ \hline
& & \\
\(\{\}\) &
\(\left\{\begin{array}{rcl}
A \wedge (\power \wedge \ok(X)) & \imply & \neg C \\
\neg A \wedge (\power \wedge \ok(X)) & \imply & C \\
\neg \power & \imply & \neg C
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
A \wedge B \wedge (\power \wedge \ok(Y)) & \imply & D \\
\neg(A \wedge B) \wedge (\power \wedge \ok(Y)) & \imply & \neg D \\
\neg \power & \imply & \neg D
\end{array}\right\}\)
\end{tabular}
\end{center}
}
\end{figure}

We can avoid the sharing of assumable \(\power\) by introducing an auxiliary
node \(\apower\) and making it equivalent to the shared assumable
\(\power\) as shown in the figure below. As a result of adding this 
auxiliary node \(\apower\), we no longer have a common assumable 
between the component descriptions \(\Delta_C\) and \(\Delta_D\) (but we 
have a common non-assumable \(\apower\) instead).

\begin{figure}[h]
\begin{center}
\mbox{\epsfxsize=75mm \leavevmode \epsffile{ssd-2b.eps}}
\end{center}

{\tiny
\begin{center}
\begin{tabular}{c|c|c|c}
\(\Delta_A, \Delta_B\) & \(\Delta_C \) & \(\Delta_D\) & \(\Delta_{\apower}\) \\ \hline
& & & \\
\(\{\}\) & 
\(\left\{\begin{array}{rcl}
A \wedge (\power' \wedge \ok(X)) & \imply & \neg C \\
\neg A \wedge (\power' \wedge \ok(X)) & \imply & C \\
\neg \power' & \imply & \neg C
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
A \wedge B \wedge (\power' \wedge \ok(Y)) & \imply & D \\
\neg(A \wedge B) \wedge (\power' \wedge \ok(Y)) & \imply & \neg D \\
\neg \power' & \imply & \neg D
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
\power & \imply & \apower \\
\neg \power & \imply & \neg \apower
\end{array}\right\}\) 

\end{tabular}
\end{center}
}
\end{figure}

This simple technique can be always used to ensure that no sharing of 
assumables takes place between component descriptions. Note, however, that
this ensurance comes at a price: The structured system description with 
auxiliary nodes (no assumable sharing) will typically be topologically 
more complex than the one where sharing is allowed. This is clearly the
case in the above example where the no-sharing-of-assumables 
led us to transform the system structure from a tree to a graph.

\newpage
\def\low{{\it low}}
\def\nom{{\it mid}}
\def\high{{\it high}}

\section{Extending the Framework to Multivalued Variables} 
\label{app:variables}

We show in this appendix how to represent constraints among assumables
using two methods:
\begin{enumerate}
\item introducing auxiliary atoms into the system structure;
\item using multivalued variables instead of atoms.
\end{enumerate}
The two approaches will be illustrated using the following example.

Consider a component which has one input and one output: the input
is either \(\low,\nom\) or \(\high\) and the
output is either \(\on\) or \(\off\). Furthermore, suppose that this component 
has two fault modes \(M_1\) and \(M_2\). Such a component can be 
represented as shown in Figure~\ref{fig:modes}.
In this figure, we have two auxiliary atoms, \(C_1\) and \(C_2\),
which represent constraints. The first constraint, \(C_1\), ensures that 
\(\low, \nom\) and \(\high\) are mutually exclusive and exhaustive.
The second constraint, \(C_2\), ensures that \(M_1\) and \(M_2\) are
mutually exclusive. The atoms \(C_1\) and \(C_2\) should always be observed
to enforce these constraints. That is, for any system 
observation \(\phi\), we must actually invoke \syscons\ on 
\(\phi \wedge C_1 \wedge C_2\) to make sure that the two constraints are 
enforced.

\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\begin{center}
\mbox{\epsfxsize=75mm \leavevmode \epsffile{modes.eps}}
\end{center}
{\tiny
\begin{center}
\begin{tabular}{|c|c|c|}
\(\Delta_{M_1'}\) & \(\Delta_{M_2'}\) & 
\(\Delta_{C_1}\)\\ \hline
 & & \\
\(\left\{\begin{array}{rcl}
M_1 & \imply & M_1' \\
\neg M_1 & \imply & \neg M_1'
\end{array}\right\}\) 
&
\(\left\{\begin{array}{rcl}
M_2 & \imply & M_2' \\
\neg M_2 & \imply & \neg M_2'
\end{array}\right\}\) 
&
\(\left\{\begin{array}{rcl}
\low \wedge \nom & \imply & \neg C_1 \\
\low \wedge \high & \imply & \neg C_1 \\
\nom \wedge \high & \imply & \neg C_1 \\
\neg \low \wedge \neg \nom \wedge \neg \high & \imply & \neg C_1
\end{array}\right\}\)
\end{tabular}
\end{center}

\begin{center}
\begin{tabular}{|c|c|}
\(\Delta_{C_2}\)  & \(\Delta_{O}\) \\ \hline 
& \\
\(\left\{\begin{array}{rcl}
M_1' \wedge M_2' & \imply & \neg C_2
\end{array}\right\}\) 
&
\(\left\{\begin{array}{rcl}
(\low \vee \nom) \wedge \neg M_1' \wedge \neg M_2' & \imply & \neg O \\
\high \wedge \neg M_1' \wedge \neg M_2' & \imply & O \\
M_1' & \imply & \neg O \\
M_2' & \imply & O
\end{array}\right\}\) 
\end{tabular}
\end{center}
}
\end{minipage}
}
\end{center}
\caption{Modeling a component with multiple fault modes and 
multiple input values.
\label{fig:modes}}
\end{figure}

This approach is relatively reasonable but the representation is not
as concise as one would expect.
A better solution for representing such systems involves the use of
{\em multivalued variables} instead of atoms. This solution will be
described next and it leads to a more concise, efficient representation.

An atom is a special case of a variable in that it only has two values.
A general variable, however, can have any finite number of values. 
In the previous example, it would be best to represent the input as a 
variable with three values \(\low, \nom\) and \(\high\); to represent 
the output as a variable with two values \(\on\) and \(\off\); and to 
represent the mode as a variable with three values \({\it ok}, M_1\)
and \(M_2\).

Using variables instead of atoms, the system in Figure~\ref{fig:modes} can 
be encoded as given in Figure~\ref{fig:modes-vars}. This is clearly a more
compact and efficient representation.

More generally though, we extend our framework to variables by taking the
set of non-assumables \(\P\) and the set of assumables \(\A\) to be 
sets of variables, instead of atoms. We next discuss formally the syntax
and semantics of the resulting variable-based logic, and then show what
modifications are needed to our presented definitions and 
pseudocode (only two changes are needed).

\para{Syntax and Semantics}
In this variable-based framework, a literal is 
a pair \((V,v)\), where \(V\) is a variable and \(v\) is a value. A 
sentence is either a literal, the negation of a sentence, or the 
combination of two sentences using a standard 
logical connective such as \(\wedge\), \(\vee\) or \(\imply\). This 
defines the syntax of a propositional logic with multivalued variables.
This logic includes standard propositional logic as a special case 
(that is, when all variables are binary). The 
semantics of this logic is defined in the usual way. That is, a model 
\(\w\) is a function that assigns one value to each variable. 
Moreover, a model \(\w\) satisfies a sentence under the following
conditions:
\begin{list}{}{\setlength{\itemsep}{0mm}\setlength{\parsep}{0mm}}
\item \(\w \models (V,v)\) if \(\w\) assigns the value \(v\) to variable \(V\);
\item \(\w \models \neg \alpha\) if \(\w \not \models \alpha\);
\item \(\w \models \alpha \vee \beta\) if 
\(\w \models \alpha\) or \(\w \models \beta\); and
\item \(\w \models \alpha \wedge \beta\) if 
\(\w \models \alpha\) and \(\w \models \beta\).
\end{list}
A sentence is satisfiable (consistent) iff it has at least one model. 
This also leads to the usual notions of entailment and validity.

\begin{figure}[tb]
{\small
\begin{center}
\fbox{
\begin{minipage}{4.5in}
\begin{center}
\mbox{\epsfxsize=35mm \leavevmode \epsffile{modes-vars.eps}}
\end{center}
{\tiny
\begin{center}
\begin{tabular}{c|c}
\(\Delta_I\) & \(\Delta_O \) \\ \hline
& \\
\(\{\}\) &
\(\left\{\begin{array}{rcl}
((I,\low) \vee (I,\nom)) \wedge (\mode,{\it ok}) & \imply & (O,\off) \\
(I,\high) \wedge (\mode,{\it ok}) & \imply & (O,\on) \\
(\mode,M_1) & \imply & (O,\off) \\
(\mode,M_2) & \imply & (O,\on)
\end{array}\right\}\) 
\end{tabular}
\end{center}
}
\end{minipage}
}
\end{center}
}
\caption{An SSD using multivalued variables.
\label{fig:modes-vars}}
\end{figure}

It is important to stress that in this variable-based logic, the term 
\(\neg (V,v)\) is not considered a literal in general. 
Note that if \(V\) is not a 
binary variable, then \(\neg (V,v)\) would be equivalent
to a clause \((V,v_1) \vee (V,v_2) \vee \ldots \vee (V,v_n)\) where
\(v_1, \ldots, v_n\) are the values of variable \(V\) not equal to \(v\).
Having said that, an instantiation of a set of variables \(\V\) is 
defined as a conjunction of literals, one literal for each variable 
in \(\V\). This means that 
\(\neg (I,\low) \vee (O,\on) \vee (M,{\it ok})\) is not an 
instantiation according to the previous definition.

\para{Modifications}
In the extended framework, all definitions and theorems remain
intact with two exceptions:
\begin{enumerate}
\item Since variables can have more than two values, we need to generalize 
the function \(\vindex\) in Appendix~\ref{app:insts} which computes unique
indices for instantiations:
\begin{center}
{\small
\begin{tabbing}
{\sc in}\={\sc dex}(\V) \\
   \>01.  \((i,b) \set \aindex(\V)\) \\
   \>02.  return \(i\)
\end{tabbing}
\begin{tabbing}
{\sc au}\={\sc x-index}(\V) \\
   \>01.  i\=f \(\V = \{\}\) \\
   \>02.  \>then return \((0,1)\) \\
   \>03.  \>else \= \((i,b) \set \aindex(\rest(\V))\) \\
   \>04.  \>     \> \(V \set \head(\V)\) \\
   \>05.  \>     \>return \((i + \ivalue(V) * b, \mid \avalues(V) \mid * b)\)
\end{tabbing}
}
\end{center}
Here, we are assuming that the values of each variable are 
\(\{0, 1, \ldots\}\). Suppose, for example, that we have 
\(\V = \{V_1, V_2, V_3\}\) where \(V_1\) and \(V_3\) have the values
\(\{0,1\}\) and \(V_2\) has the values \(\{0, 1, 2\}\). We then have
the following instantiations and their corresponding indices:
\begin{center}
{\tiny
\begin{tabular}{ccc||c}
\(V_1\) & \(V_2\) & \(V_3\) & index \\ \hline
0 & 0 & 0 & 0 \\
0 & 0 & 1 & 1 \\
0 & 1 & 0 & 2 \\
0 & 1 & 1 & 3 \\
0 & 2 & 0 & 4 \\
0 & 2 & 1 & 5 \\
1 & 0 & 0 & 6 \\
1 & 0 & 1 & 7 \\
1 & 1 & 0 & 8 \\
1 & 1 & 1 & 9 \\
1 & 2 & 0 & 10 \\
1 & 2 & 1 & 11
\end{tabular}
}
\end{center}

\item Since assumables can have more than two values, 
Definition~\ref{def:costf} of a cost function should be changed so that 
the condition:
\begin{itemize}
\item[-] \(\cf\) maps each \(\A\)-literal into a cost in \(\costs\), 
where each literal or its negation has cost~0;
\end{itemize}
reads as 
\begin{itemize}
\item[-] \(\cf\) maps each \(\A\)-literal into a cost in \(\costs\), 
where for each variable \(V \in \A\), 
at least one literal \((V,v)\) must have cost 0.
\end{itemize}
\end{enumerate}


\newpage
\section{Cutting Outgoing-Arcs of Observed Nodes} \label{app:arcs}


\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{5.8in}
\vspace{.5cm}
\begin{center}
\mbox{\epsfxsize=85mm \leavevmode \epsffile{ssd-3-abs.eps}}
\end{center}

{\tiny
\begin{center}
\begin{tabular}{c|c|c|c}
\(\Delta_A, \Delta_B\) & \(\Delta_C \) & \(\Delta_D\) & \(\Delta_E\) \\ \hline
& & & \\
\(\{\}\) & 
\(\left\{\begin{array}{rcl}
A \wedge \ok(X) & \imply & \neg C\\
\neg A \wedge \ok(X) & \imply & C
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
B \wedge \ok(Y) & \imply & D \\
\neg B \wedge \ok(Y) & \imply & \neg D
\end{array}\right\}\) &
\(\left\{\begin{array}{rcl}
(C \wedge D) \wedge \ok(Z) & \imply & E \\
\neg (C \wedge D) \wedge \ok(Z) & \imply & \neg E
\end{array}\right\}\) 
\end{tabular}
\end{center}
}
\end{minipage}
}
\end{center}
\caption{A structured system description of a digital circuit. The 
arc from node \(A\) to node \(D\) has been cut out given that node \(A\)
is observed.
\label{fig:ssd-3-abs}}
\end{figure}

Consider the structured system description given in Figure~\ref{fig:ssd-3}
and suppose that we want to compute the diagnoses for system observation
\(\phi = \neg A \wedge \neg E\). This computation can be performed with
respect to the SSD in Figure~\ref{fig:ssd-3} or, equivalently, it can be 
performed with respect to the SSD in Figure~\ref{fig:ssd-3-abs}. This
SSD is obtained from the one in Figure~\ref{fig:ssd-3} as follows:
\begin{enumerate}
\item The arc going from node \(A\) to node \(D\) is cut out.
\item Every occurrence of atom \(A\) in the component description \(\Delta_D\) 
is replaced with \(\false\) since \(A\) appears negated in 
\(\phi\).\footnote{\(A\) would be replaced by \(\true\) if it did not
appear negated.}
\end{enumerate}
It is easy to show that the consequence of \(\phi\) is the same with
respect to both SSDs. Working with the modified SSD is preferred, however,
since it has a tree system structure. 

We have the following observations about this process of cutting out arcs 
from the system structure:
\begin{itemize}
\item One can cut out all outgoing-arcs of any node that appears in
the system observation. In our previous example, we can also cut out
the arc from \(A\) to \(C\) but we must also modify \(\Delta_C\) 
accordingly.\footnote{This will lead to a disconnected system structure.
In such a case, we have to compute the consequence of each disconnected piece 
and then conjoin all consequences.}

\item Even if cutting out arcs does not lead to a tree structure, it
would typically lead to reducing the size of cliques of the resulting 
system structure. In fact, the reduction could move some problems from 
being practically unsolvable using structure-based methods to being
solvable. Consider the results reported in \cite{fattahUAI96} for 
an example which show jointree statistics for the benchmark circuits 
proposed in \cite{CIRCUITS}. The following table shows the
maximal-clique sizes reported for a few of the circuits together
with the maximal-clique sizes after the arcs outgoing from observed
nodes (root nodes) are cut out:\footnote{The jointrees after cutting 
out arcs are computed using the algorithm reported in \cite{darwicheIJAR96}.}
\begin{center}
\begin{tabular}{c||c|c|c}
{\em Circuit} & {\em \#nodes} & {\em maximal-clique size} & {\em maximal-clique size} \\
              &                &{\em before cutting arcs} & {\em after cutting arcs} \\ \hline
c432 & 196 & 28 & 22 \\
c499 & 243 & 25 & 10 \\
c880 & 443 & 28 & 10 \\
c1355 & 587 & 25 & 10 
\end{tabular}
\end{center}
There is clearly a dramatic change in the maximal-clique size for the last
three circuits. In fact, there are only a few cliques which have the 
maximal size or a size close to it as is shown in \cite{fattahUAI96}.
This makes the approach reported in this paper appropriate for the 
last three circuits. The approach, however, is not appropriate as is 
for the first circuit.

We close this section by stressing again that this process of cutting out
arcs can lead to a very dramatic reduction in maximal-clique size. 
Therefore, it should be exploited whenever possible \cite{darwicheAAAI97}.

\end{itemize}


\newpage
\section{Proofs} \label{app:proofs}

\subsection*{Proof of Theorem~\ref{theo:characterization}}

Suppose that 
\(\cons^\Delta_{\cA}(\phi) \equiv \alpha_1 \vee \ldots \vee \alpha_n\)
where each \(\alpha_i\) is an \(\A\)-instantiation.
Then \(\Delta \cup \{\phi\} \models \alpha_1 \vee \ldots \vee \alpha_n\)
by definition of a consequence. 
We need to prove two things:
\begin{enumerate}
\item Each \(\alpha_i\) is a diagnosis. \\
It suffices to show that \(\Delta \cup \{\phi, \alpha_i\}\) is consistent. 
Suppose that \(\Delta \cup \{\phi, \alpha_i\}\) is not consistent. Then
\(\Delta \cup \{\phi\} \models \neg \alpha_i\) and 
\[ \Delta \cup \{\phi\} \models
    \alpha_1 \vee \ldots \vee \alpha_{i-1} \vee \alpha_{i+1} \vee 
    \ldots \vee \alpha_n. \]
Taking \(\beta = \alpha_1 \vee \ldots \vee \alpha_n\), we contradict
Condition~3 in the definition of a consequence.

\item If \(\beta\) is a diagnosis, then \(\beta\) must be equal to some \(\alpha_i\). \\
Suppose that \(\beta\) is a diagnosis. Then \(\Delta \cup \{\phi, \beta\}\) 
must be consistent.  
Moreover, \(\Delta \cup \{\phi, \beta\} \models \alpha_1 \vee \ldots \vee \alpha_n\) 
since \(\Delta \cup \{\phi\} \models \alpha_1 \vee \ldots \vee \alpha_n\). 
This means that \(\beta\) must be equal to some \(\alpha_i\); otherwise, 
\(\Delta \cup \{\phi, \beta\}\) would be inconsistent which we know it 
is not.~\eproof
\end{enumerate}



\subsection*{Proof of Theorem~\ref{theo:connections}}

Follows directly from the definition of a consequence and the
characterization theorem.~\eproof



\subsection*{Proof of Theorem~\ref{theo:cc}}

First, observe that each clause \(\alpha\) in \(\Delta_O\) can be
written as the disjunction of two clauses \(\alpha_\P \vee \alpha_\A\)
where \(\alpha_\P\) is the projection of \(\alpha\) on non-assumables
\(\P\) and \(\alpha_\A\) is the projection of \(\alpha\) on assumables
\(\A\). Moreover, \(\phi\) mentions every atom that appears in
\(\alpha_\P\). Therefore, either 
\begin{enumerate}
\item \(\phi \models \alpha_\P\): Hence, \(\phi \models \alpha_{\P} \vee \alpha_\A\) 
and \(\phi \wedge (\alpha_{\P} \vee \alpha_{\A})\) is equivalent to
 \(\phi\); or

\item \(\phi \models \neg \alpha_\P\): Hence, 
\(\phi \wedge (\alpha_{\P} \vee \alpha_{\A})\) is equivalent to 
\(\phi \wedge \alpha_{\A}\).
\end{enumerate}
Therefore, \(\Delta_O \cup \{\phi\}\) is equivalent to \(\phi\) 
conjoined with every \(\alpha_\A\) whose matching \(\alpha_\P\)
is inconsistent with \(\phi\). Therefore, \(\cons^{\Delta_O}_{\A}(\phi)\)
is the conjunction of all \(\alpha_\A\)'s whose matching \(\alpha_\P\)
is inconsistent with \(\phi\).~\eproof


\subsection*{Proof of Theorem~\ref{theo:decomposition}}

We prove this theorem in two steps:
\begin{enumerate}
\item \(\cons^{\Theta \cup \Gamma}(\phi)  \equiv 
\cons^{\Theta}(\phi) \wedge \cons^{\Gamma}(\phi)\). \\
Recall that \(\cons^{\Theta \cup \Gamma}(\phi)\) is the strongest 
\(\cA\)-sentence entailed by \(\Theta \cup \Gamma \cup \{\phi\}\). 
By Lemma~\ref{lem:instantiation}:
\begin{itemize}
\item [-] There is a database \(\Theta'\) that does not share atoms with
\(\phi\), and \(\Theta' \cup \{\phi\} \equiv \Theta \cup \{\phi\}\). 

\item [-] There is a database \(\Gamma'\) that does not share atoms with
\(\phi\), and \(\Gamma' \cup \{\phi\} \equiv \Gamma \cup \{\phi\}\). 
\end{itemize}
Note that no clause in  \(\Theta' \cup \{\phi\}\) can resolve with any
clause in \(\Gamma' \cup \{\phi\}\) since there are no common atoms between 
\(\Theta'\) and \(\Gamma'\). Therefore, the \(\cA\)-clauses derived from
\(\Theta' \cup \Gamma' \cup \{\phi\}\) are those derived from 
\(\Theta' \cup \{\phi\}\) in addition to those derived from \(\Gamma' \cup \{\phi\}\).\footnote{An \(\A\)-clause is a clause which contains \(\A\)-literals
only.} It then follows that the strongest \(\cA\)-sentence 
entailed by \(\Theta' \cup \Gamma' \cup \{\phi\}\) --- which
is equivalent to the conjunction of all \(\cA\)-clauses entailed by 
\(\Theta' \cup \Gamma' \cup \{\Phi\}\) --- is equivalent to the 
strongest \(\cA\)-sentence entailed by \(\Theta' \cup \{\phi\}\) conjoined with the
strongest \(\A\)-sentence entailed by \(\Gamma' \cup \{\phi\}\):
\[ \cons^{\Theta' \cup \Gamma'}(\phi)  
\equiv 
\cons^{\Theta'}(\phi) \wedge \cons^{\Gamma'}(\phi),
\]
which leads to:
\[ \cons^{\Theta \cup \Gamma}(\phi)  
\equiv 
\cons^{\Theta}(\phi) \wedge \cons^{\Gamma}(\phi).
\]

\item \(\cons^{\Theta}(\phi) \equiv \cons^{\Theta}(\phi_\Theta)\) and 
\(\cons^{\Gamma}(\phi) \equiv \cons^{\Gamma}(\phi_\Gamma)\).  \\
The atoms that appear in \(\phi\) but do not appear in \(\phi_\Theta\) 
do not appear in \(\Theta\) either. Therefore, they do not affect the 
strongest \(\A\)-sentence entails by \(\Theta \cup \{\phi\}\). The same
is true for \(\Gamma\) and \(\phi_\Gamma\).
\end{enumerate}
Therefore,
\[ \cons^{\Theta \cup \Gamma}(\phi)  
\equiv 
\cons^{\Theta}(\phi_\Theta) \wedge \cons^{\Gamma}(\phi_\Gamma).~\eproof
\]


\begin{lemma} \label{lem:instantiation}
Suppose that \(\Delta\) is a database and \(\phi\) is a set of 
literals. There exists a database \(\Delta'\) such that 
\begin{enumerate}
\item \(\Delta'\) does not share atoms with \(\phi\); and 
\item \(\Delta' \cup \phi\) is equivalent to \(\Delta \cup \phi\).
\end{enumerate}
\end{lemma}

\subsection*{Proof of Lemma~\ref{lem:instantiation}}
We show how to construct \(\Delta'\) from \(\Delta\). 
Suppose that \(\Delta\) is in clausal form. Each clause \(\alpha\)
in \(\Delta\) must satisfy one of the following conditions:
\begin{enumerate}
\item \(\alpha\) does not share atoms with \(\phi\);
\item \(\alpha\) shares some atoms with \(\phi\) and we have either:
\begin{enumerate}
\item \(\alpha\) and \(\phi\) share a literal, which means that
\(\alpha\) is subsumed by \(\phi\); or

\item \(\alpha\) and \(\phi\) share no literals, which means that
\(\alpha\) resolves with some literals in \(\phi\) to yield 
a clause \(\beta\) that does not share atoms with \(\phi\). Moreover, 
\(\phi \cup \{\beta\}\) is equivalent to \(\phi \cup \{\alpha\}\).
\end{enumerate}
\end{enumerate}
We can obtain \(\Delta'\) from \(\Delta\) as follows. For each clause 
\(\alpha\) in \(\Delta\):
\begin{enumerate}
\item if \(\alpha\) is in Class~1 above, add \(\alpha\) to \(\Delta'\);
\item if \(\alpha\) is in Class~2a above, ignore \(\alpha\);
\item if \(\alpha\) is in Class~2b above, add the resolvant 
\(\beta\) to \(\Delta'\).
\end{enumerate}
It should be obvious that \(\Delta' \cup \phi\) is 
equivalent to \(\Delta \cup \phi\).~\eproof


\subsection*{Proof of Theorem~\ref{theo:case-analysis}}
It suffices to prove that 
\(\cons^\Delta(\gamma \vee \beta) \equiv 
\cons^\Delta(\gamma) \vee \cons^\Delta(\beta)\).
The theorem then follows from observing that 
\(\phi \equiv \bigvee_{\alpha} (\phi \wedge \alpha)\)
where \(\alpha\) ranges over instantiations of atoms \(\S\)
that are consistent with \(\phi\). This leads to
\(\cons^\Delta(\phi) \equiv \cons^\Delta(\bigvee_\alpha (\phi \wedge \alpha))
\equiv \bigvee_\alpha \cons^\Delta(\phi \wedge \alpha)\).
\begin{enumerate}
\item \(\cons^\Delta(\gamma) \vee \cons^\Delta(\beta) 
\models \cons^\Delta(\gamma \vee \beta)\). \\
By definition of a consequence, we have 
\(\cons^\Delta(\gamma) \models \cons^\Delta(\gamma \vee \beta)\) and
\(\cons^\Delta(\beta) \models \cons^\Delta(\gamma \vee \beta)\). 
Therefore, we must have
\(\cons^\Delta(\gamma) \vee \cons^\Delta(\beta) 
\models \cons^\Delta(\gamma \vee \beta)\).

\item \(\cons^\Delta(\gamma \vee \beta) 
\models \cons^\Delta(\gamma) \vee \cons^\Delta(\beta)\). \\
By definition of a consequence, we have 
\(\Delta \cup \{\gamma\} \models \cons^\Delta(\gamma)\) and
\(\Delta \cup \{\beta\} \models \cons^\Delta(\beta)\). Therefore,
\((\Delta \cup \{\gamma\}) \vee (\Delta \cup \{\beta\}) \models 
\cons^\Delta(\gamma) \vee \cons^\Delta(\beta)\). This is equivalent to 
\(\Delta \cup \{\gamma \vee \beta\} 
\models \cons^\Delta(\gamma) \vee \cons^\Delta(\beta)\), which means that
\(\cons^\Delta(\gamma) \vee \cons^\Delta(\beta)\) is an \(\A\)-sentence 
implied by \(\Delta \cup \{\gamma \vee \beta\}\).
By definition of \(\cons^\Delta(\gamma \vee \beta)\), we must then have 
\(\cons^\Delta(\gamma \vee \beta) 
\models \cons^\Delta(\gamma) \vee \cons^\Delta(\beta)\).~\eproof
\end{enumerate}


\subsection*{Proof of Theorem~\ref{theo:sd-ssd}}

Suppose that \(\ssd\) is a structured system description according to
Definition~\ref{def:ssd}. We want to prove that \(\Delta \cup \{\alpha\}\) 
is consistent for any instantiation \(\alpha\) of the assumables \(\cA\). 

The proof is by induction on the system structure.

\para{Base case:} Suppose that the system structure has a single node
\(O\). Then \(\Delta = \Delta_O\) and it follows from the definition
of \(\Delta_O\) that \(\Delta \cup \{\alpha\}\) is consistent for any 
instantiation \(\alpha\) of the assumables \(\cA\). 

\para{Inductive step:} Suppose that we have a 
structured system description \(\ssd\) satisfying the above property.
It suffices to show that the property will still hold after we add a leaf
node \(O\) to the system structure together with its component description
\((\I,O,\Delta_O)\). That is, we need to show that 
\(\Delta \cup \Delta_O \cup \{\alpha\}\) 
is consistent for any instantiation \(\alpha\) of the assumables \(\cA\)
given that \(\Delta \cup \{\alpha\}\) is consistent.

It suffices to show that \(\Delta \cup \Delta_O \cup \{\alpha, \beta\}\) 
is consistent for some instantiation \(\beta\) of \(\I \cup \{O\}\). Since 
\(\Delta \cup \{\alpha\}\) is consistent, there must exist some 
instantiation \(\beta_\I\) of \(\I\) such that 
\(\Delta \cup \{\alpha, \beta_\I\}\) is consistent. Moreover, since
\(\Delta_O \cup \{\alpha, \beta_\I\}\) is consistent (by definition of
a component description), there must exist some instantiation \(\beta_O\) of
\(O\) such that \(\Delta_O \cup \{\alpha, \beta_\I, \beta_O\}\) is
consistent. Consider now the following:
\begin{itemize}
\item [-] \(\Delta_O \cup \{\alpha, \beta_\I, \beta_O\}\) is equivalent
to \(\{\alpha, \beta_\I, \beta_O\}\) since every atom that appears in
\(\Delta_O\) appears in the instantiation \(\{\alpha, \beta_\I, \beta_O\}\)
and, hence, \(\{\alpha, \beta_\I, \beta_O\} \models \Delta_O\).

\item [-] \(\Delta \cup \{\alpha, \beta_\I, \beta_O\}\) is consistent
since \(\Delta \cup \{\alpha, \beta_\I\}\) is consistent and the atom \(O\)
does not appear in \(\Delta \cup \{\alpha, \beta_\I\}\).
\end{itemize}
Therefore, \(\Delta \cup \Delta_O \cup \{\alpha, \beta_\I, \beta_O\}
\equiv \Delta \cup \{\alpha, \beta_\I, \beta_O\}\) 
is consistent and, hence, \(\Delta \cup \Delta_O \cup \{\alpha\}\) is
consistent.~\eproof

\subsection*{Proof of Theorem~\ref{theo:cc-sound}}

First, the call \(\empty(\alpha_\P \cap \gamma)\) on line~06 returns true 
iff no literal in \(\alpha_\P\) appears in \(\gamma\). Since \(\alpha_\P\)
represents a clause of some atoms in \(\I \cup \{O\}\) and \(\gamma\) 
represents an instantiation of \(\I \cup \{O\}\), then every literal in
\(\alpha_\P\) is contradicted by some literal in \(\gamma\). Therefore,
this call will return true iff \(\gamma \models \neg \alpha_\P\).

Second, the call \(\cdisj(\alpha_\A)\) on line~07 returns a disjunction of 
the literals in \(\alpha_\A\). 

Therefore, for each instantiation \(\gamma\) of \(\I \cup \{O\}\), the 
function \(\compcons\) computes a conjunction of disjunctions where each 
disjunction represents an \(\alpha_\A\) whose matching \(\alpha_\P\) is 
inconsistent with \(\gamma\). The algorithm is then sound given 
Theorem~\ref{theo:cc}.~\eproof


\subsection*{Proof of Theorem~\ref{theo:cc-complexity}}

Line~01 will generate \(2^{\mid \I \mid + 1}\) instantiations, which is the
number of times that lines~02-08 will repeat. Each of lines~02,~03 and~08 take 
\(O(n)\) time. Line~04 takes \(O(1)\) time. The loop in lines~05-07 will
repeat \(s\) times. Line~06 takes \(O(n)\) time since \(\empty\) can be 
implemented in \(O(n)\) time. Line~07 also takes \(O(n)\) time since \(\cdisj\)
takes \(O(n)\) time.
Therefore, lines~05-07 take \(O(s n)\) time and, hence, lines~02-08 take 
\(O(s n)\). Finally, lines~01-09 take \(2^{\mid \I \mid + 1} O(s n)\) time 
which is \(O(s n 2^{\mid \I \mid} )\). The space complexity is no worse 
than the time complexity since adding a node or arc to the computed 
consequence takes \(O(1)\) time.~\eproof


\subsection*{Proof of Lemma~\ref{lem:sc-a}}

First, we need to prove that atoms \(\clique_i\) are instantiated to
some \(\alpha\) when the call \linebreak
\(\clscons(\clique_i)\) is made. This follows 
immediately since \(\clscons(\clique_i)\) is only called on line~06 of 
\(\strcons\) and \(\alpha\) is instantiated on line~04 of the same function.

The call \(\clscons(\clique_i)\) computes the following expression:
\[ \bigwedge_{O \in \comp(\clique_i)} \ccons_O[\vindex(O \cup \dag_O)]. \]
Therefore, all we need to show is that 
\[\cons^{\Delta_i}_{\A}(\alpha) 
 \equiv \bigwedge_{O \in \comp(\clique_i)} 
  \ccons_O[\vindex(O \cup \dag_O)]. \]
Given Theorem~\ref{theo:cc-sound}, it is enough to show that
\[\cons^{\Delta_i}_{\A}(\alpha) 
 \equiv \bigwedge_{O \in \comp(\clique_i)} 
           \cons^{\Delta_O}(\alpha_{\Delta_O}), \]
where \((O,\dag_O,\Delta_O)\) is the component description of \(O\)
and \(\alpha_{\Delta_O}\) is the projection of 
instantiation \(\alpha\) on the atoms \(\{O\} \cup \dag_O\) appearing
in \(\Delta_O\).

First note that \(\alpha\) is an instantiation of the atoms in clique
\(\clique_i\). Therefore, the common atoms between any two \(\Delta_O\)'s 
must appear in \(\alpha\) and, hence, the Decomposition Theorem gives:
\begin{eqnarray*}
\cons^{\Delta_i}_{\A}(\alpha) 
& \equiv & \cons^{\bigcup_{O \in \comp(\clique_i)}\Delta_O}_{\A}(\alpha) \\
& \equiv & \bigwedge_{O \in \comp(\clique_i)} 
\cons^{\Delta_O}_{\A}(\alpha_{\Delta_O}).~\eproof
\end{eqnarray*}


\subsection*{Proof of Lemma~\ref{lem:sc-b}}

We start with some concrete examples of the used notation.
In Figure~\ref{fig:jt1}, we have:
\[\Delta_{12} = \Delta_A \cup \Delta_B \cup \Delta_D = 
\left\{
\begin{array}{lcr}
(A \vee B) \wedge \ok(Y) & \imply & D, \\
\neg(A \vee B) \wedge \ok(Y) & \imply & \neg D
\end{array} 
\right\}; \]
while 
\[\Delta_{21} = \Delta_C \cup \Delta_E = 
\left\{
\begin{array}{lcr}
A \wedge \ok(X) & \imply & \neg C, \\ 
\neg A \wedge \ok(X) & \imply & C, \\ 
C \wedge D \wedge \ok(Z) & \imply & E, \\
\neg(C \wedge D) \wedge \ok(Z) & \imply & \neg E
\end{array}
\right\}.
\]
Moreover, given that \(\phi = A \wedge E\), then 
\(\phi_{12} = A\) and \(\phi_{21} = A \wedge E\).


\subsubsection*{Soundness of caching}

We will prove the lemma ignoring the caching on lines~00,~01 and~11.
The soundness of this caching process follows because according to the 
lemma, any two calls to \linebreak 
\(\strcons(\clique_i,\clique_j)\) will return
equivalent sentences if they are made under the same instantiation
\(\alpha\) of sepset \(\sepset_{ij}\). Line~00 computes a unique index \(l\)
for each instantiation of \(\sepset_{ij}\) which is used on line~01 to
check if a previous call with respect to this instantiation has been made.
If not, the computed sentence is cached on line~11 under the index \(l\).

\subsubsection*{Proof by induction}

First, we need to prove that atoms \(\sepset_{ij}\) are instantiated 
when the call \linebreak 
 \(\strcons(\clique_i,\clique_j)\) is made. 
\(\strcons\) is only called in two places:
\begin{enumerate}
\item \(\strcons(\clique_z,\clique_{0})\) is called on line~03 of 
\(\syscons\): the sepset \(\sepset_{z0} = \emptyset\) which is trivially 
instantiated.

\item \(\strcons(\clique_k,\clique_i)\) is called on line~08 of 
\(\strcons\): the sepset \(\sepset_{ki}\) is a subset of clique 
\(\clique_i\) and the atoms of this clique are instantiated on line~04. 
Therefore, the atoms of \(\sepset_{ki}\) are instantiated when this call to 
\(\strcons\) is made.
\end{enumerate}

The rest of the proof is by induction on the structure of the jointree. 

\para{Base case:} \(\clique_i\) has a single neighbor \(\clique_j\).

In this case, lines~08 of \(\strcons\) will not be executed. 
Therefore, the function \strcons\ is only computing the disjunction of all 
calls to \(\clscons(\clique_i)\) where each such call is made with respect to 
some instantiation \(\alpha\) of clique \(\clique_i\) which is consistent 
with \(\beta \wedge \phi_i\). 

Given Lemma~\ref{lem:sc-a}, all we need to show then is that:
\[ \cons^{\Delta_{ij}}(\beta \wedge \phi_{ij}) \equiv
\bigvee_{\alpha} \cons^{\Delta_i}(\alpha \wedge \phi_i). \]
By the Case--Analysis Theorem, we have:
\[ \cons^{\Delta_{ij}}(\beta \wedge \phi_{ij}) \equiv
\bigvee_{\alpha} 
\cons^{\Delta_{ij}}(\alpha \wedge \beta \wedge \phi_{ij}), \]
where \(\alpha\) ranges over all instantiations of clique \(\clique_i\)
which are consistent with \(\beta \wedge \phi_{ij}\). We also have
\begin{itemize}
\item[-] \(\Delta_{ij}\) equals \(\Delta_i\) and \(\phi_{ij} = \phi_i\)
since the subtree \(\tree_{ij}\) contains only the clique \(\clique_i\).

\item[-] \(\alpha \wedge \beta \wedge \phi_{ij}\) is equivalent to 
\(\alpha \wedge \beta \wedge \phi_i\).

\item[-] \(\alpha \wedge \beta \wedge \phi_i\) is equivalent to 
\(\alpha \wedge \phi_i\) since \(\alpha \wedge \beta \wedge \phi_i\) 
is consistent and the atoms in \(\beta\) are a subset of those in 
\(\alpha \wedge \phi_i\).
\end{itemize}
Therefore,
\[ \cons^{\Delta_{ij}}(\beta \wedge \phi_{ij}) \equiv
\bigvee_{\alpha} \cons^{\Delta_i}(\alpha \wedge \phi_i), \]
which is what we need to show.


\para{Inductive step:} Clique \(\clique_i\) has more than one neighbor.

The induction hypothesis is that the call \(\strcons(\clique_k,\clique_i)\)
on line~08 will return a sentence equivalent to
\(\cons^{\Delta_{ki}}(\alpha_{ki} \wedge \phi_{ki})\) where 
\(\alpha_{ki}\) is the instantiation of sepset \(\sepset_{ki}\).

Given this induction hypothesis, we want to show that the call \linebreak 
\(\strcons(\clique_i,\clique_j)\) will return a sentence 
equivalent to \(\cons^{\Delta_{ij}}(\beta \wedge \phi_{ij})\) 
where \(\beta\) is the instantiation of sepset \(\sepset_{ij}\) before 
the call is made.

Given the induction hypothesis and Lemma~\ref{lem:sc-a},
lines~02-10 are setting \(\resa\) to the following expression
\[ \bigvee_{\alpha} \cons^{\Delta_i}(\alpha) 
\wedge \bigwedge_{k \neq j} 
\cons^{\Delta_{ki}}(\alpha_{ki} \wedge \phi_{ki})\]
where \(\alpha\) is the instantiation of clique \(\clique_i\) generated 
in line~03 and \(\alpha_{ki}\) is the project of instantiation \(\alpha\)
on sepset \(\sepset_{ki}\). Note here that \(\alpha\) is guaranteed to be 
consistent with \(\phi\) and \(\beta\) (see the pseudocode of 
\(\ginstantiations\)).

All we need to show then is that this computed expression is equivalent to
\(\cons^{\Delta_{ij}}(\beta \wedge \phi_{ij})\).
By observing that \(\Delta_{ij}\) can be decomposed into \(\Delta_i\)
and \(\Delta_{ki}\) where \(k \neq j\), this equivalence can be 
proven using the Intersection Corollary. Specifically, given that
the atoms in clique \(\clique_i\) contain all atoms that are common 
between any two subtrees \(\tree_{ki}\), the Corollary gives:
\[ \cons^{\Delta_{ij}}(\beta \wedge \phi_{ij})
\equiv \bigvee_{\alpha} 
\cons^{\Delta_i}(\alpha \wedge {(\beta \wedge \phi_{ij})}_{i}) 
\wedge \bigwedge_{k \neq j} 
\cons^{\Delta_{ki}}(\alpha_{ki} \wedge {(\beta \wedge \phi_{ij})}_{ki}).\]
Note that \({(\phi_{ij})}_i = \phi_i\) and
\({(\phi_{ij})}_{ki} = \phi_{ki}\). This leads to
\[ \cons^{\Delta_{ij}}(\beta \wedge \phi_{ij})
\equiv \bigvee_{\alpha} 
\cons^{\Delta_i}(\alpha \wedge \beta_i \wedge \phi_i) 
\wedge \bigwedge_{k \neq j} 
\cons^{\Delta_{ki}}(\alpha_{ki} \wedge \beta_{ki} \wedge \phi_{ki}).\]
The atoms in 
\(\beta_i \wedge \phi_i\) are a subset of the atoms in \(\alpha\). 
Therefore, \(\alpha \models \beta_i \wedge \phi_i\) given that
\(\alpha\) and \(\beta_i \wedge \phi_i\) are consistent.
Similarly, the atoms in \(\beta_{ki}\) are a subset of the atoms in 
\(\alpha_{ki}\). Therefore, \(\alpha_{ki} \models \beta_{ki}\) 
given that \(\alpha_{ki}\) and \(\beta_{ki}\) are consistent.
This leads to
\[ \cons^{\Delta_{ij}}(\beta \wedge \phi_{ij})
\equiv \bigvee_{\alpha} 
\cons^{\Delta_i}(\alpha) \wedge \bigwedge_{k \neq j} 
\cons^{\Delta_{ki}}(\alpha_{ki} \wedge \phi_{ki}).~\eproof\]


\subsection*{Proof of Theorem~\ref{theo:sc-sound}}
To prove that the function \syscons\ terminates, it is 
enough to prove that the calls to \syscons\ will 
not recurse infinitely. To show this, note that all recursive calls
made by \(\strcons(\clique_i,\clique_j)\) are of the form \linebreak 
\(\strcons(\clique_x,\clique_y)\) where the arc
\(\clique_x \uarc \clique_y\) belongs to the subtree 
\(\tree_{ij}\). Therefore, the number of arcs visited by a
recursive call is smaller than the number of arcs visited by
its parent call. The boundary condition is when a call 
\(\strcons(\clique_i,\clique_j)\) is made and 
subtree \(\tree_{ij}\) has a single clique in it.

Proving that the function \syscons\ returns the desired consequence
follows directly from Lemma~\ref{lem:sc-b}. Consider the jointree 
\(\tree'\) and its corresponding \(\Delta'\) that results 
from adding the clique \(\clique_{0} = \emptyset\) as a neighbor to 
the pivot clique \(\clique_z\). We have \(\tree'_{z0} = \tree\), 
\(\Delta'_{z0} = \Delta\), and \(\phi_{z0} = \phi\). Moreover, 
the sepset \(\sepset_{z0}\) is empty and it has one instantiation 
\(\true\). Therefore, by Lemma~\ref{lem:sc-b}, the call on 
line~03 of \(\syscons\) returns 
\(\cons^{\Delta'_{z0}}(\true \wedge \phi_{z0}) = 
\cons^\Delta(\phi)\).~\eproof

\subsection*{Proof of Theorem~\ref{theo:sc-form}}
Suppose that each component consequence \(\ccons_P[.]\) is 
in decomposable NNF.

That the sentence returned by \syscons\ is in NNF follows immediatly given 
that only disjunctions and conjunctions are constructed in 
Figure~\ref{fig:sc} (no negations).

To prove that the sentence is decomposable, we need three results:
\begin{itemize}
\item No assumables are shared between component descriptions,
which follows from the definition of a structured system description.

\item The NNF returned by \(\clscons(\clique_i)\) mentiones only 
assumables that appear in component descriptions assigned to clique 
\(\clique_i\). This follows immediately from examining the 
pseudocode of \(\clscons(\clique_i)\).

\item The NNF returned by \(\strcons(\clique_i,\clique_j)\) mentions
only assumables that appear in component descriptions assigned to 
cliques in subtree \(\tree_{ij}\). This can be shown by induction on 
the structure of a jointree.
\end{itemize}
To prove that the returned NNF is decomposable, all we need to show
is that whenever a conjunction is constructed in Figure~\ref{fig:sc}, 
the conjuncts are guaranteed to share no assumables. There are two places 
where conjunctions are constructed:
\begin{enumerate}
\item \(\clscons\): \(\resb\) is set to the conjunction of consequences 
that correspond to distinct component descriptions. Therefore, they are 
guaranteed to share no assumables.

\item \(\strcons\): \(\resb\) is set to the conjunction of a NNF returned by
\linebreak \(\clscons(\clique_i)\) together with NNFs returned by  \linebreak 
\(\strcons(\tree_{ki})\). These NNFs are guaranteed to share no assumables
since clique \(\clique_i\) and subtrees \(\tree_{ki}\) share no 
assumables.
\end{enumerate}
Therefore, the NNF returned by \(\syscons\) must be decomposable.~\eproof


\begin{lemma} \label{lem:sc-complexity}
In Figure~\ref{fig:sc}, 
the number of calls to \(\strcons(\clique_i,\clique_j)\) that 
will not return from line~01 is no more than 
\(2^{\mid \sepset_{ij} \setminus \E\mid}\).
We will refer to such calls as \underline{non-cached calls}.
\end{lemma}

\subsection*{Proof of Lemma~\ref{lem:sc-complexity}}
By Lemma~\ref{lem:sc-b}, the sepset \(\sepset_{ij}\) is instantiated
when \(\strcons(\clique_i,\clique_j)\) is called. Moreover, the index
of such instantiation is the key used in the cache lookup on line~01 of 
\(\strcons\). The total number of possible keys is
\(2^{\mid \sepset_{ij} \setminus \E \mid}\) since this
is the maximum number of distinct 
instantiations generated for \(\sepset_{ij}\) 
(note that atoms \(\E\) are instantiated during the run of the algorithm). 
In case of a cache hit on line~01, the function returns immediately and 
the call is considered cached. In case of a cache miss, the call is 
non-cached and it will lead to an insertion into the cache on line~11 
of \(\strcons\). Since there are no more than 
\(2^{\mid \sepset_{ij} \setminus \E \mid}\) keys, there are no more 
than \(2^{\mid \sepset_{ij} \setminus \E \mid}\) cache insertions and,
hence, no more than \(2^{\mid \sepset_{ij} \setminus \E \mid}\)
cache misses. Therefore, the maximum number of non-cached calls is 
\(2^{\mid \sepset_{ij} \setminus \E \mid}\).~\eproof


\subsection*{Proof of Theorem~\ref{theo:sc-complexity}}

We will use the following notation:
\begin{itemize}

\item \(\displaystyle 
d_i \definedas \sum_{O \in \comp(\clique_i)} \mid \dag_O \cup \{O\} \mid\).

\item \(\displaystyle 
e_{ij} \definedas d_i + 
            \mid \clique_i \setminus \sepset_{ij} \setminus \E \mid + 
                 \sum_{k \neq j} \mid \sepset_{ki} \mid\) 
where \(\clique_k\) is a neighbor of clique \(\clique_i\).
\end{itemize}
Consider the following observations:
\begin{itemize}

\item The call \(\ginstantiations(\clique_i)\) on line~03 of \(\strcons\)
takes \(O(2^{\mid \clique_i \setminus \sepset_{ij} \setminus \E \mid})\) 
time, which is also the number of instantiations it returns and the 
number of times that lines~04-10 of \(\strcons\) will repeat.

\item The calls \(\assert(\alpha)\) and \(\retract(\alpha)\) on
lines~04 and~10 of \(\strcons\) take 
\(O(\mid \clique_i \setminus \sepset_{ij} \setminus \E \mid)\) time each
since the size of \(\alpha\) is 
\(O(\mid \clique_i \setminus \sepset_{ij} \setminus \E \mid)\).

\item The call \(\clscons(\clique_i)\) on line~06 of \(\strcons\)
takes \(O(d_i)\) time.

\item The call \(\strcons(\clique_k,\clique_i)\) on line~08 takes
\(O(\mid \sepset_{ki} \mid)\) time \underline{if it is cached.}
\end{itemize}
Therefore, lines~04-10 of \(\strcons\) take \(O(e_{ij})\) time assuming that
all calls to \linebreak 
\(\strcons(\clique_k,\clique_i)\) are cached.\footnote{To get the total
cost of lines~04-10, we must also add the cost of non-cached calls to
\(\strcons(\clique_k,\clique_i)\).} If we assume that the number of 
neighbors per clique is a constant and
that the number of components per clique is also a constant,
then \(e_{ij} = O(\mid \clique_i \mid)\).
We will indeed make this assumption in the following proof.

We first show that the time of all non-cached calls to 
\(\strcons(\clique_i,\clique_j)\) is 
\[ 
  O(\sum_{\clique \in \tree_{ij}} 
        \mid \clique \mid 2^{\mid \clique \setminus \E\mid}).
\]

The proof is by induction on the structure of the jointree:
\begin{itemize}
\item {\em Base case:} Clique \(\clique_i\) has only one neighbor 
\(\clique_j\). \\
Line~08 does not execute and the time of a single non-cached call to 
\linebreak \(\strcons(\clique_i,\clique_j)\) is 
\(O(\mid \clique_i \mid 
       2^{\mid \clique_i \setminus \sepset_{ij} \setminus \E \mid})\).
By Lemma~\ref{lem:sc-complexity}, there are no more than
\(2^{\mid \sepset_{ij} \setminus \E \mid}\) non-cached calls to 
\(\strcons(\clique_i,\clique_j)\). The total time of non-cached calls
is then
\[ 2^{\mid \sepset_{ij} \setminus \E \mid}
    O(\mid \clique_i \mid  
         2^{\mid \clique_i \setminus \sepset_{ij} \setminus \E \mid})
 = 
    O(\mid \clique_i \mid  
         2^{\mid \sepset_{ij} \setminus \E \mid + 
     \mid \clique_i \setminus \sepset_{ij} \setminus \E \mid}),
\] 
which is equal to 
\(O(\mid \clique_i \mid 2^{\mid \clique_i \setminus \E \mid})\)
because \(\sepset_{ij}\) is a subset of \(\clique_i\).

Since \(\clique_i\) has only one neighbor \(\clique_j\), the subtree 
\(\tree_{ij}\) contains
only the clique \(\clique_i\). Therefore,
\[  O(\mid \clique_i \mid 2^{\mid \clique_i \setminus \E \mid}) =
   O(\sum_{\clique \in \tree_{ij}} 
      \mid \clique \mid 2^{\mid \clique \setminus \E \mid}).
\]

\item {\em Inductive step:} 
Clique \(\clique_i\) has more than one neighbor. \\
Suppose that for some \(k\), the time of all non-cached calls to 
\linebreak \(\strcons(\clique_k,\clique_i)\) on line~08 is
\[ 
 O(\sum_{\clique \in \tree_{ki}}
      \mid \clique \mid 2^{\mid \clique \setminus \E \mid}). 
\]
By Lemma~\ref{lem:sc-b}, the time of all non-cached calls
to \(\strcons(\clique_i,\clique_j)\) is then 
\[
  \underbrace{2^{\mid \sepset_{ij} \setminus \E \mid} 
               O(\mid \clique_i \mid
                2^{\mid \clique_i \setminus \sepset_{ij} \setminus \E \mid})}_{\mbox{cost assuming recursive calls are cached}}
  + \underbrace{\sum_{k \neq j}
                O(\sum_{\clique \in \tree_{ki}} 
                 \mid \clique \mid 2^{\mid \clique \setminus \E \mid}),}_{\mbox{cost of non-cached recursive calls}}
\]
which reduces to
\[
    O(\mid \clique_i \mid
        2^{\mid \clique_i \setminus \E \mid})
      + \sum_{k \neq j}
           O(\sum_{\clique \in \tree_{ki}}
             \mid \clique \mid 
                2^{\mid \clique \setminus \E \mid})
\]
since \(\sepset_{ij} \subseteq \clique_i\), and then to
\[ O(\sum_{\clique \in \tree_{ij}}
         \mid \clique \mid
             2^{\mid \clique \setminus \E \mid})
\]
since subtree \(\tree_{ij}\) consists of clique \(\clique_j\) and the
subtrees \(\tree_{ki}\) where \(k \neq j\).

\end{itemize}

We are now ready to bound the running time of \(\syscons\):
line~01 costs \(O(1)\); 
line~02 costs \(O(\mid \E \mid)\) time; and
line~03 is bound by the cost of all non-cached calls to \linebreak
\(\strcons(z,0)\), which is
\[ 
  O(\sum_{\clique \in \tree'_{z0}} 
       \mid \clique \mid 
           2^{\mid \clique \setminus \E \mid}) 
= O(\sum_{\clique \in \tree} 
       \mid \clique \mid 
          2^{\mid \clique \setminus \E \mid})
\]
since \(\tree'_{z0} = \tree\).
Therefore, the time of \(\syscons\) is
\(O(\sum_{\clique \in \tree} 
       \mid \clique \mid  2^{\mid \clique \setminus \E \mid})\).

This is also the space complexity of the returned NNF since the addition
of either a node or an arc to the NNF takes \(O(1)\) time.~\eproof





\subsection*{Proof of Theorem~\ref{theo:order}}

\begin{itemize}
\item {\em Reflexive:} \\
For all \(a \in \costs\), \(a \oplus 0 = a\) and, hence, \(a \co a\).

\item {\em Transitive:} \\
Suppose that \(a \co b\) and \(b \co c\). Then these exists \(x\) and
\(y\) such that \(a \oplus x = b\) and \(b \oplus y = c\). Moreover,
\(a \oplus x \oplus y = c\) and, hence, \(a \co c\).

\item {\em Anti-symmetric:} \\
Suppose that \(a \co b\) and \(b \co a\). Then these exists \(x\) and
\(y\) such that \(a \oplus x = b\) and \(b \oplus y = a\). Moreover,
\(a \oplus x \oplus y = a\). This leads to \(x \oplus y = 0\) and,
hence, \(x = 0\) and \(y = 0\). Therefore, \(a = b\).

\item {\em Total:} \\
For all \(a\) and \(b\), either 
\(a \oplus c = b\) or \(a = b \oplus c\) for some unique \(c\).
Hence, for all \(a\) and \(b\), either \(a \co b\) or \(b \co a\).~\eproof
\end{itemize}


\begin{lemma} \label{lem:order-b}
The addition operation of a cost function satisfies the following
properties:
\begin{enumerate}
\item \(a \oplus b = a\) implies \(b = 0\).
\item If \(a \sco b\), then \(a \oplus c \sco b \oplus c\).
\end{enumerate}
\end{lemma}

\subsection*{Proof of Lemma~\ref{lem:order-b}}

\begin{enumerate}
\item We have \(a \oplus 0 = a\). We also have that \(a \oplus b = a\)
for some unique \(b\). Therefore, \(b = 0\).
\item If \(a \sco b\), then \(a \oplus x = b\) and \(x \neq 0\).
We then have \(a \oplus x \oplus c = b \oplus c\), which leads to
\(a \oplus c \leq_\oplus b \oplus c\). Since
\(a \oplus x \oplus c = b \oplus c\) for a unique \(x\), and
since \(x \neq 0\), we have
\(a \oplus c \neq b \oplus c\) and, hence, 
\(a \oplus c \sco b \oplus c\).~\eproof
\end{enumerate}


\begin{lemma} \label{lem:zexts}
In Figure~\ref{fig:extraction}, if the instantiations in set \(\T\) have 
the same cost \(c\), then the instantiations in \(\extend(\T,\S)\) 
will have the same cost \(c\).~\eproof
\end{lemma}
Moreover, we will refer to the instantiations in \(\extend(\T,\S)\) as
the \underline{zero extensions} of the instantiations in \(\T\).

The following lemma is with respect to the algorithm in 
Figure~\ref{fig:extraction}.
\begin{lemma}
\label{lem:pi-sound}
After termination of the algorithm in Figure~\ref{fig:extraction}, 
we have the following for every node \(\mu\) in the NNF-graph \(\tau\) 
and every instantiation \(\alpha\) in \(\terms(\mu)\):
\begin{enumerate}
\item \(\alpha \models \mu\);
\item \(\ct(\mu) = \cf(\alpha)\); and
\item \(\alpha\) is an \(\S\)-instantiation where \(\S\) are all the
atoms appearing in the NNF-graph rooted at \(\mu\).
\end{enumerate}
\end{lemma}

\subsection*{Proof of Lemma~\ref{lem:pi-sound}}
The proof is by induction on the structure of the NNF-graph \(\tau\).

\para{{\em Base case:}} \(\mu\) is a leaf node.

\begin{itemize}
\item {\em Case I:} \(\mu\) is a literal-node. 
Then \(\ct(\mu) = \cf(\lit(\mu)) = \cf(\{\lit(\mu)\})\) and
\(\terms(\mu) = \{\{\lit(\mu)\}\}\). The properties hold.

\item {\em Case II:} \(\mu \equiv \true\) is an and-node. 
Then \(\ct(\mu) = 0 = \cf(\{\})\) and
\(\terms(\mu) = \{\{\}\}\). The properties hold.

\item {\em Case III:} \(\mu \equiv \false\) is an or-node. 
Then \(\ct(\mu) = \infty\) and \(\terms(\mu) = \{\}\).
The properties hold.
\end{itemize}

\para{{\em Inductive step:}} \(\mu\) is a node with children.

Suppose that the property holds for each child \(\mu_i\) of 
\(\mu\) and that \(\alpha \in \terms(\mu)\).

\begin{itemize}
\item {\em Case I:} \(\mu\) is an and-node. 
Then \(\alpha\) has the form \(\bigwedge_i \alpha_i\) where 
\(\alpha_i \in \terms(\mu_i)\).
\begin{enumerate}
\item By the induction hypothesis,
\(\alpha_i \models \mu_i\). Hence, 
\(\bigwedge_i \alpha_i \models \bigwedge_i \mu_i\) 
and \(\alpha \models \mu\) 
since \(\mu \equiv \bigwedge_i \mu_i\).

\item By the induction hypothesis, \(\ct(\mu_i)=\cf(\alpha_i)\).
>From line~04 of \prune, \(\ct(\mu) = \bigoplus_i \ct(\mu_i)\) and, hence,
\(\ct(\mu) = \bigoplus_i \cf(\alpha_i) = \cf(\alpha)\).

\item \(\S = \bigcup_i \S_i\) where \(\S_i\) are the atoms appearing in
child \(\mu_i\). By the induction hypothesis, each \(\alpha_i\) is an 
\(\S_i\)-instantiation. Therefore, \(\alpha\) must be an \(\S\)-instantiation.
\end{enumerate}

\item{\em Case II:} \(\mu\) is an or-node. 
Then \(\alpha\) is the zero extension of some \(\alpha_i \in \terms(\mu_i)\) 
where \(\mu_i\) is a child of \(\mu\) and \(\ct(\mu) = \ct(\mu_i)\). 
\begin{enumerate}
\item By the induction hypothesis, \(\alpha_i \models \mu_i\).
Therefore, 
\(\alpha \models \alpha_i \models \mu_i \models \bigvee_i \mu_i
\models \mu\).

\item By the induction hypothesis, \(\ct(\mu_i)=\cf(\alpha_i)\) and by
Lemma~\ref{lem:zexts}, \(\cf(\alpha_i) = \cf(\alpha)\). Hence,
\(\ct(\mu_i)=\cf(\alpha)\). Since \(\ct(\mu_i)=\ct(\mu)\), we must
then have \(\ct(\mu)=\cf(\alpha)\).

\item By the induction hypothesis, each \(\alpha_i\) is an 
\(\S_i\)-instantiation where \(\S_i\) are the atoms appearing in 
\(\mu_i\). By calling \(\extend(\terms(\mu_i),\atoms(\mu,\mu_i))\),
we are extending each \(\alpha_i \in \terms(\mu_i)\) with one literal
for each atom in \(\atoms(\mu,\mu_i)\). Since 
\(\atoms(\mu,\mu_i) = \S \setminus \S_i\), the result of this extension 
must then be an \(\S\)-instantiation.~\eproof
\end{enumerate}
\end{itemize}

\subsection*{Proof of Theorem~\ref{theo:pi-sound}}
In this theorem, \(\mpi\) is the set of minimal instantiations with respect 
to the cost function \((\atoms(\mu),\Sigma,\oplus,\cf)\) where
\(\atoms(\mu)\) are all atoms appearing in the NNF-graph rooted at \(\mu\).

The proof is by induction on the structure of \(\tau\).

\para{{\em Base case:}} \(\mu\) is a leaf node.

\begin{itemize}
\item {\em Case I:} \(\mu\) is a literal-node. 
Then \(\terms(\mu) = \{\{\lit(\mu)\}\} = \mpi(\mu)\).

\item {\em Case II:} \(\mu \equiv \true\) is an and-node. 
Then \(\terms(\mu) = \{\{\}\} = \mpi(\mu)\).

\item {\em Case III:} \(\mu \equiv \false\) is an or-node. 
Then \(\terms(\mu) = \{\} = \mpi(\mu)\).
\end{itemize}


\para{{\em Inductive step:}} \(\mu\) is a node with children.

Suppose that \(\terms(\mu_i) = \mpi(\mu_i)\) for each child 
\(\mu_i\) of \(\mu\).


\para{  {\em First direction:}} If \(\alpha \in \mpi(\mu)\), then
\(\alpha \in \terms(\mu)\).

Suppose that \(\alpha \in \mpi(\mu)\). Then \(\alpha \models \mu\).
\begin{itemize}
\item {\em Case I:} \(\mu\) is an and-node. \\
Since \(\tau\) is a decomposable NNF, the atoms that appear in each
\(\mu_i\) must be disjoint. Therefore, \(\alpha\) must have the form 
\(\bigwedge_i \alpha_i\) where \(\alpha_i\) is the projection of \(\alpha\) 
on the atoms in \(\mu_i\). Moreover, we must have \(\alpha_i \models 
\mu_i\) for each \(\alpha_i\). It suffices then to show that 
\(\alpha_i \in \terms(\mu_i)\). Suppose that 
\(\alpha_i \not \in \terms(\mu_i)\) for some \(\alpha_i\). By the induction 
hypothesis, \(\alpha_i \not \in \mpi(\mu_i)\). 
Since \(\alpha_i \models \mu_i\), we must then have
\(\ct(\mu_i) <_\oplus \cf(\alpha_i)\). Now let \(\alpha'\) be the result of 
replacing this \(\alpha_i\) in \(\alpha\) with some 
\(\beta_i \in \terms(\mu_i)\). Then \(\alpha' \models \mu\) since 
\(\beta_i \models \mu_i\) by Lemma~\ref{lem:pi-sound}.
Moreover, the cost of \(\alpha'\) must be less than the cost of \(\alpha\)
by Lemma~\ref{lem:order-b}. 
Therefore, \(\alpha\) cannot be in \(\mpi(\mu)\) which is a
contradiction. We then conclude that \(\alpha_i \in \terms(\mu_i)\) 
and, hence, that \(\alpha \in \terms(\mu)\).

\item {\em Case II:} \(\mu\) is an or-node. \\
Since \(\alpha \models \mu\), we must have \(\alpha \models \mu_i\) for 
some child \(\mu_i\) of \(\mu\). Let \(\alpha_i\) be the projection of 
\(\alpha\) on the atoms in \(\mu_i\). 
Then \(\cf(\alpha_i) \leq_\oplus \cf(\alpha)\),
\(\alpha_i \models \mu_i\) and we have one of two cases:

\begin{enumerate}
\item \(\alpha_i \in \terms(\mu_i)\): Then \(\cf(\alpha_i) = \ct(\mu_i)\)
by Lemma~\ref{lem:pi-sound} and we have two cases:

\begin{enumerate}
\item \(\cf(\alpha_i) =_\oplus \cf(\alpha)\): \(\alpha\) is then a zero 
extension of \(\alpha_i\) and, hence, \(\alpha \in \terms(\mu)\).

\item \(\cf(\alpha_i) <_\oplus \cf(\alpha)\): any zero extension of 
\(\alpha_i\) will both entail \(\mu\) and have a lower cost than 
\(\alpha\). This contradicts \(\alpha \in \mpi(\mu)\) and the case is 
impossible.
\end{enumerate}

\item \(\alpha_i \not \in \terms(\mu_i)\): 
By the induction hypothesis, \(\alpha_i \not \in \mpi(\mu_i)\).
Since \(\alpha_i \models \mu_i\), this means that 
\(\ct(\mu_i) <_\oplus \cf(\alpha_i)\). Therefore, the zero extension of any 
\(\beta_i\) in \(\terms(\mu_i)\) will both entail \(\mu\) and have a smaller
cost than \(\alpha\). This contradicts \(\alpha \in \mpi(\mu)\) and the
case is impossible.
\end{enumerate}
\end{itemize}

\para{  {\em Second direction:}} If \(\alpha \in \terms(\mu)\), 
then \(\alpha \in \mpi(\mu)\).

Suppose that \(\alpha \in \terms(\mu)\). We need to show two things:
\begin{itemize}
\item \(\alpha \models \mu\): \\
This follows by Lemma~\ref{lem:pi-sound}.

\item \(\cf(\alpha) = \cf(\gamma)\) for some \(\gamma \in \mpi(\mu)\): \\
Suppose that \(\gamma \in \mpi(\mu)\). We just showed above that 
\(\gamma \in \terms(\mu)\). By Lemma~\ref{lem:pi-sound}, all 
instantiations in \(\terms(\mu)\) have the same cost, which is also the 
cost of \(\gamma\). Therefore, \(\alpha\) and \(\gamma\) must have the 
same cost.
\end{itemize}
This lead to \(\alpha \in \mpi(\mu)\).~\eproof

\subsection*{Proof of Theorem~\ref{theo:pi-complexity}}

The call to \prune\ on line~01 takes \(O(E)\) time. Note that saving the
computed costs is essential since \(\tau\) is a graph, not a tree.
Therefore, without the check on line~01 of \(\prune\), the cost of a node
may be computed more than once since a node can have more than one parent.


The call to \insts\ on line~02 takes \(O({\mid \terms(\tau)\mid}^2 E)\) 
time where the explanation is given below. The total time of the 
extraction algorithm is then \(O({\mid \terms(\tau)\mid}^2 E)\).

\insts\ is similar to \prune\ except that the amount of work done at 
each node \(\mu\) is different. To bound this amount, we first
observe that for any node \(\mu\) with \(\cost(\mu) \neq \infty\) and 
its child \(\nu\):\footnote{If \(\cost(\mu)=\infty\), \(\terms(\nu) = \{\}\)
and the case is handled by line~02 of \insts.}
\begin{equation}
\mid \terms(\nu) \mid \leq \mid \terms(\mu) \mid.
\label{pr:size}
\end{equation}
This follows because:
\begin{itemize}
\item[-] if \(\mu\) is an and-node, then \(\terms(\mu)\) is the cartesian
product of all \(\terms(\nu)\) and, hence, its cardinality cannot be less
than the cardinality of any \(\terms(\nu)\); and
\item[-] if \(\mu\) is an or-node, then \(\terms(\mu)\) is the union of 
all \(\extend(\terms(\nu),\atoms(\mu,\nu))\) and, hence, its cardinality
cannot be less than the cardinality of any \(\terms(\nu)\).\footnote{Note that 
\(\mid \terms(\nu) \mid \leq 
\mid \extend(\terms(\nu),\atoms(\mu,\nu)) \mid \).}
\end{itemize}
Therefore, the computation of \(\terms(\mu)\) takes
\begin{itemize}
\item[-] \(O(\mid \terms(\mu) \mid)\) time if \(\mu\) is an and-node,
which is also the size of the cartesian product 
\[ \terms(\mu) = \bigcap_{\nu \in \children(\mu)} \terms(\nu). \]
\item[-] \(O(\mid \children(\mu) \mid {\mid \terms(\mu) \mid}^2)\) time if
\(\mu\) is an or-node, which is justified as follows:
\begin{enumerate}
\item[-] the union of two sets with sizes \(n\) and \(m\) takes 
\(O(n m)\) time.
\item[-] to compute \(\terms(\mu)\) we must perform 
\(O(\mid \children(\mu) \mid)\) union operations.
\item[-] \(\mid \terms(\nu) \mid \leq \mid \terms(\mu) \mid\)
for all \(\nu\) in \(\children(\mu)\).
\end{enumerate}
\end{itemize}
Therefore, the time to compute \(\terms(\mu)\) is
\(O(\mid \children(\mu) \mid {\mid \terms(\mu) \mid}^2)\)
in the worst case.
The total time taken by \(\insts\) is then
\[ 
\sum_{\mu \in \tau} O(\mid \children(\mu) \mid {\mid \terms(\mu) \mid}^2),
\]
where \(\mu\) denotes a node in the NNF-graph \(\tau\). This reduces to:
\[ 
\sum_{\mu \in \tau} O(\mid \children(\mu) \mid {\mid \terms(\tau) \mid}^2)
\]
since \(\mid \terms(\mu) \mid \leq \mid \terms(\tau) \mid\) for any node 
\(\mu\) in the NNF-graph 
\(\tau\).\footnote{This follows by transitivity of the property in 
Equation~\ref{pr:size} and because \(\tau\) is an ancestor of \(\mu\).} 
Reducing this further, we get:
\begin{eqnarray*}
\lefteqn{{\mid \terms(\tau) \mid}^2 \sum_{\mu \in \tau} 
O(\mid \children(\mu) \mid)} \\
& = &  {\mid \terms(\tau) \mid}^2 O(E) \\
& = &  O({\mid \terms(\tau)}^2 \mid E).~\eproof
\end{eqnarray*}



\vskip 0.2in
\bibliography{/home/darwiche/latex/adam,/home/darwiche/latex/change,/home/darwiche/latex/moises,/home/darwiche/latex/provan1,/home/darwiche/latex/provan2}
\bibliographystyle{theapa}


\end{document}



