\documentstyle[epsf,jair,twoside,11pt,theapa,psfig]{article}

\input epsf %% at top of file
\jairheading{5}{1996}{27-52}{9/95}{8/96}







%\setcounter{page}{0}
%\renewcommand\baselinestretch{2}  

%\renewcommand\floatpagefraction{0.75}  


%\textwidth 16.5cm
%\textheight 23cm
%\oddsidemargin -0.2cm
%\topmargin -2cm

%\topmargin 0in
%\headheight 0in
%\headsep 0in
%\oddsidemargin 0in
%\evensidemargin 0in
%\textheight 9in 
%\textwidth 6.5in
%\parskip 2ex
%\tolerance=10000
%
\begin{document}

\newcounter{trick1}
\newcounter{trick2}
\setcounter{trick1}{1}
\setcounter{trick2}{2}

\ShortHeadings{A Hierarchy of Tractable Subsets}
{Ben-Eliyahu}
\firstpageno{27}

\title{A Hierarchy of Tractable Subsets \\ for Computing
Stable Models}

\author{\name Rachel Ben-Eliyahu \email rachel@cs.bgu.ac.il \\
        \addr Mathematics and Computer Science Department \\
        Ben-Gurion University of the Negev \\
        P.O.B. 653, Beer-Sheva 84105, Israel} 

        	
  \maketitle



\bibliographystyle{theapa}
%\input{macros}

%From rachelb Thu Oct 14 22:32:31 1993

%%% a general purpose macros file


\newtheorem{defi}{Definition}[section]
\newtheorem{lem}[defi]{Lemma}
\newtheorem{theorem}[defi]{Theorem}
\newtheorem{cor}[defi]{Corollary}
\newtheorem{ex}[defi]{Example}
\newtheorem{pro}[defi]{Proposition}
\newtheorem{claim}[defi]{Claim}
\newtheorem{remark}[defi]{Remark}
\newtheorem{Fact}[defi]{Fact}


\newenvironment{proof}{\noindent {\bf Proof:}}%
                      {\qed}


\def\squarebox#1{\hbox to #1{\hfill\vbox to #1{\vfill}}}

\newcommand{\qed}{\hspace*{\fill}
	    \vbox{\hrule\hbox{\vrule\squarebox{.667em}\vrule}\hrule}\smallskip}





\setcounter{secnumdepth}{4}
% new commands

\newcommand{\newc}{\newcommand}

\newc{\comment}[1]{}

%A
\newc{\ael}[1]{\mbox{\mbox{\bf{L}}}#1}
%C
\newc{\card}[1]{\mbox{$|\mbox{#1}|$}}
%D
\newc{\dl}{\mbox{$(D,W)$ \vspace{0.5em}}}
\newc{\dr}{\mbox{$\alpha : \beta / \gamma$}}
%E
\newc{\edge}{\mbox{$\longrightarrow$}}
\newc{\eg}{\mbox{e.\ g.\ }}
\newc{\entails}{\mbox{$\models$}}
\newc{\es}{\mbox{$E^*$}}
\newc{\etal}{\mbox{et al.\ }}
\newc{\ext}{\mbox{$\th{E}$}}
%F
\newc{\false}{\mbox{\bf false}}
%G
%I
\newc{\ie}{\mbox{i.e.}}
\newc{\impl}{\mbox{$ \hspace{0.1em} \Rightarrow \hspace{0.1em}$}}
\newc{\inter}{\mbox{$\bigcap$ }}
%J
%L
%\newc{\land}{\mbox{$\bigwedge$}}
\newc{\lang}{\mbox{$\cal L$}}
\newc{\lc}[1]{\mbox{$#1^*$}}
\newc{\limp}{\mbox{$\longrightarrow$}}
\newc{\limm}{\mbox{$\longleftrightarrow$}}
\newc{\lpimp}{\mbox{$\vspace{0.5em}\longleftarrow\vspace{0.5em}$}}
\newc{\lpneg}{\mbox{{\it not} \vspace{0.5em}}}
\newc{\lpor}{\mbox{\vspace{0.5em} $\mid$ \vspace{0.5em}}}
\newc{\lit}{\mbox{$\lang$}}
%\newc{\lor}{\mbox{$\bigvee$}}
%M
%N
\newc{\nat}{\mbox{$\cal N$}}
\newc{\negg}{\mbox{$\sim$}}
\newc{\notsubseteq}{\mbox{$\subseteq \hspace{-0.8em} / \hspace{0.15em} $}}
\newc{\ncomp}{\mbox{$\comp \hspace{-0.5em} \setminus$}}
\newc{\nmodels}{\mbox{$\models \hspace{-0.8em} \setminus$}}
\newc{\npr}{\mbox{$\prov \hspace{-0.5em} / \hspace{0.25em} $}}
%O
%P
\newc{\parl}{\mbox{$\parallel$}}
\newc{\pnp}{\mbox{$\mbox{$P^{NP[O(\log n)]}$}$}}
\newc{\pr}{\mbox{{\em Proof: }}}
\newc{\prov}{\mbox{$\vdash$}}
\newc{\pvar}{\mbox{\bf \cal V}}
%Q
%R
\newc{\rel}{\mbox{$\cal R$}}
\newc{\res}[2]{\mbox{$res(#1,#2)$}}
\newc{\refi}[1]{\mbox{(\ref{#1})}}
%S
\newc{\st}{\mbox{$\mid$}}
%T
\newc{\tag}[1]{\mbox{$#1^\prime$}}
\newc{\tagg}[1]{\mbox{$#1^{\prime \prime}$}}
\newc{\th}[1]{\mbox{$\mbox{Th}(#1)$}}
\newc{\true}{\mbox{\bf true}}
%U
\newc{\union}{\mbox{$\bigcup$}}
%V
%W
\newc{\wlg}{\mbox{w.\ l.\ g.\ }}
\newc{\wrt}{\mbox{w.\ r.\ t.\ }}



%\input{sp-macros}


%P
\newc{\pti}{\mbox{$\tag{\Pi}$}}


%\input{abst}

\begin{abstract}
Finding the stable models of
a  knowledge base is a significant computational problem in
artificial intelligence. This task is at the
computational heart of truth maintenance systems, 
autoepistemic logic, and default logic.
Unfortunately, it is
NP-hard.  In this paper we present a hierarchy of classes of 
knowledge bases, 
$\Omega_1,\Omega_2,...$, with the following properties:
first,
$\Omega_1$ is the class of all stratified knowledge bases;
second, if a knowledge base  $\Pi$ is in $\Omega_k$, then $\Pi$ has at most
$k$ stable models, and all of them 
may  be found in time $O(lnk)$, where $l$ is the length of the knowledge base 
and $n$ the number of atoms in $\Pi$; 
third, for an arbitrary knowledge base $\Pi$,
we can find the minimum $k$ such that $\Pi$ belongs to $\Omega_k$ in time
polynomial in the size of $\Pi$; and, last, 
where $\cal{K}$ is the class of all knowledge bases, 
it is the case that $\union_{i=1}^\infty \Omega_i = \cal{K}$,
that is, every knowledge base 
belongs to some class in the hierarchy.
\end{abstract}


%\input{intro}

\section{Introduction}
The task
of
computing  the stable models of a knowledge base lies at the heart of three of
the
fundamental systems in Artificial Intelligence (AI): truth maintenance systems
(TMSs), default logic, and autoepistemic logic.
Yet, this task is intractable \cite{elkan,ks:sdl,mt:auto}. In this paper,
we introduce a hierarchy of classes of knowledge bases which achieves 
this task in polynomial time. Membership
in a certain class in the hierarchy is testable in polynomial time.
Hence, given a knowledge base, the cost of computing
its stable models can be bounded prior to the actual computation 
(if the algorithms on which this hierarchy is 
based are used).

First, let us elaborate  the relevance
of computing stable models 
to AI tasks.
We define a knowledge base to be a set of rules of the form
\begin{eqnarray}
\label{cl}
C \lpimp A_1,...,A_m, \lpneg B_1,...,\lpneg B_n
\end{eqnarray}
where $C$, all $A$s, and all $B$s  are atoms in some propositional 
language. Substantial efforts
to 
give a meaning, or semantics, to a knowledge base
have been
made in the logic programming community
 \cite{pp}.
One of the most successful semantics for knowledge bases is {\em stable
model semantics} \cite{bidoit,gl:stable,fine}, which associates any knowledge base with a (possibly empty) set of
models called {\em stable models}.
Intuitively, each stable model represents a set of 
coherent conclusions one might deduce from the knowledge base.
It turns out that stable models
play a central role in some major deductive systems in AI. 
\footnote{
In  logic programming terminology, the knowledge bases  discussed in this
paper are called {\em normal logic programs}.}

\subsection{Stable Models and TMSs} TMSs 
 \cite{Doy79} are inference systems for  nonmonotonic reasoning
with default assumptions. The TMS manages a set of nodes and a set of justifications, where each
node represents a piece of information and the justifications
are rules that state the dependencies between the nodes. The TMS
computes 
a {\em grounded} set of nodes and assigns this set to be the information 
 believed to be true at a given point in time. Intuitively, a set of
believed nodes is grounded if it satisfies all the rules, but 
no node is believed true 
solely on the basis of a circular chain of justifications.
Elkan (1990) pointed
out that  the nodes of a TMS can be viewed as propositional atoms, and the 
set of its justifications as a knowledge base. He  showed that the
task of computing  grounded interpretations for a set of TMS justifications
 corresponds exactly to the task of computing the stable models
of the knowledge base represented by the set of TMS justifications.

\subsection{Stable Models and Autoepistemic Logic} 
Autoepistemic logic  was invented by Moore (1985) in order to formalize the
process of an agent reasoning
about its own beliefs. 
The language of
autoepistemic logic is a propositional language augmented by a 
modal operator $\ael$. Given a theory (a set of formulas) $T$ in autoepistemic logic,  a 
theory $E$ is called a {\em stable expansion} of $T$ iff
\[
E = \lc{(T \union \{ \ael{F} \st F \in E \} \union \{ \neg \ael{F} \st 
F \notin E \})}
\]
where $\lc{T}$ denotes the logical closure of $T$. 
We will now restrict ourselves to a subset of autoepistemic logic in which each formula
is of the form 
\begin{eqnarray}
\label{ae}
A_1 \land ... \land A_m \land  \neg \ael{B_1} \land ... \land \neg \ael{B_n}
\limp C
\end{eqnarray} where $C$, each of the $A$s,
and each of the $B$s are propositional
atoms.
We call this subset the class of {\em autoepistemic programs}.
Every autoepistemic program $T$  can be translated
into a knowledge base $\Pi_T$ by representing the formula
\refi{ae} as the knowledge base rule \refi{cl}. 
Elkan (1990) has shown that $M$ is a stable model of $\Pi_T$ iff there
is  an expansion $E$ of $T$ such that $M$ is the set of all
positive atoms in $E$.  Thus, algorithms for computing stable
models may be used in computing expansions of autoepistemic
programs.
The relationship between
stable model semantics and  autoepistemic logic has also been explored
by Gelfond (1987) and Gelfond and Lifschitz (1988, 1991).

\subsection{Stable Models and Default Logic} Default logic
is a formalism developed by Reiter (1980) for
reasoning with default assumptions.
A default theory can be viewed as a set of defaults,
and a {\em  default} is defined as an expression of the form
\begin{eqnarray}
\frac{\alpha : \beta_1,...,\beta_n }{ \gamma}
\label{disd}
\end{eqnarray}
where $\alpha,\gamma$, and $ \beta_1,...,\beta_n$
are formulas in some  first-order language.
According to Reiter,
$E$ is an extension for a  default theory $\Delta$ iff $E$ coincides
with one of the minimal
deductively closed sets
of sentences $\tag{E}$ satisfying the condition\footnote{
Note the appearance of $E$ in the condition.}
that for any grounded instance of a 
default~(\ref{disd}) from $\Delta$, if $\alpha \in \tag{E}$ 
and $\neg \beta_1,...,\neg \beta_n$ $\notin E$, then 
 $\gamma \in \tag{E}$.

Now consider the subset of  default theories
that
we call {\em  default programs}.  A {\em  default
program}  is a set of defaults of the form
\begin{eqnarray}
\frac{A_{1} \land ... \land A_{m} : \neg B_{1},..., \neg {B_n}}
{C} \label{disp}
\label{ddr}
\end{eqnarray}
in which $C$, each of the $A$s, and each of the $B$s are 
atoms in a propositional language.

Each  default program $\Delta$
can be associated with a knowledge base $\Pi_\Delta$ by replacing
each default of the form~(\ref{ddr})
with the rule \refi{cl}.
%Similarly, each disjunctive KB  $\Pi$
%can be associated with a 
%disjunctive default program $\Delta_\Pi$ by replacing each rule of the form
%\begin{eqnarray}
%C_1 | ... | C_n \lpimp 
%A_{1}, ... , A_{m}, \lpneg  B_{1},...,\lpneg B_{k} 
%\label{dr}
%\end{eqnarray}
%with the default
%\begin{displaymath}
%\frac{L_{k+1} \land ... \land L_{k+m} : \overline{L_{k+m+1}},...,
%\overline{L_{k+m+n}}}{L_1 | ... | L_k}. 
%\end{displaymath}
%\\

Gelfond and Lifschitz (1991)
have shown 
that the logical
closure of a set of atoms $E$ is an extension of $\Delta$
iff $E$ is a stable model of $\Pi_\Delta$.
Algorithms for computing stable models can thus be used in 
computing extensions of Reiter's default theories.


%We hope that the reader is convinced  now that the problem of computing
%stable models is a central computational task in some significant deduction
%systems in AI. 
%In this paper we provide several 
%algorithms for computing stable models.
%and in adition we try to understand better
%the computational difficulties inherent in this task.
\begin{center}
$***$
\end{center}

The paper is organized as follows. In the next section, we define our 
terminology. Section 3  presents two algorithms for 
computing all stable models of a knowledge base. The complexity  of
the first of these algorithms
depends
on the number of atoms  appearing negatively in the knowledge base, while
the complexity of the other algorithm depends
on the number of rules having negative atoms in their bodies.
In Section 4, we present the main algorithm of the paper, called 
{\em algorithm AAS}. Algorithm AAS works from the 
bottom up on the superstructure
of the dependency graph
of the knowledge base and uses the two algorithms presented
in Section 3 as subroutines. Section 5  explains  how the AAS algorithm can be
generalized  to handle knowledge bases over a first-order language.
Finally, in  Sections 6 and 7, 
we discuss related work and make concluding remarks. 
%\input{prelim}

\section{Preliminary Definitions}
\label{prelim}
Recall 
that here a knowledge base is defined as a set of rules of the form
\begin{eqnarray}
\label{pr}
C \lpimp A_1,...,A_m, \lpneg B_1,..., \lpneg B_n
\end{eqnarray}
where $C$, each of the $A$s, and each of the $B$s are propositional atoms.
The expression to the left of $\lpimp$ is called the {\em head} of the rule, 
while the expression
to the right of $\lpimp$ is called the {\em body} of the rule.
%Sometimes we denote the body of a rule by greek letters $\alpha, \beta$ etc.
Each of the
$A$s is said to {\em appear positive} in the rule, and, accordingly,
each of the $B$s
is said to {\em appear negative}
in the rule. 
Rule \refi{pr}
is said to be {\em about} $C$.
%A rule has a negative
%body if all the atoms in its body appear negative.
A rule with an
empty body is called a {\em unit rule}.
Sometimes we will treat a truth assignment
(in other words, interpretation)
in propositional logic as a set of atoms ---
the set of all atoms  assigned  $\true$ by the interpretation.
Given an interpretation $I$ and a set of atoms $A$, $I_A$ denotes
the projection of $I$ over $A$.
Given two interpretations, $I$ and $J$, over  sets of atoms $A$ and $B$,
respectively, 
the interpretation $I+J$ is defined
as follows: 
%if $A$ and $B$ are not consistent (\ie there is an atom
%who gets different assignment in each of them), then $A+B$ is undefined,
%else 
\[
I+J(P)=
\left\{
\begin{array}{ll}
 I(P) & \mbox{ if $P \in A \setminus B$} \\
 J(P) & \mbox{ if $P \in B \setminus A$} \\
 I(P) & \mbox{ if $P \in A \inter B$ and $I(P) = J(P)$} \\
         \mbox{undefined} & \mbox{ otherwise}
\end{array}
\right. 
\]
If
$I(P) =J(P)$ 
for every $P \in A \inter B$,
	we say that
$I$ and $J$ are {\em consistent}.


A {\em partial} interpretation
is a truth assignment
over a subset of the atoms. Hence, a partial interpretation can be
represented as a consistent set of literals: positive literals
represent the atoms that are true, negative literals the
atoms that are false, and the rest are unknown.
%A partial model is a partial interpretation that can be completed
%to be a model. A rule is called Horn if there are no negated atoms in its body.
A knowledge base will be called {\em Horn} if all its rules are Horn. 
 A model
 for a theory (set of clauses) in propositional logic is a truth assignment
that satisfies all the clauses.
If one looks at a knowledge base as
a theory in propositional logic, a Horn knowledge base has a 
unique minimal model (recall that a model $m$ is minimal among a set of models
$M$ iff  there is no  model $\tag{m} \in M$ such that $\tag{m} 
\subset m$).

Given a knowledge base $\Pi$   and a set of atoms $m$,
Gelfond and Lifschitz
defined what is now called  the {\em Gelfond-Lifschitz (GL)
transform} 
of $\Pi$ w.r.t. $m$, which is 
a knowledge base $\Pi_m$ obtained from $\Pi$ by
deleting each rule that has a negative literal $\lpneg P$ in its body
with $P \in m$ and deleting all negative literals in the bodies of the remaining rules.
Note that $\Pi_m$ is a Horn knowledge base. A model $m$ is a {\em stable}
model of a knowledge base $\Pi$ iff it is the unique minimal model of $\Pi_m$
\cite{gl:stable}. 

\begin{ex}
{\rm 
\label{can}
Consider the following knowledge base $\Pi_0$, which will be used as one
of the canonical
examples throughout this paper:
\begin{eqnarray}
warm\_blooded & \lpimp & mammal  \\
live\_on\_land & \lpimp & mammal, \lpneg ab1 \label{r7}\\
female &\lpimp & mammal, \lpneg male \label{r8} \\
male &\lpimp& mammal, \lpneg female \label{r9} \\
mammal & \lpimp & dolphin \\
ab1 & \lpimp &  dolphin \\
mammal & \lpimp & lion \\
lion&\lpimp& 
\end{eqnarray}
$m = \{ lion, mammal, warm\_blooded, live\_on\_land, female\}$
is a stable model of $\Pi_0$.
Indeed, $\Pi_{0_m}$ (the GL transform of $\Pi_0$ w.r.t. $m$)
is
\begin{eqnarray*}
warm\_blooded & \lpimp & mammal \\
live\_on\_land & \lpimp & mammal \\
female &\lpimp& mammal \\
mammal & \lpimp & dolphin \\
ab1 & \lpimp &  dolphin \\
mammal &\lpimp& lion \\
lion & \lpimp &
\end{eqnarray*}
and $m$ is a minimal model of $\Pi_{0_m}$. 
}
\end{ex}


A set of atoms $S$ {\em satisfies
the body} of a rule $\delta$
iff  each atom that appears positive in the body of $\delta$ 
is in $S$ and each
atom that appears negative in the body of $\delta$ is not in $S$. 
A set of atoms $S$ {\em satisfies a rule} iff 
either it does not satisfy its body,
or  it satisfies its body and the atom that appears
in its head belongs to $S$.




A {\em proof} of an atom is a sequence of rules from which the atom
can be derived.
 Formally, we can  recursively define
 when an atom $P$ has a  proof w.r.t. a set of atoms $S$ and
 a knowledge base $\Pi$:
 \begin{itemize}
 \item If the unit rule $P \lpimp$ is in $\Pi$,
 then $P$ has a proof w.r.t. 
 $\Pi$ and $S$.
 \item  If the rule $P \lpimp A_1,...,A_m, \lpneg B_1,..., \lpneg B_n$ is
 in $\Pi$,  and for every $i=1,...,n$ $B_i$ is not in $S$, and for
 every $i=1,...,m$
 $A_i$  already  has
 a proof w.r.t.  $\Pi$ and $S$, then $P$ has a proof w.r.t. $\Pi$
 and $S$.
 \end{itemize}
% iff there is a sequence of rules $\delta_1,...,\delta_n$ from $\Pi$ such that
%\begin{enumerate}
%\item  The body of each $\delta_i$ is satisfied by $S$, and for each $\delta_i$
%the atom in the head of $\delta_i$ belongs to $S$.
%\item $P$ is in the head of $\delta_n$. 
%\item $\delta_1$ has an empty body and, 
%for each $i>1$, each atom that appears positive in the body of $\delta_i$
%is in the head of $\delta_j$ for
%some $1 \leq j < i$. 
%\end{enumerate}

\begin{theorem}{\em \cite{elkan,bd:ilps91}}
\label{proof}
A set of atoms  $S$ is a stable model of a knowledge base $\Pi$ iff
\begin{enumerate}
\item $S$ satisfies each rule in $\Pi$, and
\item for each atom  $P$ in $S$, there is a proof of $P$ w.r.t $\Pi$
and $S$.
\end{enumerate}
\end{theorem}

It is a simple matter to show that the following lemma is true.
\begin{lem}
\label{st}
Let $\Pi$ be a knowledge base, and let $S$ be a set of atoms.
Define:
\begin{enumerate}
\item $S_0 = \emptyset$, and
\item $S_{i+1} = S_i \union \{ P \st P \lpimp A_1,...,A_m, \lpneg B_1, ...
, \lpneg B_n \mbox{ is in } \Pi,$ \\ \mbox{ all of the $A$'s belong to $S_i$
and none of the $B$'s belong to $S$}$\}$.
\end{enumerate}
Then $S$ is a stable model of $\Pi$ iff $S = \union_0^\infty S_i$.
\end{lem}

%\begin{remark}
Observe that although every stable model is
a minimal model of the knowledge base  viewed as a propositional
theory,  not every minimal model is a stable model.
\begin{ex}
{\rm 
Consider the  knowledge base
\begin{eqnarray*}
b &\lpimp& \lpneg a  
\end{eqnarray*}
Both $\{a\}$ and $\{b\}$ are minimal models of the knowledge base above,
but only $\{b\}$ is a stable model of this knowledge base. 
}
\end{ex}
%\end{remark}
Note that a knowledge base may have one or more stable models, or no
stable model
at all. If a knowledge base has at least one stable model, we say that
it is {\em consistent}.

 The {\em dependency graph} of a knowledge base $\Pi$ is  a directed
 graph where each
atom is a node and where 
there is a positive  edge directed from $P$ to $Q$ iff there is 
a rule about $Q$ in $\Pi$ in which  $P$ appears positive in the body.
Accordingly, there is a negative  edge from $P$ to $Q$ iff there is 
a rule about $Q$ in which  $P$ appears negative in the body.
Recall that a 
{\em source} of a directed graph is a node with no incoming edges, while
a {\em sink} is a node with no outgoing edges. Given a directed graph $G$ and
a node $s$ in $G$, the {\em subgraph rooted by $s$} is the subgraph of
$G$  having only nodes $t$ such that there is a path directed from $t$
to $s$ in $G$. The {\em children} of $s$ in $G$
are all nodes $t$ such that there
is an arc directed from $t$ to $s$ in $G$.

\begin{ex}
{\rm 
The dependency graph of $\Pi_0$ is shown in Figure \ref{fig:dep}.
Negative edges are marked ``not.'' The children of {\em mammal}
are {\em lion} and {\em dolphin}. The subgraph rooted by {\em on\_land} is
the subgraph that include the nodes {\em lion}, {\em mammal}, {\em dolphin},
{\em ab1}, and {\em on\_land}. 
}
\end{ex}





\begin{figure}[htbp]
\begin{center}
\leavevmode
\hbox{%
\psfig{figure=dep.eps,height=3.5in}}
\end{center}
	\caption{The dependency graph of $\Pi_0$}
    \label{fig:dep}
\end{figure}



A knowledge base is {\em stratified} iff we can assign each atom $C$ a positive
integer $i_C$ such that for every rule in the form of \refi{pr} above,
for each of the $A$s, $i_A \leq i_C$, and for each of the $B$s,
$i_B < i_C$. It can be readily demonstrated  that
a knowledge base is  stratified iff in its dependency graph there are
no directed cycles going through  negative edges. It is well known
in the logic programming community that  a stratified knowledge base
has a unique stable model that can be found in linear time
\cite{gl:stable,abw:knowledge}.

\begin{ex}
{\rm 
\label{bird}
$\Pi_0$ is not a stratified knowledge base.
The following knowledge base, $\Pi_1$, is stratified (we can assign {\em ab2}
and {\em penguin}
the number $1$, and each of the other atoms the number $2$):
\begin{eqnarray*}
live\_on\_land &\lpimp& bird \\
fly &\lpimp& bird, \lpneg ab2 \\
bird &\lpimp& penguin \\
ab2 &\lpimp& penguin 
\end{eqnarray*}
}
\end{ex}

The strongly connected components of a directed graph $G$ make up a  
      partition of its set of nodes 
      such that, for each subset $S$ in the partition
      and for each $x,y \in S$, there are 
      directed paths from $x$ to $y$ and from $y$ to $x$
      in $G$.  
   The strongly connected components are identifiable in 
linear time \cite{tarjan}.



\begin{figure}[htbp]
\begin{center}
\leavevmode
\hbox{%
\psfig{figure=super.eps,height=3.5in}}
\end{center}
	\caption{The super dependency graph of $\Pi_0$}
    \label{fig:sup}
\end{figure}


The {\em super dependency graph} of a knowledge base $\Pi$, denoted
$G_\Pi$, is the superstructure of the dependency graph of
$\Pi$. That is,  $G_\Pi$ is  a directed graph built by making 
each strongly
connected component in the dependency graph of $\Pi$ into a node
in $G_\Pi$. An arc exists from  a node $s$ to a node $v$ iff
there is an arc from one of the atoms in $s$ to one of the atoms
in $v$ in the dependency graph of $\Pi$. Note that $G_\Pi$ is
an acyclic graph.
\begin{ex}
{\rm
The super dependency graph of $\Pi_0$ is shown in Figure \ref{fig:sup}.
The nodes in the square are grouped into a single node. 
}
\end{ex}

%\input{salg}


\section{Two Algorithms for Computing Stable Models}
\label{twoa}
The main contribution of this paper is the presentation of an algorithm
whose efficiency depends on the ``distance'' of the knowledge base from a stratified
knowledge base. This distance will be measured precisely in Section \ref{all}.
%all.tex is section 4
We will first describe
two other algorithms for computing stable models.
These two algorithms
do not take into account the level of ``stratifiability" of the knowledge base,
that is, they will still work
in exponential time for stratified knowledge bases.
Our main algorithm will use
these two algorithms as procedures.

Given a truth assignment
for a knowledge base, we can verify in polynomial time whether it
is a stable model by using Lemma \ref{st}.
Therefore,  a  straightforward algorithm for computing all stable models
can simply check all possible
truth assignments and determine whether each of them is a stable model.
The time complexity of
this straightforward
procedure will be exponential in the number of atoms used in the knowledge base.
Below, we present
two algorithms that can often function more efficiently than the
straightforward procedure. 



\subsection{An Algorithm That Depends on the Number of Negative 
Atoms in the Knowledge Base}
\label{salg1}
Algorithm {\sc All-Stable1} (Figure \ref{as1}) enables us to
find all the stable
models in time exponential in the number of the atoms that appear negative
in the knowledge base.

The algorithm follows from work on abductive extensions
of logic programming in which stable models
are characterized
in terms of sets of hypotheses that can be drawn as additional
information 
\cite{EsKo89,Dun91,KaMa91}. This is done
by making negative atoms abductible and by imposing appropriate denials
and disjunctions as integrity constraints. The work of
Eshghi and Kowalski (1989), Dung (1991), and Kakas and Mancarella
(1991)
%\cite{EsKo89,Dun91,KaMa91}
 implies the following.

\begin{theorem}
\label{tas1}
Let $\Pi$  be a knowledge base, and let $H$ be the set of atoms that
appear negated in $\Pi$. $M$ is a stable model of $\Pi$
iff there is an interpretation $I$ over $H$ 
  such that
\begin{enumerate}
\item for every atom $P \in H$, if $P \in I$, then $P \in \tag{M}$,  
\item $\tag{M}$ and $I$ are consistent, and  
\item $M = I + $\tag{M},
\end{enumerate}
 where $\tag{M}$ is the
unique stable model of $\Pi_I$.
\end{theorem}

\begin{proof}
The proof follows directly from the definition of
stable models.
Suppose $M$ is a stable model of  a knowledge base 
$\Pi$, and let $H$ be the set of
atoms that appear negative in $\Pi$. Then, by definition,
$M$ is a stable model of  $\Pi_M$. But note that $\Pi_M = \Pi_{M_H}$.
Hence, the conditions of Theorem \ref{tas1} hold for $M$, taking $\tag{M} = M$
and $I = M_H$.
Now, suppose $\Pi$ is a knowledge base and
 $M = \tag{M} + I$, where $\tag{M}$ and $I$ are as in Theorem \ref{tas1}.
Observe that $\Pi_M = \Pi_I$ and, hence, since $\tag{M}$ is a stable
model of $\Pi_I$,
$\tag{M} $ is a stable model of $\Pi_M$. We will show that $M$ is a stable
model of $\Pi_M$.
First, note that by condition 1, $M \subseteq \tag{M}$. 
Thus, $M$ satisfies all the rules in $\Pi_M$ and,
if an atom $P$ has  a proof  $\wrt$$\tag{M}$ and $\Pi_M$, it has also
a proof  $\wrt$$M$ and $\Pi_M$. So,  by Theorem \ref{proof},
$M$ is a stable model of $\Pi_M$ and, by definition, $M$ is a stable
model of $\Pi$.
\end{proof}

Theorem \ref{tas1} implies  algorithm {\sc All-Stable1} (Figure \ref{as1}),
	 which computes  all stable models of a knowledge base $\Pi$.
	 Hence, we have the following complexity analysis.



 
 


\begin{figure}
\fbox{
\parbox{6.0in}{ 
{\sc All-Stable1}$(\Pi)$

Input: A knowledge base $\Pi$. \\
Output: The set of all stable models of $\Pi$.

\begin{enumerate}

\item $\cal{M} := \emptyset$;
\item For each possible interpretation $I$ for the set
 of  all atoms that appear negative in $\Pi$, do:

  \begin{enumerate}
   \item Compute $\tag{M}$, the unique stable model of $\Pi_I$;
   \item If $\tag{M}$ and $I$ are consistent,
    let $\cal{M} :=$ $ \cal{M}$ $ \union \{\tag{M} + I \}$;
  \end{enumerate}
\item Return $\cal{M}$;

\end{enumerate}
 }}
 \caption{Algorithm {\sc All-Stable1}}
 \label{as1}
\end{figure}


\begin{pro}
A knowledge base in which at most  $k$ atoms appear negated
has at most $2^k$ stable models
and all of them
can be found in time $O(nl2^k)$, where $l$ is the size of
the knowledge base and
$n$ the number of atoms used in the knowledge base.
\end{pro}

\begin{proof}
 Follows from the fact that computing $\Pi_I$ and computing the
   unique stable model of a positive knowledge base is $O(nl)$. 
\end{proof}

\subsection{An Algorithm That Depends on the Number of Non-Horn Rules} 


Algorithm {\sc All-Stable2} (Figure
\ref{as2}) depends on the number of rules in which
there are negated atoms.
 It gets as input a knowledge base $\Pi$, 
 and, it  outputs
 the set of all stable models of $\Pi$.
 This algorithm is based upon  the
 observation that a stable model can be built by attempting all possible
 means of satisfying the negated atoms in bodies of
 non-Horn rules. 
Two procedures are called
by  {\sc All-Stable2}: UnitInst, shown in
Figure \ref{ui};
and NegUnitInst, shown in Figure \ref{nui}.
Procedure UnitInst 
 gets as input a knowledge base $\Pi$ and a partial
interpretation $m$. UnitInst 
looks recursively for unit rules in $\Pi$. For each unit
rule $P \lpimp$, if $P$ is assigned $\false$ in $m$, it follows that $m$ cannot
be a part of a model for $\Pi$, and the procedure returns $\false$.
If $P$ is not $\false$ in $m$, the procedure  instantiates $P$ to $\true$ in
the interpretation $m$ and deletes the positive appearances of
$P$ from the body of each rule. It also deletes from $\Pi$ all the
rules about $P$ 
and all the rules in which $P$ appears negative.


\begin{figure}
\fbox{
\parbox{6.0in}{

{\sc All-Stable2}$(\Pi)$ \\

 Input:  A knowledge base $\Pi$. \\
Output:
 The set of all stable models of $\Pi$.
 


\begin{enumerate}
\item $M := \emptyset$;
\item Let $\Delta$ be the set of all non-Horn  rules in $\Pi$.
\item For each subset $S$ of $\Delta$, do: 
\begin{enumerate}
\item $Neg$ =
       $\{  P \st \lpneg P \mbox{ is in the body of some rule in  } S \}$;
\item $\tag{\Pi} := \Pi; $ $m := \emptyset;$
\item If NegUnitInst($\tag{\Pi},Neg,m$), then 
\begin{enumerate}
\item For each $P$ such that $m[P]=null$, let $m[P] := \false$;
\item If $m$ satisfies all the rules in $\Pi$, then  $M := M \union \{m\}$;
\end{enumerate}
 \end{enumerate}
\item EndFor;
\item Return $M$;
\end{enumerate}
 }}
 \caption{Algorithm {\sc All-Stable2}}
 \label{as2}
\end{figure}


Procedure NegUnitInst receives as input a 
knowledge base $\Pi$, a partial interpretation $m$, and
a set of atoms $Neg$. It first instantiates each atom in $Neg$ to $\false$ 
and then updates the knowledge base to reflect this instantiation.
All the instantiations are recorded in $m$. In case of a conflict, namely,
where
the procedure tries to instantiate to $\true$ an atom
that is already set to  $\false$, the procedure returns $\false$;
otherwise, it returns $\true$.




\begin{figure}
\fbox{
\parbox{6.0in}{
UnitInst$(\Pi,m)$ \\
 Input:  A knowledge base $\Pi$ and a partial
interpretation $m$. \\
Output: Updates $m$ using the unit rules of $\Pi$.
	Returns $\false$ if there is a conflict between a unit rule
	and the value assigned to some atom in $m$; otherwise, returns
	$\true$ .
\begin{enumerate}
\item While $\Pi$ has unit rules, do:
\begin{enumerate}
\item Let $P \lpimp$ be a unit rule in $\Pi$;
\item If $m[P] = \false$, return $\false$;
\item $m[P] := \true$; 
\item Erase $P$ from the body of each rule 
in $\Pi$; 
\item Erase from $\Pi$ all rules about $P$;
\item Erase from $\Pi$ all rules in which $P$ appears negative;
\end{enumerate}
\item EndWhile;
\item Return $\true$;
\end{enumerate}
 }}
 \caption{Procedure UnitInst}
 \label{ui}
\end{figure}

\begin{figure}
\fbox{
\parbox{6.0in}{
NegUnitInst($\Pi,Neg,m$) \\
 Input:  A knowledge base $\Pi$, a set of atoms $Neg$, and a partial
interpretation $m$. \\
Output: Updates $m$ assuming the atoms in  $Neg$ are false.
	Returns $\false$ if inconsistency is detected; 
	otherwise, returns $\true$.
\begin{enumerate}
\item For each atom $P$ in $Neg$
\begin{enumerate}
\item  $m[P]:=\false$;
\item Delete from the body of each rule in $\Pi$ each occurrence of $\lpneg P$;
\item Delete from $\Pi$ each rule in which $P$ appears positive in the body;
\end{enumerate}
\item EndFor;
\item Return UnitInst$(\Pi, m)$;
\end{enumerate}
 }}
 \caption{Procedure NegUnitInst}
 \label{nui}
\end{figure}

\begin{pro}
Algorithm {\sc All-Stable2} is correct, that is, $m$ is a stable model
of a knowledge base $\Pi$ iff it is generated by {\sc All-Stable2}$(\Pi)$.
\end{pro}

\begin{proof}
Suppose $m$ is a stable model of  a knowledge base 
$\Pi$. Then, by Theorem \ref{proof}, every atom set to $\true$ in $m$
has a proof $\wrt$$m$ and $\Pi$.
Let $S$ be the set of all non-Horn rules whose bodies
are satisfied by $m$. Clearly, at some point  this $S$ is checked
at step 3 of algorithm {\sc All-Stable2}. When this happens, all atoms
that have a proof $\wrt$$m$ and $\Pi$ will be set to $\true$
by the procedure NegUnitInst (as can be proved by induction on
the length of the proof). Hence, $m$ will be generated.

Suppose $m$ is generated by {\sc All-Stable2}($\Pi$). Obviously,
every rule in $\Pi$ is satisfied by $m$ (step 3.c.ii), and every
atom set to $\true$ by NegUnitInst has a proof $\wrt$$m$ and $\Pi$
(as is readily observable from the way NegUnitInst works).
Hence, by Theorem \ref{proof}, $m$ is a stable model of $\Pi$.
\end{proof}




\begin{pro}
A knowledge base having $c$ non-Horn rules 
has at most $2^c$ stable models and all of them
can be found in time $O(nl2^c)$, where $l$ is the size of
the knowledge base and
$n$ the number of atoms used in the knowledge base.
\end{pro}

\begin{proof}  Straightforward, by induction on $c$. \end{proof}
\begin{ex}
{\rm
Suppose we call {\sc All-Stable2} with $\Pi_0$ as the input knowledge base.
At step 2, $\Delta$ is the set of rules \refi{r7}, \refi{r8}, and
\refi{r9}. When subsets of $\Delta$ which include both
rules \refi{r8} and \refi{r9} are considered at step 3, NegUnitInst will return
$\false$ because UnitInst will detect inconsistency.
When the subset containing both rules \refi{r7} and \refi{r8}
is considered, the stable model $S1$ of Table \ref{t:s1} will be generated.
When the subset containing both rules \refi{r7} and \refi{r9}
is considered, the stable model $S2$ of Table \ref{t:s1} will be generated.
When all the other subsets that do not contain both rules \refi{r8}
and \refi{r9} are tested at step 3, the $m$ generated will not
satisfy all the rules in $\Pi$ and, hence, will not appear in the output.
}
\end{ex}



\begin{small}
\begin{table}
\begin{center}
\begin{tabular}{|c|| c c  c c c c c c|} \hline 
&{\bf lion}& {\bf dolphin} & {\bf ab1} & {\bf mammal} &{\bf warm\_b}& 
{\bf on\_land}& {\bf male } & {\bf female}
 \\ \hline
$S1$ & $T$ & $F$ & $F$ & $T$ & $T$ & $T$
 &$F$ & $T $\\ \cline{2-9}
$S2$ & $T$ & $F$ & $F$ & $T$ & $T$ & $T$
 &$T$ & $F $\\ \hline
\end{tabular}
\caption{Models generated by Algorithm {\sc All-Stable2}}
\label{t:s1}
\end{center}
\end{table}
\end{small}


Algorithms {\sc All-Stable1} and {\sc All-Stable2} 
do not take into account the structure of the knowledge base.
For example, they are
not polynomial for the class of stratified knowledge bases.
We present next an algorithm that exploits the structure
of the knowledge base.


%\input{all}

\section{A Hierarchy of Tractable Subsets Based on the Level
of Stratifiability of the Knowledge Base}
\label{all}
Algorithm {\sc Acyclic-All-Stable} (AAS) in Figure \ref{tree}
exploits the structure of the  knowledge base as it is reflected in 
the  super dependency graph of the knowledge base.
It computes all stable models while traversing the
super dependency graph from the bottom up,
using the algorithms for computing stable models
presented in the previous section as subroutines.


Let $\Pi$ be a knowledge base. 
With each node $s$ in $G_\Pi$ (the super dependency graph of $\Pi$),
we associate $\Pi_s$, $A_s$, and $M_s$. $\Pi_s$ is the subset  
of $\Pi$  containing all the rules about the atoms in $s$,
$A_s$
is the set of all atoms in the subgraph of $G_\Pi$ rooted
by $s$,
and $M_s$ is the set of %partial
stable models associated with
the subset of the knowledge base $\Pi$ which contains only rules about 
atoms in $A_s$. 
 Initially, $M_s$ is empty for 
every $s$.
The algorithm  traverses   $G_\Pi$ from the bottom 
up. When at a node $s$, it first combines all the submodels
of the children
%\footnote{The children of a node $s$ in the graph are defined
%here to be all the nodes $t$  such that there is an arc
%directed from $t$ to $s$.}
of $s$ into a single set of  models
$M_{c(s)}$. If $s$ is a source, then $M_{c(s)}$ is set to
$\{ \emptyset\}$\footnote{Note the difference between $\{\emptyset\}$, which
is a set of one model - the  model that assigns $\false$ to all the atoms,
and $\emptyset$, which is a set that contains no models.}.
Next, for each model $m$ in $M_{c(s)}$, AAS 
converts $\Pi_s$ to a knowledge base
$\Pi_{s_m}$  using the GL transform and other
transformations that depend on the atoms in $m$;
 then, it finds all the
stable models of $\Pi_{s_m}$ and combines them with $m$. The set 
$M_s$ is obtained by repeating this operation for each $m$
in $M_{c(s)}$. AAS uses the procedure
CartesProd (Figure \ref{cart}),
which receives as input several sets of models and returns the
 consistent portion of their Cartesian product. 
  If one of the sets of models which
CartesProd gets as  input is the empty set, CartesProd will output
an empty set of models.
The procedure Convert gets as input a knowledge base $\Pi$, a model
$m$, and a set of atoms $s$, and performs the following: 
for each atom $P$ in $m$, 
each positive occurrence of
$P$ is deleted from  the body of each rule in $\Pi$; 
for each rule in $\Pi$, if $\lpneg P$ is in the body of the rule
and $P \in m$, then the rule is deleted from $\Pi$; if $\lpneg P$ is in the
body of a rule and $P \notin m$,  then,  if $P \notin s$, 
$\lpneg P$ is deleted from that body.
The procedure {\sc All-Stable} called by AAS may be one
of the procedures previously presented  
({\sc All-Stable1} or {\sc All-Stable2}) 
 or it may be any other procedure that generates all
stable models.



\begin{figure}
\fbox{
\parbox{6.0in}{ 
{\sc Acyclic-All-Stable}($\Pi$) \\
Input: A knowledge base $\Pi$. \\
Output: The set of all stable models of $\Pi$.

\begin{enumerate}

\item Traverse $G_\Pi$ from the bottom up. For each node $s$, do:
\begin{enumerate}
\item $M_s := \emptyset$;
\item Let $s_1,...,s_j$ be the children of $s$.
\item If $j=0$, then $M_{c(s)}:= \{ \emptyset \}$; \\
else $M_{{c(s)}} :=$ CartesProd$(\{M_{s_1},...,M_{s_j}\})$; 
\item For each $m \in M_{{c(s)}}$, do:
\begin{enumerate}
\item $\Pi_{s_m}:=$ Convert$(\Pi_s,m,s)$;
%\item Inst($\Pi_{s_m},m$);
\item M := {\sc All-Stable}$(\Pi_{s_m})$;
\item If $M \neq \emptyset$, then $M_s:=M_s \union$CartesProd$(\{\{m\},M\})$;
\end{enumerate}
\end{enumerate}
\item Output CartesProd($\{M_{s_1},...,M_{s_k}\}$), where $s_1,...,s_k$
are the sinks of $G_\Pi$.
\end{enumerate}
 }}
 \caption{Algorithm {\sc Acyclic-All-Stable} (AAS) }
 \label{tree}
\end{figure}


\begin{figure}
\fbox{
\parbox{6.0in}{ 
CartesProd($\cal{M}$) \\
Input: A set of sets of models $\cal{M}$. \\
Output: A set of models which is
the consistent portion of the Cartesian product of the sets in $\cal{M}$.
\begin{enumerate}
\item If $\cal{M}$ has a single element $\{E\}$, then  return $E$; 
\item $M := \emptyset$;
\item Let $\tag{M} \in \cal{M}$; 
\item $D :=$ CartesProd($\cal{M} \setminus \{\tag{M}\}$);
\item For each $d$ in $D$, do:
\begin{enumerate}
\item For each $m$ in $\tag{M}$, do: 
\begin{description}
\item[]
 If $m$ and $d$ are consistent, then $M := M \union \{m+d\}$;
\end{description}
\item EndFor;
\end{enumerate}
\item EndFor;
\item Return $M$;
\end{enumerate}
 }}
 \caption{Procedure CartesProd}
 \label{cart}
\end{figure}

\begin{ex}
{\rm 
Suppose  AAS is called to compute the stable
models of $\Pi_0$.
Suppose further that the algorithm  traverses the super dependency graph
in Figure \ref{fig:sup} in the order \{{\em lion}, {\em dolphin}, {\em mammal},
{\em ab1}, {\em on\_land}, {\em warm\_blooded}, {\em female-male}\}
(recall that all the nodes
inside the square make up
one node that we are calling  female-male or, for short,  FM). 
After visiting all the nodes except the  last,
we have $M_{lion} = \{\{lion\}\}$,
$M_{dolphin}=\{ \emptyset\}$, $M_{mammal} = \{\{lion,mammal\}\}$,
$M_{on\_land} = \{\{lion, mammal, on land\}\}$,
$M_{warm\_blooded} = \{\{lion, mammal, warm\_blooded\}\}$.
When visiting the node FM, we have after step 1.c that
$M_{c(FM)} = M_{mammal}$. So  step 1.d loops 
only once, for $m=\{lion,mammal\}$. Recall that $\Pi_{FM}$
is the knowledge base 
\begin{eqnarray*}
female &\lpimp & mammal, \lpneg male \\
male &\lpimp& mammal, \lpneg female \\
\end{eqnarray*}
After executing step 1.d.\roman{trick1}, we have $\Pi_{{FM}_m}$ set to
\begin{eqnarray*}
female &\lpimp &  \lpneg male \\
male &\lpimp&  \lpneg female \\
\end{eqnarray*}
The above knowledge base has two stable models: $\{female\}$ and $\{male \}$.
The Cartesian product of the above set with $\{lion, mammal\}$
 yields $M_{FM} =
$ $\{ \{lion, mammal, female \}, $ $\{lion, mammal, male \}\}$.
At step 2, the Cartesian product of
$M_{warm\_blooded}$, $M_{on\_land}$, and $M_{FM}$ is taken.
Thus, the algorithm outputs
$\{ \{lion, mammal, on\_land, warm\_blooded, female \}$, \\
$\{lion, mammal, on\_land, warm\_blooded,  male \}\}$,
and these are indeed the two stable models of $\Pi_0$.
Note that algorithm AAS is  more efficient than either 
{\sc All-Stable1} or {\sc All-Stable2} on the knowledge base $\Pi_0$.
}
\end{ex}



\begin{theorem}
\label{acyc}
Algorithm AAS is correct, that  is, $m$ is a stable model
of a knowledge base $\Pi$ iff 
$m$ is generated by 
AAS when  applied to $\Pi$.
\end{theorem}

\begin{proof} Let $s_0,s_1,...,s_n$ be the ordering of the nodes of
the super dependency graph by which the algorithm is 
executed. We can show by induction on $i$ that AAS, when at node $s_i$,
 generates all and only the stable models of the portion of the knowledge base
composed of rules that only use atoms from $A_{s_i}$.
\begin{description}
\item[case $i=0$:] In this case, at step 1.d.\roman{trick2} of 
AAS, $\Pi_{s_m}=\Pi_s$; thus, the claim follows from the correctness
of the algorithm {\sc All-Stable} called in step 1.d.\roman{trick2}.

\item[case $i>0$:]
Showing that
 every model generated
is stable
is straightforward, by
the induction hypothesis and Theorem \ref{proof}.
The other direction is: suppose $m$ is a stable model of $\Pi_s$;
show that $m$ is generated. Clearly, for each child $s$ of $s_i$,
the projection of $m$ onto $A_s$ is a stable model of the part of the
knowledge base that uses only atoms from $A_s$. By induction,
 $m_c$,
which is the projection of $m$ onto the union of $A_s$ for every child $s$ of
$s_i$, must belong to $M_{c(s_i)} $ computed at step 1.c.
Therefore,  to show that $m$ is generated, we need only show 
 that $\tag{m}=m - m_c$ is a stable model
of $\Pi_{{s_i}_{m_c}}$. This is easily done using
Theorem \ref{proof}.
\end{description}
\end{proof}

We will now analyze the complexity of AAS.
First, given a knowledge base $\Pi$ and a set of atoms $s$,
we define $\hat{\Pi}_s$ to be the knowledge base obtained from $\Pi$ by
deleting 
each negative occurrence of
an atom that does not belong to $s$
from the body of every rule. 
For example,
if $\Pi =$ $\{ a \lpimp \lpneg b, c \lpimp \lpneg d, a\}$ and
$s=$ $\{b\}$, then $\hat{\Pi}_s=$ $\{ a \lpimp \lpneg b, c \lpimp  a\}$.
While visiting a node $s$
during the execution of 
AAS, 
we have to compute
at step 1.d.\roman{trick2} 
all stable models of some knowledge base $\Pi_{s_m}$. Using either 
{\sc All-Stable1} or {\sc All-Stable2}, the estimated time required 
to find all stable models of $\Pi_{s_m}$ is shorter than or equal to the
time required to find all stable models of $\hat{\Pi}_s$.
This occurs because
the number of negative atoms and the number of rules with
negative atoms in their bodies in $\hat{\Pi}_s$ is higher than or equal to the 
number of negative atoms and the number of rules with
negative atoms in their bodies in ${\Pi}_{s_m}$, regardless of what $m$ is. 
Thus,
if  $\hat{\Pi}_s$ is a Horn knowledge base, we 
 can
find the stable model of $\hat{\Pi}_s$,
and hence  of $\Pi_{s_m}$,
in polynomial time, no matter what
$m$ is. If $\hat{\Pi}_s$ is not
positive, then we can find all stable models of $\hat{\Pi}_s$,
and hence of $\Pi_{s_m}$, in time
min$(ln*2^k,ln*2^c)$,
where $l$ is the length of $\hat{\Pi}_s$, $n$ the number
of atoms used in $\hat{\Pi}_s$, $c$ the number of rules
in $\hat{\Pi}_s$ that contain negative atoms,
and $k$ the number of atoms that appear negatively in $\hat{\Pi}_s$.
%In other wards, reconsidering again the definition of $\hat{\Pi}_s$
%few lines ago, for every $m$ we consider in the For loop in step 4 of
%the algorithm, we can find a stable model of ${\Pi}_{s_m}$ in time
%min$(l*2^k,l*c!)$
%where $l$ is the length of ${\Pi}_s$, $c$ is the number of rules
%in ${\Pi}_s$ that contain negative atoms from $s$,
%and $k$ the number of atoms from $s$ that appear negatively in $\Pi_s$.

Then, with each knowledge base $\Pi$, we  associate  a number $t_\Pi$ as
follows.  Associate a number $v_s$ with every node 
in $G_\Pi$.  If 
 $\hat{\Pi}_s$ is a Horn knowledge base, then $v_s$ is
1; else, $v_s$ is $min(2^k,2^c)$, where  
  $c$ is the number of rules
in $\hat{\Pi}_s$ that contain negative atoms from $s$,
and $k$ is the number of atoms from $s$ that appear negatively in $\hat{\Pi}_s$.
Now associate a number $t_s$ with every node $s$.
If $s$  is a leaf node, then $t_s=v_s$. If $s$ has children 
$s_1,...,s_j$ in $G_\Pi$, then  $t_s = v_s * t_{s_1}*...*t_{s_j}$.
Define $t_\Pi$ to be
$t_{s_1}*...*t_{s_k}$, where $s_1,...,s_k$ are all the
sink nodes in $G_\Pi$.

\begin{defi}
A knowledge base $\Pi$ belongs to $\Omega_j$ if
$t_\Pi = j$.
\end{defi}


\begin{theorem}
If a knowledge base belongs to
$\Omega_j$ for some $j$, then it has  at most $j$ stable
models that can be computed in time $O(lnj)$.
\end{theorem}


\begin{proof}
 By induction on $j$. The dependency graph and the super dependency graph
are both built in time linear in the size of the knowledge base. So 
we may only   consider the time it takes to compute all stable
models with the super dependency graph  given.
\begin{description}
\item[case $j=1$:] $\Pi \in \Omega_1$ means that for every node $s$
in $G_\Pi$, $\hat{\Pi}_s$
is a Horn knowledge base. In other words, $\Pi$
is stratified, and therefore it has exactly one stable model. 
There are at most $n$ nodes in the graph.
At each node, the loop in step 1.d is executed at most once, because
at most one model is generated 
at every node.
Procedure Convert runs in time $O(l_s)$, where
$l_s$ is the length of $\Pi_s$ (we assume that $m$ is stored in an array
where the access to each atom is in constant time).
Since,
for every node $s$, $\hat{\Pi}_s$ is a Horn knowledge base,
$\Pi_{s_m}$ is computed in time $O({l_s}n)$.
Thus, the overall complexity is $O(ln)$.

\item[case $j>1$:]
By induction on $n$, the number of nodes in the super dependency graph
of $\Pi$.
\begin{description}
\item[case $n=1$:] Let $s$ be the single node in $G_\Pi$. Thus, $j=v_s$.
Using the algorithms from Section \ref{twoa},
%section 3
all stable models 
of $\Pi = \Pi_s$ can be found in time $O(lnv_s)$, and $\Pi$ has
at most $v_s$ models.

\item[case $n > 1$:]
Assume without loss of generality that $G_\Pi$ has a single sink $s$
(to get a single sink, 
we can add to the program the rule $P \lpimp s_1,..,s_k$,
where $s_1,...,s_k$ are all the sinks and $P$ is a new atom).
Let $c_1,...,c_k$ be  the children of $s$. For each child $c_i$,
$\Pi(c_i)$, the part of the knowledge base which corresponds to the 
subgraph rooted by $c_i$, must belong to $\Omega_{t_i}$ for some $t_i \leq j$. 
By induction on $n$, for each child node
$c_i$, all  stable models of $\Pi(c_i)$ can be computed in time
$O(lnt_i)$, and $\Pi(c_i)$ has at most $t_i$ stable models.
Now let us observe what happens when AAS is visiting node $s$.
First, the Cartesian product of all the models computed
at the child nodes is taken. This is executed in time
$O(n*t_1 *...*t_k)$, and yields at most $t_1*...*t_k$ models in $M_{c(s)}$.
 For every $m \in M_{c(s)}$,  we call Convert ($O(ln)$)  and compute
 all the stable models of $\Pi_{s_m}$ ($O(lnv_s)$).  We then
 combine them with $m$ using CartesProd ($O(nv_s)$). Thus, the overall
 complexity of computing $M_s$, that is, of computing
 all the stable
 models of $\Pi$, is $O(lnt_1*...*t_k*v_s)$ $=O(lnj)$.

%By the discussion before this theorem, 
%a stable model of $\hat{\Pi}_s$ can be
%computed in time $O(lnv_s)$. So all stable models of $\Pi$ can be
%computed in time $v_s*t_1*...*t_k=j$.
\end{description}
\end{description}
\end{proof}
%Since algorithm AAS
%computes in each node the set of all stable models of the program represented
%by the sub graph rooted by $s$, we can assume with out loss of generality that
%$$s^*$ is a sink in $G_\Pi$.



Note that all stratified
knowledge bases belong to $\Omega_1$, and the more that any knowledge base 
looks  stratified, the more efficient algorithm
AAS will be.

Given a knowledge base $\Pi$, it is easy to find the minimum  $j$
such that $\Pi$ belongs to $\Omega_j$. This follows because 
building $G_\Pi$  and finding $c$ and $k$ for every node
in $G_\Pi$ are polynomial-time tasks. Hence,


\begin{theorem}
Given a knowledge base $\Pi$, we can find the minimum $j$ such that
$\Pi$ belongs to
$\Omega_j$  in polynomial time. 
\end{theorem}


\begin{ex}
{\rm 
For all the nodes $s$ in $G_{\Pi_0}$
except FM, $v_s$=1.   $v_{FM}=2$. 
Thus,  $\Pi_0 \in \Omega_2$.
$\Pi_1$ is a stratified  knowledge base and therefore belongs to $\Omega_1$.
}
\end{ex}
%for example:
%
%\begin{theorem}
%If the knowledge base $\Pi$ is consistent (that is, has at least one stable model)
%then for every node $s$ in  $G_\Pi$, every submodel $m$ in $M_s$
%($M_s$ as computed in step 1 of algorithm $Acyc-All-Stable$) is 
%a subset of some stable model of $\Pi$.  Moreover, if an atom $P \in A_s$
%is not in any $m \in M_s$, there is no model of $\Pi$ that contains $P$.
%\end{theorem}
%



\begin{figure}[htbp]
\begin{center}
\leavevmode
\hbox{%
\psfig{figure=bigsuper.eps,height=3.5in}}
\end{center}
	\caption{The super dependency graph of $\Pi_0 \union \Pi_1$}
    \label{fig:bigsuper}
\end{figure}




\begin{figure}[htbp]
\begin{center}
\leavevmode
\hbox{%
\psfig{figure=rachel.eps,height=3.5in}}
\end{center}
	\caption{Super dependency graph of $\Pi_4$} 
    \label{fig:cart}
\end{figure}

\begin{figure}[htbp]
\begin{center}
\leavevmode
\hbox{%
\psfig{figure=ab.eps,height=3.5in}}
\end{center}
	\caption{Dependency graph (1) and super dependency graph (2) of $\Pi_2$} 
    \label{fig:ab}
\end{figure}

The next example shows that step 5 of procedure CartesProd is necessary.
\begin{ex}
{\rm
\label{ex:cart}
Consider knowledge base $\Pi_4$:
\begin{eqnarray*}
a & \lpimp & \lpneg b \\
b & \lpimp & \lpneg a \\
c & \lpimp & a \\
d & \lpimp & b \\
e & \lpimp & c, d \\
f & \lpimp & c
\end{eqnarray*}
The super dependency graph of $\Pi_4$ is shown in Figure \ref{fig:cart}.
During the run of algorithm AAS, $M_{ab}$ (the set of  models
computed at the node $\{a,b\}$)  is set to $\{\{a,  \neg b\},\{\neg a,
b\}\}$. When AAS visits nodes $c$ and $d$, we get
$M_{c} =$ $ \{ \{ a, \neg b, c \},$ $ \{ \neg a,
b \}\}$, 
$M_{d} =$ $ \{ \{ \neg a, b , d \},$ $ \{ a,
\neg b\}\}$.
When AAS visits node $e$, CartesProd is called on the input
$\{ M_c, M_d \}$, yielding the output $M_e =$
$\{ \{ a, \neg b, c \},$ $ \{ \neg a,
b , d\}\}$. Note that CartesProd does not output
any model in which both $c$ and $d$ are {\bf true}, because the models
 $\{ a, \neg b, c \}$ and  
$\{ \neg a, b , d \}$ are inconsistent and CartesProd checks 
for consistency in step 5. When visiting node $f$, we get
$M_f =$
 $ \{ \{ a, \neg b, c , f \},$ $ \{ \neg a,
b \}\}$. AAS then returns CartesProd$(\{M_e, M_f\})$, which
is
 $ \{ \{ a, \neg b, c , f \},$ $ \{ \neg a,
b , d\}\}$. 
}
\end{ex}





The next example demonstrates that some  models generated
at some nodes of the super dependency graph during the run of AAS may 
later be deleted, since they
cannot be completed to a stable model of the whole knowledge base.

\begin{ex}
{\rm 
\label{ed}
Consider knowledge base $\Pi_2$:
\begin{eqnarray*}
a & \lpimp & \lpneg b \\
b & \lpimp & \lpneg a \\
c & \lpimp & a, \lpneg c 
\end{eqnarray*}
The dependency graph
and  the super dependency graph  of $\Pi_2$ are shown
in Figure \ref{fig:ab}.
During the run of algorithm AAS, $M_{ab}$ (the set of  models
computed at the node $\{a,b\}$)  is set to $\{\{a\},\{b\}\}$.
However, only $\{b\}$  is a stable model of $\Pi_2$. 
}
\end{ex}

Despite the deficiency illustrated in Example \ref{ed},
algorithm AAS does have desirable features.
%The theorem above has few useful computational implications.
First,  AAS enables us 
to compute stable models in a modular fashion.
We can use $G_\Pi$ as a  structure in which to store the stable models.
Once the knowledge base is changed, we need to resume computation 
only at the 
nodes affected by the change. For example, suppose that after computing
the stable models of the knowledge base $\Pi_0$, we add to $\Pi_0$ the knowledge base
$\Pi_1$ of Example \ref{bird}, which gives us a new knowledge base, 
$\Pi_3 = \Pi_0 \union \Pi_1$. The super dependency graph of the new knowledge base
$\Pi_3$ is shown in Figure \ref{fig:bigsuper}. Now we need only to compute
the stable models at the nodes {\em penguin}, {\em bird},
{\em ab2}, {\em fly}, and {\em on\_land}
and then to combine the models generated at the sinks.
We do not have to re-compute the stable models at all the other nodes as well.


Second, in using the AAS algorithm,
we do not always have to compute all  stable models up to the
root node. If we are  queried
about an atom that is somewhere in the middle of
the graph, it is often  enough to compute only the models of the subgraph rooted
by the node that represents this atom. For example, suppose 
we are given the knowledge base $\Pi_2$ 
and asked if {\em mammal} is {\bf true} in every stable
model of $\Pi_2$. We can run AAS for the nodes
{\em dolphin}, {\em lion}, and {\em mammal}
--- and then stop. If  {\em mammal} is {\bf true} in
all the  stable models computed at the node {\em mammal} (\ie, 
in all the  models
in $M_{mammal}$), we answer ``yes'', otherwise, we  must continue 
the computation.
%has stable models,
%in some of them mammal is $\false$.
%For there are two 
%possibilities: either $\Pi_2$ has  stable models, in which  case every
% stable model of $\Pi_2$ projected on $A_{mammal}$ (the set of all atoms
%having a path to $mammal$) must belong to $M_{mammal}$, or $\Pi_2$ has no
%stable models, in which case if the answer was "yes", we are still right,
%and if the answer was Maybe - of course we are right.
%it was conditioned on the knowledge base being 
%consistent, but it is not, so it was also a reliable answer.



Third, the AAS algorithm is useful in computing the 
labeling of a TMS subject
to nogoods. A set of nodes of a TMS can be declared  {\em nogood},
which means that all acceptable labeling should assign $\false$
to at least one node in the nogood set.\footnote{In logic programming
terminology nogoods are simply integrity constraints.}
In stable models terminology, this means that when handling nogoods, we  look
for stable models in which at least one atom from a nogood is
$\false$. A straightforward approach would be to first
compute all the stable models
and then choose only the ones that comply with the nogood constraints.
But since the AAS algorithm is modular and works from the
bottom up, in many cases
it  can
prevent the generation of unwanted stable models at an early stage.
During the computation,
we can exclude
the submodels that do not comply with the nogood constraints and erase
these submodels
from $M_s$ 
once we are at a node $s$ in the super dependency graph
such that  $A_s$ includes all the members of a certain nogood. 


%\input{first}

\section{ Computing Stable Models of First-Order Knowledge Bases}
\label{herb}
In this section, we show how we can generalize
algorithm AAS so that it can 
 find all stable models 
of a  knowledge base over  a first-order language
with no function symbols.
The new algorithm will be called {\sc First-Acyclic-All-Stable}
(FAAS).

We will now refer to a knowledge base as a set of rules of the form
\begin{eqnarray}
C \lpimp A_1 , A_2 , ... , A_m, \lpneg B_1,...,\lpneg B_n 
\label{f}
\end{eqnarray}
where all $A$s, $B$s, and $C$ are atoms in a {\em first-order} language
with no function symbols. 
The definitions of  head, body, and positive and negative appearances of
an atom are
the same as in the propositional case. In the expression
$p(X_1,...,X_n)$, $p$ is called a {\em predicate name}.

As in the propositional case,
 every knowledge base $\Pi$ is associated with a directed graph
called the {\em dependency
graph} of $\Pi$,
in which (a) each predicate name in $\Pi$ is a node,
(b) there is a {\em positive arc} directed from a node $p$ to a node $q$ iff there is a rule 
in $\Pi$ in which $p$ is a predicate name in
one of the $A_i$s and $q$ is a predicate name in the head, and 
(c) there is a {\em negative arc} directed from a node $p$ to a node $q$ iff there is a rule 
in $\Pi$ in which $p$ is a predicate name in
one of the $B_i$s and $q$ is a predicate name in the head.  The super
dependency graph, $G_\Pi$, is defined in an analogous manner.
We define
a {\em stratified} knowledge base 
to be a knowledge base in which there are no cycles through the
negative edges in the dependency graph of the knowledge base.



A knowledge base will be called {\em safe} iff each of its rules is safe.
A rule is {\em safe} iff all the variables  appearing in the head
of the rule
or in
predicates  appearing negative in the rule
also appear in positive predicates in the body of the rule. 
In this section, we assume 
that knowledge bases are safe. The {\em Herbrand base} of a knowledge base
is the
set of all atoms constructed using predicate
names and constants from the knowledge base. 
The set of  {\em ground instances of a rule} is the set of rules obtained by
consistently
substituting variables from the rule with constants that appear in 
the knowledge base in all possible ways. The {\em ground instance
of a knowledge base}
is the union of all ground instances of  its rules. Note
that the ground instance of a first-order knowledge base 
can be viewed as a  propositional
knowledge base.
%A Herbrand model of $\Pi$ is a subset of the Herbrandbase
%that satisfies all the instances of the rules in $\Pi$.




A  {\em model}
for a knowledge base is a  subset $M$ of 
the knowledge base's Herbrand base.
This subset has
%\footnote{Roughly
%speaking,
%the Herbrandbase of
%a knowledge base is the set of all
%grounded  atoms that  can be formed out of symbols 
%appearing in the knowledge base.}
the  property
that for every rule in the grounded 
knowledge base, if all the atoms that appear positive in the body of the rule
belong to $M$ and all the atoms that appear negative in the body of
the rule do not belong to $M$, then
  the atom in the head of the rule  belongs to $M$.
A stable model for a first-order knowledge base $\Pi$ is
a Herbrand model of $\Pi$, which 
is also a stable model of the grounded version of $\Pi$. 
%To apply the definition to a knowledge base
%with variables, we first have to replace each rule with its grounded
%instances.
%A knowledge base may have none or several stable models.

We  now present FAAS, an algorithm that computes all stable models of
a first-order knowledge base.
Let $\Pi$ be a first-order knowledge base.  As in the propositional case,
with each node $s$ in $G_\Pi$ (the super dependency graph of $\Pi$),
we associate $\Pi_s$, $A_s$, and $M_s$.
$\Pi_s$  is the subset  
of $\Pi$  containing all the rules about predicates whose names are in $s$.
$A_s$ 
 is the set of all predicate names $P$ 
that appear in the subgraph of $G_\Pi$ rooted by $s$.
$M_s$ are the  stable models associated with
the sub--knowledge base of $\Pi$ that contains only rules about 
predicates whose  names are in $A_s$. 
 Initially, $M_s$ is empty for 
every $s$.
Algorithm  FAAS traverses   $G_\Pi$ from the bottom 
up. When at a node $s$, the algorithm  first combines all the submodels
of the children
 of $s$ into a single set of  models,
$M_{c(s)}$. Then, for each model $m$ in $M_{c(s)}$, it 
calls a procedure that finds all the stable models of $\Pi_s$
union the set of all unit clauses  $P \lpimp$ where $P \in m$.
%does the following:
%first, it converts $\Pi_s$ to a knowledge base
%${\Pi_s}_m$  using the Gelfond-Lifschitz transform.
% Then, it finds all the
%stable models of $\Pi_{s_m}$ and combines them with $m$.
%The set 
%$M_s$ is obtained by repeating this operation for each $m$
%in $M_{c(s)}$. The algorithm {\sc Acyclic-All-Stable} used the procedure
%CartezProd which gets as an input two sets of models and returns their
%cartesian product. The procedure Convert gets a knowledge base $\Pi$ and a model
%$m$ and returns the Gelfond-Lifschitz transform of $\Pi$ w.r.t. $m$.
The procedure {\sc All-Stable} called by FAAS can be 
 any  procedure that computes all the
stable models of a first-order knowledge base. 
Because procedure {\sc All-Stable} computes stable models 
 for only parts of the knowledge base, it may take advantage of
some fractions of the knowledge base being stratified or having any
other property that
simplifies computation of the
stable models of a fraction. 


\begin{figure}
\fbox{
\parbox{6.0in}{ 
{\sc First-Acyclic-All-Stable}$(\Pi)$
\\
Input: A first-order knowledge base $\Pi$. \\
Output: All the stable models of $\Pi$.
\begin{enumerate}

\item Traverse $G_\Pi$ from the bottom up. For each node $s$, do:
\begin{enumerate}
\item $M_s := \emptyset$;
\item Let $s_1,...,s_j$ be the children of $s$;
\item $M_{{c(s)}} :=$ CartesProd$(\{M_{s_1},...,M_{s_j}\})$; 
\item For each $m \in M_{{c(s)}}$ do
\item[] $M_s := M_s \union$all-stable$(\Pi_s \union \{ P \lpimp \st P \in m \})$
\end{enumerate}
\item Output CartesProd($\{M_{s_1},...,M_{s_k}\}$), where $s_1,...,s_k$
are the sinks of $G_\Pi$.
\end{enumerate}
 }}
 \caption{Algorithm {\sc First-Acyclic-All-Stable} (FAAS)}
 \label{ftree}
\end{figure}

\begin{theorem}

Algorithm FAAS is correct, that  is, $m$ is a stable model
of a knowledge base $\Pi$ iff 
$m$ is one of the models in the  output when applying FAAS to $\Pi$.
\end{theorem}
\begin{proof}
  As the proof of Theorem \ref{acyc}. \end{proof}

Note that
the more that a knowledge base 
appears stratified, the more efficient algorithm
FAAS  becomes.

\begin{ex}
{\rm
Consider  knowledge base $\Pi_5$:
\begin{eqnarray*}
warm\_blooded(X) & \lpimp & mammal(X) \\
live\_on\_land(X) & \lpimp & mammal(X), \lpneg ab1(X) \\
female(X) &\lpimp & mammal(X), \lpneg male(X) \\
male(X) &\lpimp& mammal(X), \lpneg female(X) \\
mammal(X) & \lpimp & dolphin(X) \\
ab1(X) & \lpimp &  dolphin(X) \\
mammal(X) & \lpimp & lion(X) \\
dolphin(flipper)&\lpimp& \\ \\
live\_on\_land(X) &\lpimp& bird(X) \\
fly(X) &\lpimp& bird(X), \lpneg ab2(X) \\
bird(X) &\lpimp& penguin(X) \\
ab2(X) &\lpimp& penguin(X)\\ 
bird(bigbird) & \lpimp &
\end{eqnarray*}

The super dependency graph of $\Pi_5$, $G_{\Pi_5}$, is the same as the super
dependency graph of the knowledge base $\Pi_2$ (see Figure 
\ref{fig:bigsuper}). Observe that when at node {\em mammal}, for example,
in step 1.d 
the algorithm  looks for all stable models of the knowledge base $\tag{\Pi} =
\Pi_{mammal}$ $ \union$ $\{\lpimp dolphin(flipper)\}$, where
$\Pi_{mammal}=$$\{ mammal(X) \lpimp dolphin(X), mammal(X) \lpimp lion(X) \}$.
$\tag{\Pi}$ is a stratified knowledge base that has a unique stable model that
can be found efficiently. Hence, algorithm FAAS  saves us from
having to ground all the rules of the knowledge base before starting 
to calculate
the models, and it can take advantage of parts of the knowledge base being
stratified. 
}
\end{ex}


%\input{rel}


\section{Related Work}
\label{related}
In recent years, quite a few algorithms have been developed for reasoning
with stable models. Nonetheless,
as far as we know, the work presented here is original
in the sense
that it provides a partition of the set of
all the  knowledge bases into a hierarchy
of tractable
classes. The partition
is based on the structure of the dependency graph. Intuitively,
the task of  computing all the stable models of a knowledge base  using
algorithm AAS becomes
increasingly complex as the ``distance'' of the knowledge base from 
being stratified becomes larger. 
Next, we summarize the work that
seems to us most relevant.


Algorithm AAS is based on an idea that appears 
in the work of Lifschitz and Turner (1994), where they 
show that in many cases a logic program can be divided
into two parts, such that one part, the 
``bottom'' part, does not refer to the predicates defined in the 
``top'' part. They then explain how the task of
computing the stable models of a program  can be simplified when the program 
is split into parts.
Algorithm AAS,
using the superstructure of
the dependency graph,
exploits a specific method for
splitting the program.

Bell \etal (1994) and Subrahmanian \etal (1995) 
implement linear and integer programming techniques in order to compute 
stable models   (among other nonmonotonic logics).
However, 
it is difficult to assess the 
merits of their  approaches
in terms of  complexity. 
Ben-Eliyahu and Dechter (1991)  
illustrate how a knowledge base $\Pi$
can be translated  into a propositional theory $T_\Pi$ such that each
model of the latter corresponds to a stable model of the former.
It follows from this that
the problem  of finding all the stable models of 
a knowledge base corresponds to
the problem of finding all the models of a propositional theory.
Satoh and Iwayama (1991)
 provide a nondeterministic procedure
for computing the
stable models of logic programs with integrity constraints.
Junker and Konolige (1990) present an algorithm for computing
TMS' labels. Antoniou and Langetepe (1994) 
introduce a method for representing
some classes of default theories as normal logic programs in such a way that
SLDNF-resolution can be used to compute extensions. 
Pimentel and Cuadrado (1989)
 develop a label-propagation algorithm that uses  data
structures called {\em compressible semantic trees} in order to implement 
a TMS;
their algorithm is based on stable model semantics. The algorithms developed
by Marek and Truszczy\'{n}ski (1993) for autoepistemic logic
can also be adopted for computing stable models.
The procedures by Marek and Truszczy\'{n}ski (1993), Antoniou and
Langetepe (1994), 
Pimentel and Cuadrado (1989), Ben-Eliyahu and Dechter (1991),
Satoh and Iwayama (1991),
Bell \etal (1994),  Subrahmanian \etal (1995), and 
Junker and Konolige (1990) 
do not take advantage of the structure
of the knowledge base as reflected in its dependency graph,
and therefore are not  efficient for
stratified knowledge bases.

Sacc{\`{a}} and Zaniolo (1990) 
present a {\em backtracking fixpoint} algorithm for
constructing {\em one} stable model of a first-order knowledge base.
This algorithm is similar to algorithm {\sc All-Stable2} presented here
in Section \ref{twoa} but
its complexity is worse than the complexity of {\sc All-Stable2}.  
They show how the backtracking fixpoint
algorithm can be modified to handle stratified
knowledge bases in an efficient manner, 
 but the algorithm
needs further adjustments before it can deal efficiently
with knowledge bases that
are very close to being stratified. 
Leone \etal (1993) present an improved backtracking fixpoint 
algorithm for computing one stable model of a Datalog$^\neg$ program
and discuss how the improved algorithm can be implemented.
One of the procedures called by the improved
algorithm   is based
on the backtracking fixpoint algorithm of
Sacc{\`{a}} and Zaniolo (1990). 
  Like the
backtracking fixpoint algorithm, the improved algorithm as is
does not take advantage of the structure
of the program, \ie, it is not efficient for programs
that are close to being stratified. 

Several tractable subclasses
for computing extensions of default theories (and, hence,
computing stable models) are known 
\cite{ks:sdl,PaSi94,PaZa94,DiMa94,BeDe96}.
Some of these tractable subclasses  are characterized 
 using a graph
that reflects dependencies in the program between atoms and rules.
 The algorithms presented in these papers
are  complete only for a subclass
of all  knowledge bases, however.  Algorithms for computing extensions of
{\em stratified} default theories or  extensions of default theories that 
have no odd cycles (in some precise sense) are given by
Papadimitriou and Sideri (1994) and Cholewi\'{n}ski (1995a, 1995b). 


Algorithms for handling a TMS with nogoods have been developed in
the AI community by Doyle (1979) and Charniak \etal (1980).
But, as Elkan (1990) points out, these algorithms
are not always faithful to the semantics of the TMS and their complexities
have not been analyzed. Dechter and Dechter (1994) provide  algorithms
for manipulating a TMS when it is
represented as a constraint network. The efficiency
of their algorithms depends on the structure of the constraint network
 representing the TMS, and  the structure  they employ differs
from 
the dependency graph of the knowledge base.

%\input{concl}

\section{Conclusion}
The task of computing stable models is at the heart of several 
systems central to AI, including
TMSs,  autoepistemic logic, and default logic.
This task has been shown to be NP-hard. In this paper,  
we present a partition of the set of all knowledge bases to
 classes 
$\Omega_1,\Omega_2,...$, 
such that if a knowledge base  $\Pi$ is in $\Omega_k$, then $\Pi$ has at most
$k$ stable models, and they may all 
 be found in time $O(lnk)$, where $l$ is the length of the knowledge base 
and $n$ the number of atoms in $\Pi$. 
Moreover, for an arbitrary knowledge base $\Pi$,
we can find the minimum $k$ such that $\Pi$ belongs to $\Omega_k$ in time
linear in the size of $\Pi$.  Intuitively, the more the knowledge base
is stratified, the more efficient our algorithm becomes.
We believe that beyond stratified knowledge bases,
the more expressive the knowledge base is ($\ie$ the more
rules with nonstratified negation in the knowledge base), the less likely it 
 will be needed. Hence, our analysis should be quite useful. In addition, 
we show that  algorithm AAS has several advantages in a dynamically
changing knowledge base, and we provide 
applications for answering queries
and implementing a TMS's nogood strategies. We also illustrate
a generalization of
algorithm AAS for the class of first-order knowledge bases.

Algorithm AAS  can  easily be adjusted to find only
one stable model of a knowledge base. While traversing the super dependency 
graph, we generate only one  model at each node. If we arrive at 
 a node where we cannot generate a  model based on
what we have computed so far, we backtrack to the most recent node
where  several  models were available
to choose from and take the
next  model that was not yet chosen. The worst-case time complexity
of this algorithm is equal to the worst-case time complexity of
the algorithm for finding all stable models because we may have to
exhaust all possible ways of generating a stable model before
finding out that a certain knowledge base does not have a stable model
at all.  Nevertheless, we believe that in the average case,
finding  just one model
will be easier 
than
finding them all. 
A similar modification of the AAS algorithm is required if we are
interested in finding one model in which one particular atom
gets the value $\true$.


This work is another attempt to bridge the gap between the declarative 
systems (e.g., default logic, autoepistemic logic) and the
procedural systems
(e.g., ATMs, Prolog) 
of the nonmonotonic  reasoning community.
It is argued that
while the declarative methods are sound,
they are impractical since they are computationally expensive,
and while the procedural  methods are more efficient, it is difficult to
completely understand their performance or to evaluate their correctness.
%The work presented
%here is  another step towards a successful combillustrates that the declarative   and the procedural  approaches can be
%combined to yield an efficient yet formally supported nonmonotonic
%system.
The work presented
here illustrates that the declarative   and the procedural  approaches can be
combined to yield an efficient yet formally supported nonmonotonic
system.

\vspace{-0.3cm}
\subsection*{Acknowledgments}
Thanks to Luigi Palopoli for useful comments on earlier draft of this
paper and to
 Michelle Bonnice and
 Gadi Dechter for editing on parts of the manuscript.
 Many thanks to the
anonymous referees for 
very useful comments.
 
Some of this work was done while the author
was visiting the Cognitive Systems Laboratory,
Computer Science Department,
  University of California, Los Angeles, California, USA. 
This work 
was partially supported
by NSF grant  
IRI-9420306 and by Air Force Office of Scientific Research 
grant \#F49620-94-1-0173.

%bla bla \cite{AnLa94,bnns:linear,CRM80,Cho95a,
%Cho95b,kn:dynamic,Gel87,gl:negation,konolige90,LRRS93,
%LiTu94,MaTr93,moore,PiCu89,r:ldr,SaZa90,SaIw91,snv:linear}


\begin{thebibliography}{}

\bibitem[\protect\BCAY{Antoniou \BBA\ Langetepe}{Antoniou \BBA\
  Langetepe}{1994}]{AnLa94}
Antoniou, G.\BBACOMMA\  \BBA\ Langetepe, E. \BBOP1994\BBCP.
\newblock \BBOQ Soundness and completeness of a logic programming approach to
  default logic\BBCQ\
\newblock In {\Bem AAAI-94: Proceedings of the 12th national conference on
  artificial intelligence}, \BPGS\ 934--939. AAAI Press, Menlo Park, Calif.

\bibitem[\protect\BCAY{Apt, Blair, \BBA\ Walker}{Apt
  et~al.}{1988}]{abw:knowledge}
Apt, K., Blair, H., \BBA\ Walker, A. \BBOP1988\BBCP.
\newblock \BBOQ Towards a theory of declarative knowledge\BBCQ\
\newblock In Minker, J.\BED, {\Bem Foundations of deductive databases and logic
  programs}, \BPGS\ 89--148. Morgan Kaufmann.

\bibitem[\protect\BCAY{Bell, Nerode, Ng, \BBA\ Subrahmanian}{Bell
  et~al.}{1994}]{bnns:linear}
Bell, C., Nerode, A., Ng, R., \BBA\ Subrahmanian, V. \BBOP1994\BBCP.
\newblock \BBOQ Mixed integer programming methods for computing non-monotonic
  deductive databases\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 41\/}(6), 1178--1215.

\bibitem[\protect\BCAY{Ben-Eliyahu \BBA\ Dechter}{Ben-Eliyahu \BBA\
  Dechter}{1994}]{bd:ilps91}
Ben-Eliyahu, R.\BBACOMMA\  \BBA\ Dechter, R. \BBOP1994\BBCP.
\newblock \BBOQ Propositional semantics for disjunctive logic programs\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem 12},
  53--87.
\newblock A short version appears in JICSLP-92: Proceedings of the 1992 joint
  international conference and symposium on logic programming.

\bibitem[\protect\BCAY{Ben-Eliyahu \BBA\ Dechter}{Ben-Eliyahu \BBA\
  Dechter}{1996}]{BeDe96}
Ben-Eliyahu, R.\BBACOMMA\  \BBA\ Dechter, R. \BBOP1996\BBCP.
\newblock \BBOQ Default reasoning using classical logic\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 84\/}(1-2), 113--150.

\bibitem[\protect\BCAY{Bidoit \BBA\ Froidevaux}{Bidoit \BBA\
  Froidevaux}{1987}]{bidoit}
Bidoit, N.\BBACOMMA\  \BBA\ Froidevaux, C. \BBOP1987\BBCP.
\newblock \BBOQ Minimalism subsumes default logic and circumscription in
  stratified logic programming\BBCQ\
\newblock In {\Bem LICS-87: Proceedings of the IEEE symposium on logic in
  computer science}, \BPGS\ 89--97. IEEE Computer Science Press, Los Alamitos,
  Calif.

\bibitem[\protect\BCAY{Charniak, Riesbeck, \BBA\ McDermott}{Charniak
  et~al.}{1980}]{CRM80}
Charniak, E., Riesbeck, C.~K., \BBA\ McDermott, D.~V. \BBOP1980\BBCP.
\newblock {\Bem Artificial Intelligence Programming}, \BCH~16.
\newblock Lawrence Erlbaum, Hillsdale, NJ.

\bibitem[\protect\BCAY{Cholewi{\'{n}}ski}{Cholewi{\'{n}}ski}{1995a}]{Cho95b}
Cholewi{\'{n}}ski, P. \BBOP1995a\BBCP.
\newblock \BBOQ Reasoning with stratified default theories\BBCQ\
\newblock In Marek, W.~V., Nerode, A., \BBA\ Truszczy{\'{n}}ski, M.\BEDS, {\Bem
  Logic programming and nonmonotonic reasoning: proceedings of the 3rd
  international conference}, \BPGS\ 273--286.
\newblock Lecture notes in computer science, 928. Springer-Verlag, Berlin.

\bibitem[\protect\BCAY{Cholewi{\'{n}}ski}{Cholewi{\'{n}}ski}{1995b}]{Cho95a}
Cholewi{\'{n}}ski, P. \BBOP1995b\BBCP.
\newblock \BBOQ Stratified default theories\BBCQ\
\newblock In Pacholski, L.\BBACOMMA\  \BBA\ Tiuryn, A.\BEDS, {\Bem Computer
  science logic: 8th workshop, CSL'94: Selected papers}, \BPGS\ 456--470.
\newblock Lecture notes in computer science, 933. Springer-Verlag, Berlin.

\bibitem[\protect\BCAY{Dechter \BBA\ Dechter}{Dechter \BBA\
  Dechter}{1996}]{kn:dynamic}
Dechter, R.\BBACOMMA\  \BBA\ Dechter, A. \BBOP1996\BBCP.
\newblock \BBOQ Structure-driven algorithms for truth maintenance\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 82\/}(1-2), 1--20.

\bibitem[\protect\BCAY{Dimopoulos \BBA\ Magirou}{Dimopoulos \BBA\
  Magirou}{1994}]{DiMa94}
Dimopoulos, Y.\BBACOMMA\  \BBA\ Magirou, V. \BBOP1994\BBCP.
\newblock \BBOQ A graph-theoretic approach to default logic\BBCQ\
\newblock {\Bem Journal of Information and Computation}, {\Bem 112}, 239--256.

\bibitem[\protect\BCAY{Doyle}{Doyle}{1979}]{Doy79}
Doyle, J. \BBOP1979\BBCP.
\newblock \BBOQ A truth-maintenance system\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 12}, 231--272.

\bibitem[\protect\BCAY{Dung}{Dung}{1991}]{Dun91}
Dung, P.~M. \BBOP1991\BBCP.
\newblock \BBOQ Negation as hypothesis: An abductive foundation for logic
  programming\BBCQ\
\newblock In Furukawa, K.\BED, {\Bem ICLP-91: Proceedings of the 8th
  international conference on logic programming}, \BPGS\ 3--17. MIT Press.

\bibitem[\protect\BCAY{Elkan}{Elkan}{1990}]{elkan}
Elkan, C. \BBOP1990\BBCP.
\newblock \BBOQ A rational reconstruction of nonmonotonic truth maintenance
  systems\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 43}, 219--234.

\bibitem[\protect\BCAY{Eshghi \BBA\ Kowalski}{Eshghi \BBA\
  Kowalski}{1989}]{EsKo89}
Eshghi, K.\BBACOMMA\  \BBA\ Kowalski, R.~A. \BBOP1989\BBCP.
\newblock \BBOQ Abduction compared with negation by failure\BBCQ\
\newblock In Levi, G.\BBACOMMA\  \BBA\ Martelli, M.\BEDS, {\Bem ICLP-89:
  Proceedings of the 6th international conference on logic programming}, \BPGS\
  234--254. MIT Press.

\bibitem[\protect\BCAY{Fine}{Fine}{1989}]{fine}
Fine, K. \BBOP1989\BBCP.
\newblock \BBOQ The justification of negation as failure\BBCQ\
\newblock {\Bem Logic, Methodology and Philosophy of Science}, {\Bem 8},
  263--301.

\bibitem[\protect\BCAY{Gelfond}{Gelfond}{1987}]{Gel87}
Gelfond, M. \BBOP1987\BBCP.
\newblock \BBOQ On stratified autoepistemic theories\BBCQ\
\newblock In {\Bem AAAI-87: Proceedings of the 5th national conference on
  artificial intelligence}, \BPGS\ 207--211. Morgan Kaufmann.

\bibitem[\protect\BCAY{Gelfond \BBA\ Lifschitz}{Gelfond \BBA\
  Lifschitz}{1988}]{gl:stable}
Gelfond, M.\BBACOMMA\  \BBA\ Lifschitz, V. \BBOP1988\BBCP.
\newblock \BBOQ The stable model semantics for logic programming\BBCQ\
\newblock In Kowalski, R.~A.\BBACOMMA\  \BBA\ Bowen, K.~A.\BEDS, {\Bem Logic
  Programming: Proceedings of the 5th international conference}, \BPGS\
  1070--1080. MIT Press.

\bibitem[\protect\BCAY{Gelfond \BBA\ Lifschitz}{Gelfond \BBA\
  Lifschitz}{1991}]{gl:negation}
Gelfond, M.\BBACOMMA\  \BBA\ Lifschitz, V. \BBOP1991\BBCP.
\newblock \BBOQ Classical negation in logic programs and disjunctive
  databases\BBCQ\
\newblock {\Bem New Generation Computing}, {\Bem 9}, 365--385.

\bibitem[\protect\BCAY{Junker \BBA\ Konolige}{Junker \BBA\
  Konolige}{1990}]{konolige90}
Junker, U.\BBACOMMA\  \BBA\ Konolige, K. \BBOP1990\BBCP.
\newblock \BBOQ Computing the extensions of autoepistemic and default logics
  with a {TMS}\BBCQ\
\newblock In {\Bem AAAI-90: Proceedings of the 8th national conference on
  artificial intelligence}, \BPGS\ 278--283. AAAI Press.

\bibitem[\protect\BCAY{Kakas \BBA\ Mancarella}{Kakas \BBA\
  Mancarella}{1991}]{KaMa91}
Kakas, A.~C.\BBACOMMA\  \BBA\ Mancarella, P. \BBOP1991\BBCP.
\newblock \BBOQ Stable theories for logic programs\BBCQ\
\newblock In Saraswat, V.\BBACOMMA\  \BBA\ Udea, K.\BEDS, {\Bem ISLP-91:
  Proceedings of the 1991 international symposium on logic programming}, \BPGS\
  85--100. MIT Press.

\bibitem[\protect\BCAY{Kautz \BBA\ Selman}{Kautz \BBA\ Selman}{1991}]{ks:sdl}
Kautz, H.~A.\BBACOMMA\  \BBA\ Selman, B. \BBOP1991\BBCP.
\newblock \BBOQ Hard problems for simple default logics\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 49}, 243--279.

\bibitem[\protect\BCAY{Leone, Romeo, Rullo, \BBA\ Sacc{\`{a}}}{Leone
  et~al.}{1993}]{LRRS93}
Leone, N., Romeo, N., Rullo, M., \BBA\ Sacc{\`{a}}, D. \BBOP1993\BBCP.
\newblock \BBOQ Effective implementation of negation in database logic query
  languages\BBCQ\
\newblock In Atzeni, P.\BED, {\Bem LOGIDATA{$^+$}: Deductive database with
  complex objects}, \BPGS\ 159--175.
\newblock Lecture notes in computer science, 701. Springer-Verlag, Berlin.

\bibitem[\protect\BCAY{Lifschitz \BBA\ Turner}{Lifschitz \BBA\
  Turner}{1994}]{LiTu94}
Lifschitz, V.\BBACOMMA\  \BBA\ Turner, H. \BBOP1994\BBCP.
\newblock \BBOQ Splitting a logic program\BBCQ\
\newblock In {Van Hentenryck}, P.\BED, {\Bem ICLP-94: Proceedings of the 11th
  international conference on logic programming}, \BPGS\ 23--37. MIT Press.

\bibitem[\protect\BCAY{Marek \BBA\ Truszczy{\'{n}}ski}{Marek \BBA\
  Truszczy{\'{n}}ski}{1993}]{MaTr93}
Marek, V.~W.\BBACOMMA\  \BBA\ Truszczy{\'{n}}ski, M. \BBOP1993\BBCP.
\newblock {\Bem Nonmonotonic logic: Context-dependent reasoning}.
\newblock Springer Verlag, Berlin.

\bibitem[\protect\BCAY{Marek \BBA\ Truszczy{\'{n}}ski}{Marek \BBA\
  Truszczy{\'{n}}ski}{1991}]{mt:auto}
Marek, W.\BBACOMMA\  \BBA\ Truszczy{\'{n}}ski, M. \BBOP1991\BBCP.
\newblock \BBOQ Autoepistemic logic\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 38}, 588--619.

\bibitem[\protect\BCAY{Moore}{Moore}{1985}]{moore}
Moore, R.~C. \BBOP1985\BBCP.
\newblock \BBOQ Semantical consideration on nonmonotonic logic\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 25}, 75--94.

\bibitem[\protect\BCAY{Palopoli \BBA\ Zaniolo}{Palopoli \BBA\
  Zaniolo}{1996}]{PaZa94}
Palopoli, L.\BBACOMMA\  \BBA\ Zaniolo, C. \BBOP1996\BBCP.
\newblock \BBOQ Polynomial-time computable stable models\BBCQ.
\newblock {\em Annals of Mathematics and Artificial Intelligence}, in press.

\bibitem[\protect\BCAY{Papadimitriou \BBA\ Sideri}{Papadimitriou \BBA\
  Sideri}{1994}]{PaSi94}
Papadimitriou, C.~H.\BBACOMMA\  \BBA\ Sideri, M. \BBOP1994\BBCP.
\newblock \BBOQ Default theories that always have extensions\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 69}, 347--357.

\bibitem[\protect\BCAY{Pimentel \BBA\ Cuadrado}{Pimentel \BBA\
  Cuadrado}{1989}]{PiCu89}
Pimentel, S.~G.\BBACOMMA\  \BBA\ Cuadrado, J.~L. \BBOP1989\BBCP.
\newblock \BBOQ A truth maintenance system based on stable models\BBCQ\
\newblock In Lusk, E.~L.\BBACOMMA\  \BBA\ Overbeek, R.~A.\BEDS, {\Bem ICLP-89:
  Proceedings of the 1989 North American conference on logic programming},
  \BPGS\ 274--290. MIT Press.

\bibitem[\protect\BCAY{Przymusinska \BBA\ Przymusinski}{Przymusinska \BBA\
  Przymusinski}{1990}]{pp}
Przymusinska, H.\BBACOMMA\  \BBA\ Przymusinski, T. \BBOP1990\BBCP.
\newblock \BBOQ Semantic issues in deductive databases and logic programs\BBCQ\
\newblock In Banerji, R.~B.\BED, {\Bem Formal techniques in artificial
  intelligence: A sourcebook}, \BPGS\ 321--367. North-Holland, New York.

\bibitem[\protect\BCAY{Reiter}{Reiter}{1980}]{r:ldr}
Reiter, R. \BBOP1980\BBCP.
\newblock \BBOQ A logic for default reasoning\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 13}, 81--132.

\bibitem[\protect\BCAY{Sacc{\`{a}} \BBA\ Zaniolo}{Sacc{\`{a}} \BBA\
  Zaniolo}{1990}]{SaZa90}
Sacc{\`{a}}, D.\BBACOMMA\  \BBA\ Zaniolo, C. \BBOP1990\BBCP.
\newblock \BBOQ Stable models and non-determinism in logic programs with
  negation\BBCQ\
\newblock In {\Bem PODS-90: Proceedings of the 9th {ACM SIGACT-SIGMOD-SIGART}
  symposium on principles of database systems}, \BPGS\ 205--217. ACM Press.

\bibitem[\protect\BCAY{Satoh \BBA\ Iwayama}{Satoh \BBA\ Iwayama}{1991}]{SaIw91}
Satoh, K.\BBACOMMA\  \BBA\ Iwayama, N. \BBOP1991\BBCP.
\newblock \BBOQ Computing abduction by using the {TMS}\BBCQ\
\newblock In Furukawa, K.\BED, {\Bem ICLP-91: Proceedings of the 8th
  international conference on logic programming}, \BPGS\ 505--518. MIT Press.

\bibitem[\protect\BCAY{Subrahmanian, Nau, \BBA\ Vago}{Subrahmanian
  et~al.}{1995}]{snv:linear}
Subrahmanian, V., Nau, D., \BBA\ Vago, C. \BBOP1995\BBCP.
\newblock \BBOQ {WFS} + branch and bound = stable models\BBCQ\
\newblock {\Bem IEEE Transactions on Knowledge and Data Engineering}, {\Bem
  7\/}(3), 362--377.

\bibitem[\protect\BCAY{Tarjan}{Tarjan}{1972}]{tarjan}
Tarjan, R. \BBOP1972\BBCP.
\newblock \BBOQ Depth-first search and linear graph algorithms\BBCQ\
\newblock {\Bem SIAM Journal on Computing}, {\Bem 1}, 146--160.

\end{thebibliography}
%\bibliography{sat,const,reiter,dis,complex,nonmon,rachel,stable}
\end{document}





