
\documentstyle[jair,twoside,theapa,11pt]{article}
\input{epsfig}

\input{definitions}

\jairheading{9}{1998}{37-97}{2/98}{9/98}
\ShortHeadings{The Divide-and-Conquer Subgoal-Ordering Algorithm}
{Ledeniov \& Markovitch}
\firstpageno{37}


\begin{document}

\title{The Divide-and-Conquer Subgoal-Ordering Algorithm \\ 
       for Speeding up Logic Inference}
\author{\name Oleg Ledeniov \email {olleg@cs.technion.ac.il} \\
        \name Shaul Markovitch \email {shaulm@cs.technion.ac.il} \\
\addr{Computer Science Department} \\
\addr{Technion -- Israel Institute of Technology}\\
\addr{ Haifa 32000, Israel}\\
} 


\maketitle


\begin{abstract}

It is common to view programs as a combination of logic and control:
the logic part defines {\em what} the program must do, 
the control part -- {\em how} to do it.
The Logic Programming paradigm was developed
with the intention of separating the logic from the control.
Recently, extensive research has been conducted on automatic
generation of control for logic programs.
Only a few of these works considered the issue of automatic
generation of control for improving the efficiency of logic programs.
In this paper we present a novel algorithm for automatic finding of 
lowest-cost subgoal orderings.
The algorithm works using the divide-and-conquer strategy.  
The given set of subgoals is partitioned into smaller sets, 
based on co-occurrence of free variables.
The subsets are ordered recursively and merged, yielding a provably optimal order.
We experimentally demonstrate the utility of the algorithm 
by testing it in several domains, and discuss the possibilities of its
cooperation with other existing methods.
\end{abstract}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%                      I N T R O D U C T I O N                   %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Introduction}



It is common to view programs as a combination of logic and control
\cite{kowalski:79}.
The logic part defines {\em what} the program must do,
the control part -- {\em how} to do it.  Traditional programming
languages require that the programmers supply both components.
The Logic Programming paradigm was developed
with the intention of separating the logic from the control \cite{lloyd:87}.
The goal of the paradigm is that the programmer specifies the
logic without bothering about the control, which should be 
supplied by the interpreter.

Initially, most practical logic programming languages, such as Prolog 
\cite{clocksin:87,sterling:94}, 
did not include the means for automatic generation of control.
As a result, a Prolog programmer had to implicitly define the control
by the order of clauses and of subgoals within the clauses.
Recently, extensive research has been conducted on automatic
generation of control for logic programs.
A major part of this research is concerned with control that
affects correctness and termination of logic programs
\cite{DeSchreye:94,somogyi:96:algorithm,cortesi:97}.
Only a few of these works consider the issue of automatic
generation of control for improving the {\em efficiency} of logic programs.
Finding a good ordering that leads to efficient execution 
requires a deep understanding of the logic inference mechanism.
Hence, in many cases, only expert programmers are able to generate efficient
programs.  The problem intensifies with the recent development of
the field of inductive logic programming \cite{muggleton94:jlp}.  There, logic
programs are automatically induced by learning.  Such learning algorithms
are commonly built with the aim of speeding up the induction process 
without considering the efficiency of resulting programs.

The goal of the research described in this paper is to design algorithms
that automatically find efficient orderings of subgoal sequences.
Several researchers have explored the problem of automatic reordering of 
subgoals in logic programs 
\cite{warren:81,naish:85,smith:85,natarajan:87,markovitch:89:ordering}.  
The general subgoal ordering problem is known to be NP-hard 
\cite{ullman:82,ullman:88}.  
\citeA{smith:85} and \citeA{markovitch:89:ordering} 
present search algorithms for finding optimal orderings.
These algorithms are general and  carry  exponential 
costs for non-trivial sets of subgoals.  
\citeA{natarajan:87} describes
an efficient algorithm for the special case where subgoals in the
set do not share free variables.

In this paper we present a novel algorithm for subgoal ordering.
We call two subgoals that share a free variable {\em dependent}.
Unlike Natarajan's approach, which can only
handle subgoal sets that are completely independent, our algorithm
can deal with any subgoal set, while making maximal use of the
existing dependencies for acceleration of the ordering process.  
In the worst case the algorithm -- like that of Smith and Genesereth --
is exponential.
Still, in most practical cases, our algorithm exploits
subgoal dependencies and finds optimal orderings in polynomial time.

We start with an analysis of the ordering problem and demonstrate
its importance through examples.
We then show how to compute the cost
of a given ordering based on the cost and the number of solutions of 
the individual subgoals.  We describe the algorithm of Natarajan
and the algorithm of Smith and Genesereth and show how the
two can be combined into an algorithm that is more efficient
and general than each of the two.  We show drawbacks of the
combined algorithm and introduce the new algorithm, which
avoids these drawbacks.  We call it the {\em Divide-and-Conquer
algorithm (\ALG)}.
We prove the correctness of the algorithm, discuss its complexity
and compare it to the combined algorithm.
The \ALG\ assumes knowledge of the cost and the number of solutions
of the subgoals.  
This knowledge can be obtained by machine learning 
techniques such as those employed by \citeA{markovitch:89:ordering}.
Finally, we  test the utility of our algorithm by running
a set of experiments on artificial and real domains.

The \ALG\ for subgoal ordering can be combined with many existing 
methods in logic programming, such as program transformation,
compilation, termination control, correctness verification, and others. 
We discuss the possibilities of such combinations in the concluding section.

Section \ref{sec:background} states the ordering problem.
Section \ref{sec:algorithms-old} describes existing ordering algorithms
and their combination.  
Section \ref{sec:algorithm-new} presents the new algorithm.
Section \ref{sec:learning} discusses the acquisition of the control knowledge.
Section \ref{sec:experimentation} contains experimental results.  
Section \ref{sec:discussion} contains a
discussion of practical issues, comparison with other works and conclusions.






%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%                      B A C K G R O U N D                       %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Background: Automatic Ordering of Subgoals}
\label{sec:background}

We start by describing the conventions and assumptions accepted in this paper.
Then we demonstrate the importance of subgoal ordering and discuss its validity.  
Finally, we present a classification of ordering methods and discuss
related work. 


%;;;;;;;;;;;;;;;;;;;;;;;;;;   CONVENTIONS   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


\subsection{Conventions and Assumptions}

All constant, function and predicate symbols 
in programs begin with 
lower case letters, while capital letters are reserved for variables.
Braces are used to denote unordered sets (e.g., $\{a,b,c\}$),
and angle brackets are used for ordered sequences (e.g., $\langle a,b,c \rangle$).
Parallel lines ($\cc$) denote concatenations of ordered
sequences of subgoals.
When speaking about abstract subgoals (and not named predicates of 
concrete programs), we denote separate subgoals by capital letters
$(A, B\ldots)$, ordered sequences of subgoals by capitalized vectors
$(\Bv,\Ov_S\ldots)$, and sets of subgoals by calligraphic capitals
$(\B,\S\ldots)$.
$\pi(\S)$ denotes the set of all permutations of $\S$.

We assume that the programs we work with are written
in {\em pure Prolog}, i.e., without cut operators, 
meta-logical or extra-logical predicates.
Alternatively, we can assume that only pure Prolog sub-sequences of subgoals
are subject to ordering.  For example, given a rule of the form
\[
A \leftarrow B_1, B_2, B_3, !, B_4, B_5, B_6.
\]
only its final part $\{B_4, B_5, B_6\}$ can be ordered (without
affecting the solution set).

In this work we focus upon the task of finding {\em all} the solutions to a 
set of subgoals.





%;;;;;;;;;;;;;;;;;;;;;;;;;;   O R D E R I N G   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



\subsection{Ordering of Subgoals in Logic Programs}

A logic program is a set of clauses:
\[
 A \leftarrow B_1, B_2, \ldots, B_n. \hspace{1cm} (n \geq 0) 
\]
where $A,B_1,\ldots,B_n$ are literals (predicates with arguments).
To use such a clause for proving a goal that matches $A$,
 we must prove that {\em all} $B$-s
hold simultaneously, under consistent bindings of the free variables.
A {\em solution} is  such a set of variable bindings.
The {\em solution set} of a goal is the bag of all its solutions
created by its program.

A {\em computation rule} defines which subgoal will be proved next.
In Prolog, the computation rule always selects the leftmost subgoal in a goal.
If a subgoal fails, {\em backtracking} is performed --
the proof of the previous subgoal is re-entered to generate another solution.
For a detailed definition of the logic inference process, see \citeA{lloyd:87}.

\begin{theorem}
\label{theorem:lloyd1}
The solution set of a set of subgoals does not depend on the order of 
their execution.
\end{theorem}
\begin{proof}
When we are looking for all solutions,
the solution set does not depend on the computation rule chosen
\cite<Theorems 9.2 and 10.3 in>{lloyd:87}.
Since a transposition of subgoals in an ordered sequence can be
regarded as a change of the computation rule (the subgoals are
selected in different order), such transposition does not change the
solution set. 
\hfill $\Box$
\end{proof}
\ \\ \medskip

This theorem implies that we may reorder subgoals  during the proof
derivation. 
Yet the {\em efficiency} of the derivation
strongly depends on the chosen order of subgoals.
The following example illustrates how two different orders
can lead to a large difference in execution efficiency.

\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{4.8in}
\begin{center}

\medskip
\noindent
\begin{minipage}[t]{2.2in}
{\tt  parent(abraham,isaac).}\\
{\tt  parent(sarah,isaac).  }\\
{\tt  parent(abraham,ishmael).} \\
{\tt  parent(isaac,esav).  }\\
{\tt  parent(isaac,jakov). }\\
{\small ... More parent clauses ...}
\end{minipage}
\begin{minipage}[t]{1.5in}
{\tt male(abraham).}\\
{\tt male(isaac).}\\
{\tt male(ishmael).}\\
{\tt male(jakov).}\\
{\tt male(esav).}\\
{\small ... More male clauses ...}
\end{minipage}
\end{center}

\begin{center}
\begin{minipage}{4.5in}
\noindent
{\tt brother(X,Y)} $\leftarrow$  {\tt male(X), parent(W,X), parent(W,Y), X=/=Y.} \\
{\tt father(X,Y)}  $\leftarrow$  {\tt male(X), parent(X,Y).} \\
{\tt uncle(X,Y)}   $\leftarrow$  {\tt parent(Z,Y), brother(X,Z).} \\
{\small ... More rules of relations ...}
\end{minipage}
\end{center}

\medskip
\end{minipage}

} % fbox
\caption{\label{fig:family-database}
{\small 
A small fragment of a Biblical database describing family relationships.
}}
\end{center}
\end{figure}



\begin{example} \ 
\label{ex:family-uncle}
\end{example}
Consider a Biblical family database such as the one listed in
Figure~\ref{fig:family-database} \cite<a similar database appears in the book by>{sterling:94}.
The body of the rule defining the  uncle-nephew  (or uncle-niece) relation
can be ordered in two ways:
\begin{enumerate}
\item {\tt uncle(X,Y)} $\leftarrow$ {\tt brother(X,Z), parent(Z,Y).}
\item {\tt uncle(X,Y)} $\leftarrow$ {\tt parent(Z,Y), brother(X,Z).}
\end{enumerate}
To prove the goal {\tt uncle(ishmael,Y)} using the first version
of the rule, the interpreter will first look for
Ishmael's siblings (and find Isaac)
and then for the siblings' children (Esav and Jacov).
The left part of Figure~\ref{fig:family-database-two-trees} shows
the associated proof tree with a total of 10 nodes.
If we use the second version of the rule, the interpreter will create
all the parent-child pairs available in the database,
and will test for each parent whether he (or she) is Ishmael's sibling.
The right part of Figure~\ref{fig:family-database-two-trees} shows
the associated proof tree with a total of $4(N-2)+6 \cdot 2 + 2 = 4N + 6$
nodes, where N is the number of parent-child pairs in the database.
The tree contains two success branches and $N-2$ failure branches;
in the figure we show one example of each.
While the two versions of the rule yield identical
solution sets, the first version leads to a much smaller tree
and to a faster execution.

Note that this result is true only for the given mode 
({\tt bound,free}) of the head literal;
for the mode ({\tt free,bound}), as in {\tt uncle(X,jacov)},
the outcome is the contrary:
the second version of the rule yields a smaller tree.




\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{6in}

\medskip
\begin{center}
{\small
{\tt uncle(X,Y)} $\leftarrow$ {\tt brother(X,Z), parent(Z,Y).} 
\ \ 
{\tt uncle(X,Y)} $\leftarrow$ {\tt parent(Z,Y), brother(X,Z).}
}
\end{center}

\hspace{0.3in}
\begin{minipage}[t]{1.9in}
\epsfig{figure=figs/pictures/proof-tree-uncle-1.eps,width=1.9in}
\end{minipage}
\begin{minipage}[t]{3.5in}
\epsfig{figure=figs/pictures/proof-tree-uncle-2.eps,width=3.5in}
\end{minipage}

\end{minipage}
} % fbox
\caption{\label{fig:family-database-two-trees}
{\small
Two proof trees obtained with different orderings of a single rule in 
Example~\protect\ref{ex:family-uncle}.
} 
}
\end{center}
\end{figure}




%;;;;;;;;;;;;;;;;;;;;;;;;;;  C A T E G O R I E S   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



\subsection{Categories of Subgoal Ordering Methods}
\label{sec:interlaving-static-etc}

Assume that the current conjunctive goal (the current resolvent)
is $\left\{ A_1,A_2 \right\}$.  Assume that we use the rule 
``$A_1 \leftarrow A_{11},A_{12}.$''
to reduce $A_1$.  
According to Theorem~\ref{theorem:lloyd1}, the produced resolvent,
$\left\{ A_{11},A_{12},A_2\right\}$, can be executed in any order.
We call ordering methods that allow any permutation of the resolvent
{\em interleaving ordering methods}, since they permit interleaving
of subgoals from different rule bodies.
When ordering is performed only on rule bodies {\em before} using them
for reduction, 
the method is {\em non-interleaving}.
In the above example, interleaving methods will consider all
6 permutations of the resolvent, while non-interleaving methods
will consider only two orderings: 
$\left\la A_{11},A_{12},A_2\right\ra$ and 
$\left\la A_{12},A_{11},A_2\right\ra$.
Interleaving ordering methods deal with significantly more
possible orderings than non-interleaving methods.
That means that they can find more efficient orderings. 
On the other hand, the space of possible orderings may become prohibitively large,
requiring too many computational resources.

Subgoal ordering can take place at various stages of the 
proof process.  We divide all subgoal ordering methods 
into static, semi-dynamic and dynamic.
\begin{itemize}
\item
{\bf Static ordering:} 
The rule bodies are ordered before the execution starts.  
No ordering takes place during the execution.

\item
{\bf Semi-dynamic ordering:} 
Whenever a rule is selected for reduction, its body is ordered.  
The order of its
subgoals does not change after the reduction takes place.

\item
{\bf Dynamic ordering:} 
The ordering decision is made at each inference step.
\end{itemize}


Static methods add no overhead to the execution time.
However, the optimal ordering of a rule often depends on a
particular binding of a variable, which can be known only at run-time.
For instance, in Example~\ref{ex:family-uncle}
we saw that the first ordering of the rule is better for proving the goal
{\tt uncle(ishmael,Y)}.  And yet, for the goal {\tt uncle(X,jacov)},
it is the second ordering that yields more efficient execution.  
To handle such cases statically, we must compute the optimal
ordering for each possible binding.

Obviously, static ordering can only be non-interleaving.
The dynamic method is more flexible, since it can use more
updated knowledge about variable bindings, but
it also carries the largest runtime overhead, 
since it is invoked several times for each use of a rule body.
The semi-dynamic method is a compromise between the two:
it is more powerful than the static method, because it can dynamically
propose different orderings for different instances of the same
rule;  it also carries less overhead than the dynamic method, because
it is invoked only once for each use of a rule body.

The total time of proving a goal is the sum of
the ordering time and the inference time.
Interleaving and dynamic methods have the best potential
for reducing the inference time, but may significantly augment the
ordering time.  Static methods do not devote time to ordering
(it is done off-line), but have a limited potential for reducing the
inference time.

The algorithms described in this paper can be used for
all categories of ordering methods, although in the experiments described
in Section~\ref{sec:experimentation} we have only implemented semi-dynamic, 
non-interleaving ordering methods:
on each reduction, the rule body is ordered and added to the left end
of the resolvent, and then the leftmost literal of the resolvent is
selected for the next reduction step.





%;;;;;;;;;;;;;;;;;;;;;   R E L A T E D    W O R K   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



\subsection{Related Work}

The problem of computational inefficiency of logic inference was the
subject of extensive research.
The most obvious aspect of this inefficiency is the possible
non-termination of a proof.
Several researchers developed compile-time and run-time techniques to
detect and avoid infinite computations \cite{DeSchreye:94}.
A certain success was achieved in 
providing more advanced control through employment of co-routining for
inter-predicate synchronization purposes \cite{clark:79,porto:84,naish:84}.
Also, infinite computations can be avoided by pruning infinite branches
that do not contain solutions 
\cite{vasak:85,SmithGeneserethGinsberg:86,Bol:91}.
In the NAIL! system \cite{morris:88} 
subgoals are automatically reordered to avoid nontermination.

Still, even when the proof is finite, it is desirable to make it more efficient.
Several researchers studied the problem of clause ordering 
\shortcite{smith:89,cohen:90,etzioni:91,laird:92,mooney:93,greiner:96}.
If we are looking for {\em all} the solutions of a goal, then
the efficiency does not depend on the clause order
(assuming no {\tt cut}s).
Indeed, if some predicate has $m$ clauses, and for some argument bindings these
clauses produce all their solutions in times $t_1, t_2 \ldots t_m$,
then all solutions of the predicate under these bindings are obtained in time
\mbox{$t_1 + t_2 + \ldots + t_m$}, 
regardless of the order in which the clauses are applied.
Different clause orderings correspond to different orders in which
branches are selected in a proof tree;
if we traverse the entire tree, then the number of traversal steps
does not depend on the order of branch selection, though the order of
solutions found does depend on it.

Subgoal ordering, as was demonstrated in Example~\ref{ex:family-uncle}, can 
significantly affect the efficiency of proving a goal.
There are two major approaches to subgoal ordering.  The first approach
uses various heuristics to order subgoals, for example:
\begin{itemize}
\item
Choose a subgoal whose predicate has the smallest number of matching clauses
\cite{minker:78}.
\item
Prefer a subgoal with more constants \cite{minker:78}.
\item
Choose a subgoal with the largest {\em size},
where the size is defined as the number of 
occurrences of predicate symbols, function symbols, and variables \cite{nie:90}.
\item
Choose a subgoal with the largest {\em mass}, 
where the mass of a subgoal depends on the
frequency of its arguments and sub-arguments in the entire goal
\cite{nie:90}. 
\item
Choose a subgoal with the least number of solutions \cite{warren:81,nie:90}.
\item
Apply ``tests'' before ``generators'' \cite{naish:85:lpj}.
\item
Prefer calls that fail quickly \cite{naish:85}.
\end{itemize}
The heuristic methods usually execute quickly, but may yield
suboptimal orderings.

The second approach, which is adopted in this paper,
 aims at finding {\em optimal} orderings
\cite{smith:85,natarajan:87,markovitch:89:ordering}.
Natarajan proposed an efficient way to order a special sort of subgoal set
(where all subgoals are independent), while Smith and Genesereth
proposed a general, but inefficient algorithm. 
In the following section we build a unifying framework for
dealing with subgoal ordering and describe variations on
Natarajan's and Smith and Genesereth's algorithms.  We also show
how the two can be combined for increased efficiency.




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%               A L G O R I T H M S  --  O L D                   %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Algorithms for Subgoal Ordering in Logic Programs}
\label{sec:algorithms-old}

The goal of the work presented here is to order subgoals for
speeding up logic programs.  This section starts with 
an analysis of the cost of executing a sequence of subgoals.
The resulting formula is the basis for the subsequent ordering algorithms.  
Then we discuss dependence of subgoals and present existing ordering
algorithms for independent and dependent sets of subgoals.
Finally, we combine these algorithms into a more general and efficient one.





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%         C O S T      C O M P U T A T I O N                     %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\subsection{The Cost of Executing a Sequence of Subgoals}
\label{sec:cost}

In this subsection we analyze the cost of executing a sequence of subgoals.
The analysis builds mainly on the work of \citeA{smith:85}.

Let $\S = \{ A_1, A_2, \ldots A_k \}$ be a set of subgoals and $b$
be a binding.  
We denote $Sols(\S)$ to be the solution set of $\S$,
and define $Sols(\emptyset) = \{\emptyset\}$.
We denote $A_i|_b$ to be $A_i$ whose variables are bound according to $b$
($A_i|_{\emptyset} = A_i$).
Finally, we denote $Cost(A_i|_b)$ to be the amount of resources needed 
for proving $A_i|_b$.
$Cost(A_i|_b)$  should reflect the time complexity of proving $A_i$ under
binding $b$.  For example, the number of 
unification steps is a natural measure of complexity for logic programs
\cite{itai:87}.

To obtain the cost of finding all the solutions of 
an ordered sequence of subgoals
\begin{equation}
\Sv = \langle A_1, A_2, A_3, \ldots  A_n \rangle,
\label{eq:sequence}
\end{equation}
we note that the proof-tree of $A_1$ is traversed only once,
the tree of $A_2$ is traversed once for each
solution generated by $A_1$,
the tree of $A_3$ -- once for each solution of
$\{ A_1, A_2 \}$, etc. 
Consequently, the total cost of proving Equation~\ref{eq:sequence} is
\begin{eqnarray}
\label{eq:real-cost} 
Cost(\langle A_1,\ldots A_n \rangle) & = & Cost(A_1) +
\!\!\!\!\!\!\sum_{b \in Sols(\{A_1\})} \!\!\!\!\!\!\!Cost(A_2|_{b}) + \ldots +
\!\!\!\!\!\!\!\!\!\!\!\!\sum_{b \in Sols(\{ A_1,\ldots A_{n-1}\})} 
\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!Cost(A_n|_{b}) = \nonumber \\
& = &
\sum_{i=1}^{n} 
\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!
\sum_{\ \ \ \ \ \ \ \ \ b \in Sols(\{ A_1,\ldots A_{i-1}\})}
\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!Cost(A_i|_{b}).
\end{eqnarray}



To compute Equation~\ref{eq:real-cost} one must know the cost 
and the solution set for each subgoal under each binding.
To reduce the amount of information needed, we derive an equivalent
formula, which uses average cost and average number of solutions.

\bigskip

\begin{definition}
Let $\B$ be a set of subgoals, $A$ a subgoal.
Define $\cost(A)|_{\B}$ to be the average cost of 
$A$ over all solutions of $\B$ and
$\nsols(A)|_{\B}$ to be its average number of solutions 
over all solutions of $\B$:
\[
\cost(A)|_{\B} = 
\left\{ \begin{array}{ll}
Cost(A), & \B = \emptyset \\
\frac{\sum_{b \in Sols(\B)} Cost(A|_{b})}{| Sols(\B) | }, & 
 \B \neq \emptyset,\ Sols(\B) \neq \emptyset \\
\mbox{\em undefined},& \B \neq \emptyset,\ Sols(\B) = \emptyset 
\end{array} \right.
\]

\[
\nsols(A)|_{\B} = 
\left\{ \begin{array}{ll}
|Sols(\{A\})|, & \B = \emptyset \\
\frac{\sum_{b \in Sols(\B)} |Sols(\{A|_{b}\})|}{| Sols(\B) | }, & 
 \B \neq \emptyset,\ Sols(\B) \neq \emptyset \\
\mbox{\em undefined},& \B \neq \emptyset,\ Sols(\B) = \emptyset 
\end{array} \right.
\]
\end{definition}
\medskip

\noindent
>From the first definition, it follows that:
\begin{equation}
\sum_{b \in Sols(\{A_1,\ldots A_{i-1}\})} 
   \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!Cost(A_i|_{b}) =
   |Sols(\{A_1,\ldots A_{i-1}\})| \times \cost(A_i)|_{\{A_1,\ldots A_{i-1}\}}.
\label{eq:cost-derivation-1} 
\end{equation}
\noindent
If we apply the second definition recursively, we obtain
\begin{eqnarray}
|Sols(\{A_1,\ldots A_i\})| 
  &=& \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\sum_{\ \ \ \ \ \ \ b \in Sols(\{A_1,\ldots A_{i-1}\})} 
      \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!|Sols(\{A_i|_b\})| 
\nonumber \\
  &=& |Sols(\{A_1,\ldots A_{i-1}\})| \times \nsols(A_i)|_{\{A_1,\ldots A_{i-1}\}}
\nonumber \\
  &=& \ldots \ = \ \prod_{j=1}^i \nsols(A_j)|_{\{A_1 \ldots A_{j-1}\}}.
\label{eq:cost-derivation-2}
\end{eqnarray}
Note that we defined $Sols(\emptyset) = \{\emptyset\}$; thus, these
equations hold also for $i=1$.
Incorporation of Equations~\ref{eq:cost-derivation-1} 
and~\ref{eq:cost-derivation-2} into Equation~\ref{eq:real-cost} yields
\begin{equation} 
Cost(\la A_1, A_2, \ldots A_n \ra) = 
   \sum_{i=1}^n
   \left[
   \left( \prod_{j=1}^{i-1} \nsols(A_j)|_{\{A_1 \ldots A_{j-1}\}} \right)
   \times 
   \cost(A_i)|_{\{A_1 \ldots A_{i-1}\}} 
   \right].
\label{eq:cost}
\end{equation}

For each subgoal $A_i$, its average cost is multiplied by 
the total number of solutions of all the preceding subgoals.
We can define average cost and number of solutions for every continuous
sub-sequence of Equation~\ref{eq:sequence}:
$\forall k_1, k_2, 1 \leq {k_1} \leq {k_2} \leq n$,
\begin{eqnarray}
\cost(\langle A_{k_1}, \ldots A_{k_2} \rangle)|_{\{A_1, \ldots A_{k_1-1}\}} &=& 
\frac{\cost(\langle A_1, \ldots A_{k_2} \rangle)|_{\emptyset} -
      \cost(\langle A_1, \ldots A_{k_1-1} \rangle)|_{\emptyset}}
     {\nsols(\langle A_1, \ldots A_{k_1-1} \rangle)|_{\emptyset}}
\label{eq:cost-sub-sequence} \\
&=& \sum_{i=k_1}^{k_2} \left[
   \left( \prod_{j=k_1}^{i-1} \nsols(A_j)|_{\{A_1, \ldots A_{j-1}\}} \right)
   \times 
   \cost(A_i)|_{\{A_1, \ldots A_{i-1}\}}
   \right]
\nonumber \\
\nsols(\langle A_{k_1}, \ldots A_{k_2} \rangle)|_{\{A_1, \ldots A_{k_1-1}\}} &=& 
\frac{\nsols(\langle A_1, \ldots A_{k_2} \rangle)|_{\emptyset}}
     {\nsols(\langle A_1, \ldots A_{k_1-1} \rangle)|_{\emptyset}}
= \prod_{i=k_1}^{k_2} \nsols(A_i)|_{\{A_1, \ldots A_{i-1}\}}
\label{eq:nsols-sub-sequence} 
\end{eqnarray}




The values of $\cost(A_i)$ and $\nsols(A_i)$ depend on the
position of $A_i$ in the ordered sequence.
For example, assume that we want to find Abraham's sons, using the domain of 
Example~\ref{ex:family-uncle}.
The unordered conjunctive goal is {\tt \{male(Y),parent(abraham,Y)\}}.
Let there be $N$ males in the database (two of them, Isaac and Ishmael,
are Abraham's sons):
\[
\begin{array}{ll}
\nsols(\mbox{\tt male(Y)})|_{\emptyset} = N &
\nsols(\mbox{\tt parent(abraham,Y)})|_{\emptyset} = 2 \\
\nsols(\mbox{\tt male(Y)})|_{\mbox{\footnotesize\tt \{parent(abraham,Y)\}}} = 1 &
\nsols(\mbox{\tt parent(abraham,Y)})|_{\mbox{\footnotesize\tt \{male(Y)\}}} = 2/N
\end{array}
\]
Note that $\nsols(\la\mbox{\tt male(Y),parent(abraham,Y)}\ra) = 2 =
\nsols(\la\mbox{\tt parent(abraham,Y),male(Y)}\ra)$, 
exactly as Theorem~\ref{theorem:lloyd1} predicts.


Having defined the cost of a sequence of subgoals, we can now
define the objective of our ordering algorithms:

\bigskip

\begin{definition}
Let $\S$ be a set of subgoals.
Define $\pi(\S)$ to be set of all permutations of $\S$.
$\Ov_S \in \pi(\S)$ is a {\em minimal ordering} of $\S$
(denoted $Min(\Ov_S,\S)$),
if its cost according to Equation~\ref{eq:cost} is minimal over all
possible permutations of $\S$:
\[ Min(\Ov_S,\S) \iff \forall O'_S \in \pi(\S): Cost(\Ov_S) 
\leq Cost(O'_S). \]
\end{definition}
\smallskip

The total execution time is the sum of the time which is spent on ordering,
and the inference time spent by the interpreter on the ordered sequence.
In this paper we focus upon developing
algorithms for minimizing the inference time.  
Elsewhere \cite{Ledeniov:1998:CUC,Ledeniov:1998:LIF}
we present algorithms that attempt to reduce the total execution time.

The values of cost and number of solutions can be obtained
in various ways: by exact computation, by estimation and bounds, and
by learning.
Let us assume at the moment that there exists a mechanism
that returns the average cost and number of solutions
of a subgoal in time $\tau$.
In Section~\ref{sec:learning} we show how this control knowledge 
can be obtained by inductive learning.





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%                I  N  D  E  P  E  N  D  E  N  T                 %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Ordering of Independent Sets of Subgoals}
\label{sec:ordering-independent}

The general subgoal ordering problem is NP-hard \cite{ullman:88}.  
However, there is a special case where ordering can be performed
efficiently: if all the subgoals in the given set are independent,
i.e. do not share free variables.
This section begins with the definition of subgoal dependence and
related concepts. 
We then show an ordering algorithm for independent sets
and prove its correctness.


\subsubsection{Dependence of Subgoals}
\label{sec:dependence-definition}

\noindent 
\begin{definition} 
Let $\S$ and $\B$ be sets of subgoals
($\B$ is called the {\em binding set} of $\S$).
A pair of subgoals in $\S$ is {\em directly dependent} under $\B$, 
if they share a free variable not bound by a subgoal of $\B$.

A pair of subgoals is {\em indirectly dependent} with respect to 
$\S$ and $\B$
if there exists a third subgoal in $\S$ which is directly dependent 
on one of them under $\B$, 
and dependent (directly or indirectly) on the other one under $\B$.
A pair of subgoals of $\S$ is {\em independent} under $\B$
if it is not dependent under $\B$ (either directly or indirectly).  
A subgoal is {\em independent} of $\S$ under $\B$
if it is independent of all members of $\S$ under $\B$.

Two subsets $\S_1 \subset \S$ and $\S_2 \subset \S$ are
{\em mutually independent} under the binding set $\B$
if every pair of subgoals $(A_1,A_2)$, 
such that $A_1 \in \S_1 $  and $A_2 \in \S_2 $,
is independent under $\B$.

The entire  set $\S$ is called {\em independent} under the binding set $\B$
if all its subgoal pairs are independent under $\B$, 
and is called {\em dependent} otherwise.
A dependent set of subgoals is called {\em indivisible} if all its
subgoal pairs are dependent under $\B$, and {\em divisible} otherwise.

A {\em divisibility partition} of $\S$ under $\B$,
$DPart(\S,\B)$, is a partition of $\S$ into subsets that are mutually 
independent and indivisible under $\B$, except at most one
subset which contains all the subgoals independent of $\S$ under $\B$.
It is easy to show that $DPart(\S,\B)$ is unique.
\end{definition}

\bigskip

For example, let $\S_0= \{a, b(X), c(Y), d(X,Y), e(Z), f(Z,V), h(W)\}$.
With respect to $\S_0$ and an empty binding set,
the pair $\{b(X),d(X,Y)\}$ is directly dependent, $\{b(X),c(Y)\}$ is
indirectly dependent and $\{b(X),e(Z)\}$ is independent.
If we represent a set of subgoals as a graph, 
where subgoals are vertices and directly dependent subgoals
are connected by edges, then dependence is equivalent to
connectivity and indivisible subsets are equivalent
to connected components of size greater than 1.  
The  divisibility partition is the partition of a graph into connected
components, with all the ``lonely'' vertices collected together, in a
special component. 
Figure~\ref{fig:subgoal-graph}
shows an example of such a graph for the set $\S_0$ and for an empty binding set.
The whole set is divisible into four mutually independent subsets.
The subsets $\{ e(Z), f(Z,V) \}$ and $\{ b(X), c(Y), d(X,Y) \}$ are indivisible.
Elements of the divisibility partition $DPart(\S_0, \emptyset)$ are shown
by dotted lines.

\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{0.6\textwidth}

{\tt \{a, b(X), c(Y), d(X,Y), e(Z), f(Z,V), h(W)\}} $\Rightarrow$ 
\begin{center}
\epsfig{figure=figs/pictures/divisible-groups.eps,width=2.8in}
\end{center}

\end{minipage}
} % fbox
\caption{\label{fig:subgoal-graph}
{\small 
An example of a graph representing a set of subgoals.  
Directly dependent subgoals are connected by edges. 
Independent subgoals and indivisible subsets are equivalent
to connected components (surrounded by dashed lines).
The divisibility partition (under the empty binding set) is shown by
dotted lines. 
}}
\end{center}
\end{figure}

If a subgoal is independent of the set, 
then its average cost and number of solutions do not depend on 
its position within the ordered sequence:
\[
\cost(A)|_{\B} = 
\frac{\sum_{b \in Sols(\B)}Cost(A|_{b})}{|Sols(\B)|} =
\frac{|Sols(\B)| \times Cost(A)}{|Sols(\B)|} = Cost(A),
\]
\[
\nsols(A)|_{\B} =
\frac{\sum_{b \in Sols(\B)}|Sols(\{A|_{b}\})|}{|Sols(\B)|} =
\frac{|Sols(\B)| \times |Sols(\{A\})|}{|Sols(\B)|} =
|Sols(\{A\})|.
\]
In this case we can omit the binding information and write
$\cost(A_{i})$ instead of $\cost(A_{i})|_{\{A_1 \ldots A_{i-1}\}}$, and
$\nsols(A_{i})$ instead of $\nsols(A_{i})|_{\{A_1 \ldots A_{i-1}\}}$.

In practice, program rule bodies rarely feature independent sets of
literals.  
An example is the following clause, which states that children like
candy: 
\begin{center}
{\tt likes(X,Y)} $\leftarrow$ {\tt child(X), candy(Y).}
\end{center}
More often, independent rule bodies appear not because they are
written as such in the program text, but because some variables are
bound in (initially dependent) rule bodies, as a result of clause head
unification.
For example, if the rule 
\begin{center}
{\tt father(X,Y)}  $\leftarrow$  {\tt male(X), parent(X,Y).}
\end{center}
is used to reduce {\tt father(abraham,W)}, then {\tt X} is bound
to {\tt abraham}, and the rule body becomes independent.
Rule bodies often become independent after substitutions are
performed in the course of the inference process.





\subsubsection{Algorithm for Ordering Independent Sets by Sorting}

Let $\Sv$ be an ordered sub-sequence of subgoals, $\B$ a set of subgoals.
We denote
\[
cn(\Sv)|_{\B} = \frac{\nsols(\Sv)|_{\B} - 1}{\cost(\Sv)|_{\B}}.
\]
The name ``$cn$'' reflects the participation of $\cost$ and $\nsols$ in the
definition.
When the sub-sequence $\Sv$ is independent of other subgoals, the binding 
information ($|_{\B}$) can be omitted. 
Together, the average cost, average number of solutions, and $cn$ value
of a subgoal will be called {\em the control values} of this subgoal.


For independent sets, there exists an efficient ordering algorithm,
listed in Figure~\ref{fig:alg-sorting}.
The complexity of this algorithm is $O(n (\tau + \log n))$:
$O(n\cdot\tau)$ to obtain the control values of $n$ subgoals,
and  $O(n \log n)$ to perform the sorting \cite{knuth:73:vol3}.
To enable the division, we must define the cost so that $\cost(A_i)$ is
always positive. 
If we define the cost as the number of unifications performed, 
then always $\cost(A_i) \geq 1$, under a reasonable assumption
that predicates of all rule body subgoals are defined in the program. 
(In this case, at least one unification is performed for each subgoal).
Similar algorithms were proposed by \citeA{simon:75} and \citeA{natarajan:87}.


\begin{figure}[bt]
\begin{center}
\fbox{
\begin{minipage}{0.95\textwidth}
\smallskip
\noindent
\begin{algorithm}
\label{alg:sorting}
\ 
\begin{quotation}
\noindent
Let $\S = \{A_1,A_2,\ldots A_n\}$ be a set of subgoals.\\
Sort $\S$ using \( cn(A_i) = \frac{\nsols(A_i)-1}{\cost(A_i)} \) as the key for $A_i$,
and return the result.
\end{quotation}
\end{algorithm}
\smallskip
\end{minipage}
} % fbox
\caption{\label{fig:alg-sorting}
{\small 
The algorithm for ordering subgoals by sorting.
}}
\end{center}  
\end{figure}



\begin{example}
\label{ex:algorithm-sorting}

Let the set of independent subgoals be $\{p, q, r\}$, with the following 
control values:
\begin{center}
\begin{tabular}{|l|ccc|} \hline 
         &   p  &   q   &     r   \\ \hline 
\cost    & $10$ &  $20$ &     $5$ \\
\nsols   &  $1$ &   $5$ &   $0.1$ \\
\cn      &  $0$ & $0.2$ & $-0.18$ \\ \hline
\end{tabular}
\end{center}

We compute the costs of all possible orderings, using Equation~\ref{eq:cost}:
\begin{eqnarray*}
Cost(\la p, q, r \ra) &=& 10 + 1 \cdot 20 + 1 \cdot 5 \cdot 5 = 55 \\
Cost(\la p, r, q \ra) &=& 10 + 1 \cdot 5 + 1 \cdot 0.1 \cdot 20 = 17 \\
Cost(\la q, p, r \ra) &=& 20 + 5 \cdot 10 + 5 \cdot 1 \cdot 5 = 95 \\
Cost(\la q, r, p \ra) &=& 20 + 5 \cdot 5 + 5 \cdot 0.1 \cdot 10 = 50 \\
Cost(\la r, p, q \ra) &=& 5 + 0.1 \cdot 10 + 0.1 \cdot 1 \cdot 20 = 8 \\
Cost(\la r, q, p \ra) &=& 5 + 0.1 \cdot 20 + 0.1 \cdot 5 \cdot 10 = 12 
\end{eqnarray*}

The minimal ordering is $\la r, p, q \ra$, and this is exactly the
ordering which is found much more quickly by
Algorithm~\ref{alg:sorting} for the set $\{p, q, r\}$: 
$r$ has the smallest $cn$ value, $-0.18$,
then goes $p$ with $cn(p) = 0$, and finally $q$ with $cn(q) = 0.2$.
\end{example}


Note that the sorting algorithm reflects a well-known principle:
The best implementations of generate-and-test programs are obtained
with the tests placed as early as possible in the rule body and the
generations as late as possible \cite{naish:85:lpj}.  
Of course, the cheap tests should come first, while the expensive ones 
should come last. 
If one looks at the $cn$ measure, one quickly realizes that tests
should be put in front (because $\nsols < 1$, so $cn < 0$), while 
generator subgoals should move towards the end ($\nsols > 1$, so 
$cn > 0$). 
The weakness of the ``test-first'' principle is in the fact that not
every subgoal can be easily tagged as a test or a generator.
If one subgoal has $\nsols < 1$ and another one has 
$\nsols > 1$, then their order is obvious even without looking at the
costs (because their $cn$ values have different signs). 
But if both subgoals have $\nsols < 1$, or both have $\nsols > 1$,
then the decision is not so simple.
Sorting by $cn$ can correctly handle all the possible cases.






\subsubsection{Correctness Proof of the Sorting Algorithm for Independent Sets}
\label{sec:sorting-correctness}

We saw that Algorithm~\ref{alg:sorting} 
found a minimal ordering in Example~\ref{ex:algorithm-sorting}. 
We are now going to prove that Algorithm~\ref{alg:sorting} {\em always}
finds a minimal ordering for independent sets. 
First we show an important lemma which will also be used in further discussion.
This lemma states that substitution of a sub-sequence by its cheaper
permutation makes the entire sequence cheaper.

\begin{lemma}
\label{lemma:cheaper-permutation} \ \\
Let $\Sv = \Av\cc\Bv\cc\Cv$, $\Sv' = \Av\cc\Bv'\cc\Cv$,
where $\Bv$ and $\Bv'$ are permutations of one another,
and $\Av$ either is empty or has $\nsols(\Av) > 0$. Then
\[Cost(\Sv) < Cost(\Sv') \iff \cost(\Bv)|_{\Av} < \cost(\Bv')|_{\Av}, \]
\[Cost(\Sv) = Cost(\Sv') \iff \cost(\Bv)|_{\Av} = \cost(\Bv')|_{\Av}.\]

\end{lemma}

\begin{proof}
If $\Av$ and $\Cv$ are not empty,
\noindent
{\small
\begin{eqnarray*}
Cost(\Sv) - Cost(\Sv')
&=& Cost(\Av\cc\Bv\cc\Cv) - Cost(\Av\cc\Bv'\cc\Cv) = \\
&\stackrel{\mbox{(\ref{eq:cost})}}{=} &
    \left( \cost(\Av)|_{\emptyset}
         + \nsols(\Av)|_{\emptyset}\times\cost(\Bv)|_{\Av}
         + \nsols(\Av\cc\Bv)|_{\emptyset}\times\cost(\Cv)|_{\Av\cc\Bv}
    \right) - \\
& & \left( \cost(\Av)|_{\emptyset}
         + \nsols(\Av)|_{\emptyset}\times\cost(\Bv')|_{\Av}
         + \nsols(\Av\cc\Bv')|_{\emptyset}\times\cost(\Cv)|_{\Av\cc\Bv'}
    \right).
\end{eqnarray*}
}
By Theorem~\ref{theorem:lloyd1}, $\Bv$ and $\Bv'$ produce the same
solution sets. 
Hence, the third terms in the parentheses above are equal, and  
\[
Cost(\Sv) - Cost(\Sv') = \nsols(\Av)|_{\emptyset} \times 
    \left( \cost(\Bv)|_{\Av} - \cost(\Bv')|_{\Av} \right).
\]
Since $\nsols(\Av) > 0$, the sign of $Cost(\Sv) - Cost(\Sv')$
coincides with the sign of $\cost(\Bv)|_{\Av} - \cost(\Bv')|_{\Av}$.

If $\Av$ or $\Cv$ is empty, the proof is similar.
\hfill $\Box$
\end{proof}

\medskip


\begin{definition}
Let $\Sv = \Av \cc \Bv_1 \cc \Cv \cc \Bv_2 \cc \Dv$
be an ordered sequence of subgoals
($\Av$, $\Cv$ and $\Dv$ may be empty sequences).
With respect to $\Sv$, the pair $\langle \Bv_1, \Bv_2 \rangle$ is
\begin{itemize}
\item {\em cn-ordered},  if $cn(\Bv_1)|_{\Av} \leq  
                      cn(\Bv_2)|_{\Av\cup\Bv_1\cup\Cv}$
\item {\em cn-inverted}, if $cn(\Bv_1)|_{\Av} >
                      cn(\Bv_2)|_{\Av\cup\Bv_1\cup\Cv}$
\end{itemize}

\end{definition}


We now show that two adjacent {\em mutually independent} sequences of subgoals
in a minimal ordering must be cn-ordered.

\begin{lemma}
\label{lemma:independent-adjacent}
\ \\
Let $\Sv = \Av \cc \Bv_1 \cc \Bv_2 \cc \Cv $,
    $\Sv' = \Av \cc \Bv_2 \cc \Bv_1 \cc \Cv $,
where $\Bv_1$, $\Bv_2$ are mutually independent under $\Av$.
Let $\Av$ either be empty or have $\nsols(\Av) > 0$.
Then
\begin{eqnarray*}
Cost(\Sv) < Cost(\Sv') &\iff& cn(\Bv_1)|_{\Av} < cn(\Bv_2)|_{\Av}, \\
Cost(\Sv) = Cost(\Sv') &\iff& cn(\Bv_1)|_{\Av} = cn(\Bv_2)|_{\Av}.
\end{eqnarray*}
\end{lemma}
\begin{proof}
\begin{eqnarray*}
Cost(\Sv) < Cost(\Sv') 
&\stackrel{\mbox{Lemma~\ref{lemma:cheaper-permutation}}}{\iff} &
\cost(\Bv_1\cc\Bv_2)|_{\Av} < \cost(\Bv_2\cc\Bv_1)|_{\Av} \\
&\iff& \cost(\Bv_1)|_{\Av} 
       \!+ \nsols(\Bv_1)|_{\Av}
        \!\!\times \cost(\Bv_2)|_{\Av\cup\Bv_1} < \\
& &     \cost(\Bv_2)|_{\Av} 
        \!+ \nsols(\Bv_2)|_{\Av}
          \!\!\times \cost(\Bv_1)|_{\Av\cup\Bv_2} \\
&\hspace{-7mm}\stackrel{\mbox{indep.$\{\Bv_1,\Bv_2\}$}}{\iff} &
  \cost(\Bv_1)|_{\Av} 
       \!+ \nsols(\Bv_1)|_{\Av}
        \!\!\times \cost(\Bv_2)|_{\Av} < \\ 
& &  \cost(\Bv_2)|_{\Av} 
        \!+ \nsols(\Bv_2)|_{\Av}
          \!\!\times \cost(\Bv_1)|_{\Av} \\
&\iff& \nsols(\Bv_1)|_{\Av} \times \cost(\Bv_2)|_{\Av} - \cost(\Bv_2)|_{\Av} < \\
& &    \nsols(\Bv_2)|_{\Av} \times \cost(\Bv_1)|_{\Av} - \cost(\Bv_1)|_{\Av} \\
&\hspace{-7mm}\stackrel{\cost(\Bv_i)|_{\Av}>0}{\iff} &
   \frac{\nsols(\Bv_1)|_{\Av} - 1}{\cost(\Bv_1)|_{\Av}} 
     < \frac{\nsols(\Bv_2)|_{\Av} - 1}{\cost(\Bv_2)|_{\Av}} \\
&\iff& cn(\Bv_1)|_{\Av} < cn(\Bv_2)|_{\Av} \\
\\
Cost(\Sv) = Cost(\Sv') &\iff& cn(\Bv_1)|_{\Av} = cn(\Bv_2)|_{\Av} 
\mbox{\ \  ---\  similar. \hspace{1in} $\Box$}
\end{eqnarray*}
\end{proof}



In an {\em independent set}, all subgoal pairs are independent,
in particular all adjacent pairs.
So, in a minimal ordering of an independent set, all adjacent subgoal
pairs must be cn-ordered; otherwise, the cost of the sequence can be reduced
by a transposition of such pair.
This conclusion is expressed in the following theorem.


\noindent
\begin{theorem}
\label{theorem:sorting-independent}
\ \\
Let $\S$ be an independent set.  
Let  $\Sv$ be an ordering of $\S$.
$\Sv$ is minimal iff all the subgoals in $\Sv$ are sorted 
in non-decreasing order by their $cn$ values.
\end{theorem}

\begin{proof}
\begin{enumerate}
\item
Let $\Sv$ be a minimal ordering of $\S$. 
If $\Sv$ contains a cn-inverted adjacent pair of subgoals, 
then transposition of this pair reduces the cost of $\Sv$
(Lemma~\ref{lemma:independent-adjacent}),
contradicting the minimality of $\Sv$.

\item
Let $\Sv$ be some ordering of $\S$, whose subgoals are sorted in
non-decreasing order by $cn$.
Let $\Sv'$ be a minimal ordering of $\S$.
According to item 1, $\Sv'$ is also sorted by $cn$.
The only possible difference between the two sequences
is the internal ordering of sub-sequences with equal $cn$ values.
The ordering of each such sub-sequence in $\Sv$ can be transformed
to the ordering of its counterpart sub-sequence in $\Sv'$ by
a finite number of transpositions of adjacent subgoals.
By Lemma~\ref{lemma:independent-adjacent}, transpositions of adjacent independent 
subgoals with equal $cn$ values cannot change the cost of the sequence.  
Therefore, \mbox{$Cost(\Sv) = Cost(\Sv')$}, and $\Sv$ is a minimal ordering of $\S$
(since $\Sv'$ is minimal).
\hfill $\Box$
\end{enumerate}
\end{proof}

\begin{corollary} 
\label{corollary:sorting-algorithm-is-correct}
Algorithm~\ref{alg:sorting} finds a minimal ordering of 
an independent set of subgoals.
\end{corollary}








%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%        D  E  P  E  N  D  E  N  T    --    O L D                %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\subsection{Ordering of Dependent Sets of Subgoals}
\label{sec:ordering-dependent}

Algorithm~\ref{alg:sorting} does not guarantee finding
a minimal ordering when the given set of
subgoals is dependent, as the following proposition shows.

\begin{proposition}
\label{prop:cannot-sort-dependent}
When the given set of subgoals is dependent, then: 
\begin{enumerate} 
\item The result of Algorithm~\ref{alg:sorting} on it is not always defined. 
\item Even when the result is defined, it is not always a minimal ordering
of the set. 
\end{enumerate} 
\end{proposition}


\begin{proof} Both claims are proved by counter-examples.
\begin{enumerate}
\item
We show a set of subgoals that cannot be ordered by sorting.

\begin{minipage}[t]{1.75in}
\noindent
The program:
\begin{verbatim}
  a(c1).   b(c1).
  a(c2).   b(c2).
\end{verbatim}
\end{minipage}
\begin{minipage}[t]{3in}
\noindent
Control values: \\
\begin{tabular}{l|cccc} 
& $a(X)|_{\emptyset}$ & $a(X)|_{\{b(X)\}}$ & $b(X)|_{\emptyset}$ & $b(X)|_{\{a(X)\}}$ 
\\ \hline 
\cost  & $2$ & $2$ & $2$ & $2$  \\
\nsols & $2$ & $1$ & $2$ & $1$  \\
\cn    & $\frac{1}{2}$ & $0$ & $\frac{1}{2}$ & $0$
\end{tabular}
\end{minipage}

\medskip
\noindent
The set {\tt \{a(X), b(X)\}} has two possible orderings,
$\la a(X), b(X) \ra$ and $\la b(X), a(X) \ra$.
Both orderings have minimal cost, though neither one is sorted by $cn$:
each ordering has $cn = \frac{1}{2}$ for its first subgoal,
and $cn = 0$ for the second one.
Sorting by $cn$ is impossible here: when we transpose subgoals, their $cn$ values
are changed, and the pair becomes cn-inverted again.



\item
We show a set of subgoals that can be ordered by sorting,
but its sorted ordering is not minimal.

\begin{minipage}[t]{1.75in}
\noindent
The program: \\
{\tt a(c1).    }\\
{\tt a(c1).    }\\
{\tt b(c1).}\\
{\tt b(c2)} $\leftarrow$ {\tt a(c1), a(c2).}
\end{minipage}
\begin{minipage}[t]{3in}
\noindent
Control values:\\
\begin{tabular}{l|cccc} 
       & $a(X)|_{\emptyset}$ & $a(X)|_{\{b(X)\}}$ & 
         $b(X)|_{\emptyset}$ & $b(X)|_{\{a(X)\}}$ \\ \hline 
\cost  &  2 & 2 & 8 & 2 \\
\nsols &  2 & 2 & 1 & 1 \\
\cn    & $\frac{1}{2}$ & $\frac{1}{2}$ & 0 & 0 
\end{tabular}
\end{minipage}

\medskip
\noindent
Let the unordered set of subgoals be {\tt \{a(X), b(X)\}}.
Its ordering $\langle b(X), a(X) \rangle$ is sorted by $cn$,
while $\langle a(X), b(X) \rangle$ is not.
But $\langle a(X), b(X) \rangle$ is cheaper than $\langle b(X), a(X) \rangle$:
\begin{eqnarray*}
\cost(\langle a(X),b(X) \rangle) = 2 + 2 \cdot 2 = 6 &\ &
\cost(\langle b(X),a(X) \rangle) = 8 + 1 \cdot 2 = 10
\end{eqnarray*}
\ \hfill $\Box$
\end{enumerate}
\end{proof}




Since sorting cannot guarantee minimal ordering for dependent subgoals,
we now consider alternative ordering algorithms.
The simplest algorithm checks every possible permutation of the set
and returns the one with the minimal cost.  
The listing for this algorithm is shown in Figure \ref{fig:alg-permutations}.


\begin{figure}[htb]
\begin{center}
\fbox{
\begin{minipage}{0.90\textwidth}
\smallskip
\noindent
\begin{algorithm}
\label{alg:permutations}
\ 
\begin{quotation}
\noindent
For each permutation of subgoals, find its cost according to 
Equation~\ref{eq:cost}.\\
Store the currently cheapest permutation and update it when
a cheaper one is found.\\
Finally, return the cheapest permutation.
\end{quotation}
\end{algorithm}
\smallskip
\end{minipage}
} %fbox

\caption{\label{fig:alg-permutations}
{\small 
The algorithm for subgoal ordering by an exhaustive check of all
permutations. 
}}
\end{center}  
\end{figure}

This algorithm  runs in $O(\tau \cdot n!)$ time, where $\tau$
is the time it takes to compute the control values
for one subgoal, and $n$ is the number of subgoals.

\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{0.85\textwidth}

\smallskip
\noindent
\begin{algorithm} \ 
\label{alg:prefixes}
\end{algorithm}

\begin{tabbing}
\TABLINE{5mm}
{\bf Order}$(\S)$  \\
\>  let ${\cal P}_0 \leftarrow \{ \emptyset \},\  n \leftarrow |\S|$\\
\>  loop for $k = 1$ to $n$ \\
\>  \>  ${\cal P}_k' \leftarrow \left\{ \Pv \cc B 
           \ \left|\  \Pv \in {\cal P}_{k-1},\ B \in \S \setminus \Pv \right. \right\}$ \\
\>  \>  ${\cal P}_k \leftarrow \left\{ \Pv \in {\cal P}_k'
           \ \left|\  \forall \Pv' \in {\cal P}_k',\  
           \left[ permutation(\Pv,\Pv') \Rightarrow
           Cost(\Pv) \leq Cost(\Pv') \right] \right. \right\}$ \\
\>  Return {\em the single member of} ${\cal P}_n$.
\end{tabbing}

\smallskip
\end{minipage}
} % fbox
\caption{\label{fig:alg-prefixes}
{\small 
The ordering algorithm which checks permutations of ordered prefixes.
}}
\end{center}  
\end{figure}


The following observation can help to reduce the ordering time
at the expense of additional space.
Ordered sequences can be constructed incrementally, by adding
subgoals to the right ends of ordered prefixes.
By Lemma~\ref{lemma:cheaper-permutation}, if a cheaper permutation
of a prefix exists, then this prefix cannot belong to a minimal
ordering.
The ordering algorithm can build prefixes with increasing lengths,
at each step adding to the right end of each prefix one of the 
subgoals that do not appear in it already, 
and for each subset keeping only its cheapest permutation
(if several permutations have equal cost, any one of them can be chosen).
The listing for this algorithm is shown in Figure~\ref{fig:alg-prefixes}.
At each step $k$, ${\cal P}_k'$ stores the set of prefixes from step $k-1$
extended by every subgoal not appearing there already.
${\cal P}_k \subseteq {\cal P}_k'$, and in ${\cal P}_k$ each subset of
subgoals is represented only by its cheapest permutation.
Obviously, $|{\cal P}_k| = (^n_k)$ 
(one prefix is kept for every subset of $\S$ of size $k$).
For each prefix of length $k-1$, there are $n-(k-1)$ possible
continuations of length $k$.
The size of ${\cal P}_k'$ is as follows:
\[
|{\cal P}_k'| = (^{\ \;n}_{k-1}) \cdot (n-(k-1)) 
= \frac{n!}{(n-(k-1))!(k-1)!} \cdot (n-(k-1))
= \frac{k}{k} \cdot \frac{n!}{(n-k)!(k-1)!} = k \cdot (^n_k).
\]
For each prefix, we compute its cost in $\tau$ time.
The permutation test can be completed in
$O(n)$ time, by using, for example, a trie structure \shortcite{aho:87},
where subgoals in prefixes are sorted lexicographically.
Each step $k$ takes \mbox{$O((n + \tau) \cdot k \cdot (^n_k))$} time,
and the whole algorithm runs in 
\[ \sum_{k=1}^{n} O((n + \tau) \cdot k \cdot (^n_k)) = 
O(n \cdot (n + \tau) \cdot \sum_{k=1}^{n}
(^n_k)) =  O(n \cdot (n + \tau) \cdot 2^n). \]
If $\tau = O(n)$, this makes $O(n^2 \cdot 2^n)$.


\citeA{smith:85} and \citeA{natarajan:87} point out that
in a minimal ordered sequence every adjacent pair of subgoals must
satisfy an {\em adjacency restriction}.
The most general form of such a restriction in our notation says that
two adjacent subgoals $A_k$ and $A_{k+1}$ in a minimal ordering 
$\la A_1,A_2\ldots A_n\ra$ must satisfy 
\begin{equation}
\cost(\la A_k, A_{k+1} \ra)|_{\{A_1 \ldots A_{k-1}\}} \leq
\cost(\la A_{k+1}, A_k \ra)|_{\{A_1 \ldots A_{k-1}\}}.
 \label{eq:adjacency-restriction}
\end{equation}
The restriction follows immediately from Lemma~\ref{lemma:cheaper-permutation}.
However, it can only help to find a {\em locally} minimal
ordering, i.e., an ordering that 
 cannot be improved by transpositions of adjacent subgoals.
It is possible that all adjacent subgoal pairs satisfy
Equation~\ref{eq:adjacency-restriction}, but the ordering is still not
minimal. 
The following example illustrates this statement.


\begin{example} 
\label{ex:adjacency-restriction}

Let the unordered set be $\{ p(X), q(X), r(X) \}$, where the
predicates are defined by the following program:
\begin{center}
\fbox{
\begin{minipage}{2in}
\(
\begin{array}{lll}
p(c_1).\hspace{7mm} & q(c_1).\hspace{7mm} & r(c_1). \\
p(c_2) \leftarrow f.& q(c_2).             & r(c_1). \\
                    & q(c_3) \leftarrow f.\\
\end{array}
\)\\

$f \leftarrow$ fails after 50 unifications.
\end{minipage}
} % fbox
\end{center}

\noindent
The ordering $\la p(X), q(X), r(X) \ra$ satisfies the adjacency
restriction (Equation~\ref{eq:adjacency-restriction}):

\[
\begin{array}{ll}
\cost(p(X),q(X))|_{\emptyset} = 55 \hspace{1cm} &
\cost(q(X),r(X))|_{p(X)} = 5 \\
\cost(q(X),p(X))|_{\emptyset} = 107 &
\cost(r(X),q(X))|_{p(X)} = 8 
\end{array}
\]

\noindent
But it is not minimal:
\begin{center}
$\cost(\la p(X), q(X), r(X) \ra) = 57$\\
$\cost(\la r(X), p(X), q(X) \ra) = 12$
\end{center}
\end{example}


To find a globally minimal ordering,
it seems beneficial to combine the prefix algorithm with the adjacency restriction:
if a prefix does not satisfy the adjacency restriction, then there is a cheaper
permutation of this prefix. 
The adjacency test can be performed faster than the permutation test,
since it must only consider the two last subgoals of each prefix.
Nevertheless, the number of
prefixes remaining after each step of Algorithm~\ref{alg:prefixes}
is not reduced: if a prefix is rejected due to a violation of the adjacency
restriction, it would have also been rejected by the permutation test.
Furthermore, if the adjacency restriction test does not fail, 
we should still perform the permutation test to avoid local minima
(as in Example~\ref{ex:adjacency-restriction}). 
The adjacency test succeeds in at least half of the cases:
if we examine a prefix $\la A_1, \ldots A_k, B_1, B_2\ra$, we shall also examine
$\la A_1, \ldots A_k, B_2, B_1\ra$, and the adjacency test cannot fail in both.
Consequently, addition of the adjacency test can only halve the total
running time of the ordering algorithm, leaving it $O(n^2 \cdot 2^n)$
in the worst case.

Smith and Genesereth propose performing a best-first search
in the space of ordered prefixes, preferring prefixes with
lower cost.  The best-first search can be combined with the
permutation test and the adjacency restriction.  In addition,
when the subgoals not in a prefix are independent under
its binding, they can be sorted, and the sorted result concatenated 
to the prefix.  
By Lemma~\ref{lemma:cheaper-permutation} and
Corollary~\ref{corollary:sorting-algorithm-is-correct}, 
this produces the cheapest completion of this prefix.  
When we perform completion,
there is no need to perform the adjacency or permutation test: 
if a complete sequence is not minimal, it will never be chosen as the cheapest
prefix; even if it is added to the list of prefixes, it will
never be extracted therefrom.
The resulting algorithm is shown in Figure~\ref{fig:alg-smith+natarajan}.

\begin{figure}[hbt]
\begin{center}
\medskip
\fbox{
\begin{minipage}{0.85\textwidth}

\medskip
\begin{algorithm} \
\label{alg:smith+natarajan}
\end{algorithm}

\begin{quotation}
\begin{tabbing}
\TABLINE{5mm}
{\bf Order}$(\S)$  \\
\>  let {\em prefix-list} $\leftarrow$ $\emptyset$,
        {\em prefix} $\leftarrow$ $\emptyset$,
        {\em rest} $\leftarrow$ $\S$ \\
\>  loop until {\bf empty}({\em rest}) \\
\>  \>  if {\bf Independent}({\em rest}$|_{\mbox{\footnotesize\em prefix}}$) \\
\>  \>  then \\
\>  \>  \>  let {\em completion} $\leftarrow$ {\em prefix}$\cc${\bf Sort-by-cn}({\em rest}$|_{\mbox{\footnotesize\em prefix}}$)\\
\>  \>  \>  {\bf Insert-By-Cost}({\em completion}, {\em prefix-list}) \\
\>  \>  else \\
\>  \>  \>  loop for {\em subgoal} $\in$ {\em rest}\\
\>  \>  \>  \>  let {\em extension} $\leftarrow$ {\em prefix}$\cc${\em subgoal}\\
\>  \>  \>  \>  if  {\bf Adjacency-Restriction-Test}({\em extension})\\
\>  \>  \>  \>  and {\bf Permutation-Test}({\em extension})\\
\>  \>  \>  \>  then \\
\>  \>  \>  \>  \>  {\bf Insert-By-Cost}({\em extension}, {\em prefix-list})\\
\>  \>  {\em prefix} $\leftarrow$ {\bf Cheapest}({\em prefix-list})\\
\>  \>  {\bf Remove-from-list}({\em prefix}, {\em prefix-list})\\
\>  \>  {\em rest} $\leftarrow \S \setminus${\em prefix} \\
\>  Return {\em prefix}\\
\end{tabbing}
\end{quotation}

\end{minipage}
} %fbox
\caption{\label{fig:alg-smith+natarajan}
{\small 
An algorithm for subgoal ordering, incorporating the ideas of earlier researchers.
}}
\end{center}  
\end{figure}


The advantage of using best-first search is that it avoids
expanding prefixes whose cost is higher than
the cost of the minimal ordering.  The policy used
by the algorithm may, however, be suboptimal or even harmful.
It often happens that the
best completion of a cheaper prefix is much more expensive than the best completion
of a more expensive prefix.  When the number of solutions is large, it
is better to place subgoals with high costs closer to the beginning
of the ordering to reduce the number of times that their cost
is multiplied.

For example, let the set be $\{a(X),b(X)\}$, with 
$\cost(a(X)) = 10$, $\cost(b(X))$ $=$ $\nsols(a(X))$ $=$ $\nsols(b(X))$ $= 2$.
Then a minimal ordering starts with the most expensive prefix:
\[ Cost(\la a(X), b(X) \ra) = 10 + 2 \cdot 2 = 14 \]
\[ Cost(\la b(X), a(X) \ra) = 2 + 2 \cdot 10 = 22 \]
If there are many prefixes whose cost is higher than the cost of the minimal
ordering, then best-first search saves time.
But if the number of such prefixes is small, using best-first search can
increase the total time, due to the need to perform insertion of a prefix into
a priority queue, according to its cost.

A sample run of Algorithm~\ref{alg:smith+natarajan} will be shown later
(in Section~\ref{sec:sample-run}).











%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%        D  E  P  E  N  D  E  N  T    --    N E W                %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{The Divide-and-Conquer Subgoal Ordering Algorithm}
\label{sec:algorithm-new}


Algorithm~\ref{alg:sorting} presented in Section~\ref{sec:ordering-independent} 
is very efficient, but is applicable only
when the entire set of subgoals is independent.
Algorithm~\ref{alg:prefixes} can handle a dependent set of subgoals
but is very inefficient.  Algorithm~\ref{alg:smith+natarajan}, a combination
of the two, can exploit independence of subgoals for better
efficiency.  
However, the obtained benefit is quite limited.
In this section, we present the Divide-and-Conquer (\DC) algorithm,
which is able to exploit subgoal independence in a more elaborate way.
The algorithm divides the set of subgoals into smaller subsets,
orders these subsets recursively and combines the results. 




% ;;;;;;;;;;;;;;  D I V I S I B I L I T Y    T R E E  ;;;;;;;;;;;;;;;;;;;;;;

\subsection{Divisibility Trees of Subgoal Sets}
In this subsection we define a structure that represents all the 
ways of breaking a subgoal set into independent parts.
Our algorithm will work by traversing this structure.

\medskip

\begin{definition}
Let $\S$ and $\B$ be sets of subgoals.  
The {\em \TREE\ of $\S$ under $\B$}, 
$DTree(\S,\B)$, is an AND-OR tree defined as follows:

{\small
\[
DTree(\S,\B) = \left\{\begin{array}{ll}
\mbox{leaf}(\S,\B)& -\ \S \mbox{ is independent under } \B \\ \\
\mbox{OR}(\S,\B,\{DTree(\S \setminus \{B_i\}, \B \cup \{B_i\})\ |\ B_i \in \S \})&
-\ \S \mbox{ is indivisible under } \B \\ \\
\mbox{AND}(\S,\B,\{DTree(\S_i, \B)\ |\ \S_i \in DPart(\S, \B) \})&
-\ \S \mbox{ is divisible under } \B \\
			 \end{array} \right.
\]
}
\end{definition}

Each node $N$ in the tree $DTree(\S_0,\B_0)$ has an associated set of subgoals
$\S(N) \subseteq \S_0$ and an associated binding set $\B(N) \supseteq \B_0$.  
For the root node, $\S(N) = \S_0$, $\B(N) = \B_0$.
If the binding set of the root is not specified explicitly, we assume it 
to be empty.
For AND-nodes and OR-nodes we also define the sets of children.

\begin{itemize}
\item 
If  $\S(N)$ is {\em independent} under $\B(N)$, then $N$ is a leaf.
\item 
If  $\S(N)$ is {\em indivisible} under $\B(N)$, then
$N$ is an OR-node.  Each subgoal $B_i$ in $\S(N)$ defines
a child node whose set of subgoals is $\S(N) \setminus \{ B_i \}$
and the binding set is $\B(N) \cup \{ B_i \}$.
We call $B_i$ the {\em binder} of the generated child.
Note that the binding set of every node in a \TREE\ is the union of the 
binders of all its indivisible ancestors and of the root's binding set.
\item 
If $\S(N)$ is {\em divisible} under $\B(N)$, then
$N$ is an AND-node.  Each subset $\S_i$ in the divisibility
partition $DPart(\S(N), \B(N))$ defines a child node with 
associated set of subgoals $\S_i$ and binding set $\B(N)$.
Divisibility partition was defined in Section~\ref{sec:dependence-definition}.
\end{itemize}

It is easy to show that the \TREE\ of a set of subgoals is
unique up to the order of children of each node.
Figure~\ref{fig:and-or-tree} shows the \TREE\ 
of the set $\{a,b,c(X),d(X),e(X)\}$ under empty initial binding set.
The associated sets and binding sets are written next to the nodes.


\begin{figure}[bt]
\begin{center}
\fbox{
\begin{minipage}{4in}

\medskip
\begin{center}
\epsfig{figure=figs/pictures/and-or-tree.eps,width=3.8in}
\end{center}

\medskip
\end{minipage}
} % fbox
\caption{\label{fig:and-or-tree}
{\small 
The \TREE\ of $\{a,b,c(X),d(X),e(X)\}$ under empty initial binding set.
The set associated with node $n1$ is divisible, and is represented by an 
AND-node. Its children correspond to its divisibility subsets -- one independent,
$S(n2) = \{a,b\}$,
and one indivisible, $S(n3)=\{c(X),d(X),e(X)\}$. 
$n3$ is an OR-node, whose children correspond to its three subgoals
(each subgoal serves as a binder in one of the children).
The sets $S(n2)$, $S(n4)$, $S(n5)$ and $S(n6)$ are independent under
their respective binding sets, and their nodes are leaves.
Here we assumed that the subgoals $c(X)$, $d(X)$ and $e(X)$ bind $X$
as a result of their proof.
}}
\end{center}  
\end{figure}



The following lemma expresses an important property of \TREE s:
subgoals of each node are independent of the rest of subgoals
under the binding set of the node.

\begin{lemma}
Let $\S_0$ be a set of subgoals.
Then for every node $N$ in $DTree(\S_0,\emptyset)$, 
for every subgoal $A \in \S(N)$,
and for every subgoal $Y \in \S_0 \setminus (\S(N) \cup \B(N))$, 
$A$ and $Y$ are independent under $\B(N)$.
\end{lemma}

\begin{proof}
by induction on the depth of $N$ in the \TREE.
\begin{description}
\item[Inductive base:] 
$N$ is the root node, $\S_0 \setminus \S(N)$ is empty, and no such $Y$ exists.
\item[Inductive hypothesis:]
The lemma holds for $M$, the parent node of $N$.
\item[Inductive step:]
Let $A \in \S(N)$, $Y \in \S_0 \setminus (\S(N) \cup \B(N))$.
$A \in \S(M)$, and for $M$ the lemma holds, thus
either $A$ and $Y$ are independent under $\B(M)$, or $Y \in \S(M)$.

If $A$ and $Y$ are independent under $\B(M)$, then they are also independent 
under $\B(N)$, since $\B(M) \subseteq \B(N)$.
Otherwise, $A$ and $Y$ are dependent under $\B(M)$, and $Y \in \S(M)$.
\begin{itemize}
\item
If $M$ is an AND-node, and $A$ and $Y$ are dependent under $\B(M)$,
then $A$ and $Y$ belong to the same element of $DPart(\S(M),\B(M))$,
and $Y \in \S(N)$ -- a contradiction.
\item
If $M$ is an OR-node and $Y \in \S(M) \setminus \S(N)$, then $Y$ must be 
the binder of $N$.
But then $\B(N) = \B(M)\cup\{Y\}$ and $Y \in \B(N)$ -- a contradiction
again.
\hfill $\Box$
\end{itemize}
\end{description}
\end{proof}

The lemma relates to subgoal independence inside \TREE s.
We shall sometimes need to argue about independence inside ordered
sequences of subgoals. 
The following corollary provides the necessary connecting link.

\begin{corollary}
\label{corollary:interleaving-independent}
Let $\S_0$ be a set of subgoals, 
$N$ be a node in the \TREE\ of $\S_0$,
$\Sv$ an ordering of $\S_0$,
$\Sv = \Sv_1\cc\Sv_2$, where $\B(N) \subseteq \Sv_1$
and $\S(N) \subseteq \Sv_2$.
Then $\S(N)$ is mutually independent of $\Sv_2\setminus\S(N)$ under $\Sv_1$.
\end{corollary}
\begin{proof}
Let $A \in \S(N)$, $Y \in \Sv_2\setminus\S(N)$.
$A$ and $Y$ are independent under $\B(N)$, by the preceding lemma.
Since $\B(N) \subseteq \Sv_1$, $A$ and $Y$ are independent under $\Sv_1$.
Every subgoal of $\S(N)$ is independent of every subgoal of $\Sv_2\setminus\S(N)$
under $\Sv_1$; therefore, $\S(N)$ and $\Sv_2\setminus\S(N)$ are
mutually independent under $\Sv_1$. 
\hfill $\Box$
\end{proof}









% ;;;;;;;;;;;;;;;  A L G O R I T H M   ---   S K E L E T O N  ;;;;;;;;;;;;;;;;;;;

\subsection{Valid Orderings in Divisibility Trees}
\label{sec:valid-orderings}

The aim of our ordering algorithm is to find a minimal ordering of a given set
of subgoals.
We construct orderings following a divide-and-conquer policy:
larger sets are split into smaller ones, and orderings of the 
smaller sets are combined to produce an ordering of the larger set.
To implement this policy, we perform a post-order traversal of the 
\TREE\ corresponding to the given set of subgoals under an empty
initial binding set. 
When orderings of child nodes are combined to produce an ordering of the
parent node, the inner order of their subgoals is not changed:
smaller orderings are {\em consistent} with larger orderings.

\bigskip

\begin{definition}
Let $\S$ and $\G \subseteq \S$ be sets of subgoals.
An ordering $\Ov_G$ of $\G$ and an ordering $\Ov_S$ of $\S$ are {\em consistent}
(denoted $Cons(\Ov_G, \Ov_S)$),
if the order of subgoals of $\G$ in $\Ov_G$ and in $\Ov_S$ is the same.
\end{definition}

\bigskip

The divide-and-conquer process described above seems analogous to
Merge Sort \cite{knuth:73:vol3}.
There, the set of numbers is split into two (or more)
subsets, each subset is independently ordered to a sequence consistent
with the global order, and these sequences are merged.
Is it possible to use a similar method for subgoal ordering?
Assume that a set of subgoals is partitioned into two mutually independent
subsets, $\A$ and $\B$.  Can we build an algorithm that,
given $\A$, produces its ordering consistent with a minimal
ordering of $\A \cup \B$, independently of $\B$?
Unfortunately, the answer is negative.  
An ordering of $\A$ may be consistent with a minimal ordering of $\A \cup \B_1$ 
but at the  same time not be consistent with a minimal ordering of $\A \cup \B_2$ 
for some $\B_1 \neq \B_2$.

\begin{figure}[bt]
\begin{center}
\fbox{
\begin{minipage}{\textwidth}
\begin{center}

\noindent
{\small
\begin{minipage}[m]{1.8in}
\noindent
The program:\\
\fbox{
\smallskip
\begin{minipage}{2in}
\begin{tabbing}
{\tt a1(c1).} \hspace{5mm} \= {\tt b} $\leftarrow$ {\tt a1(X).}\\
{\tt a1(c1).}              \> {\tt b} $\leftarrow$ {\tt d.}\\
{\tt a2(c1).}              \> {\tt d.}\\
{\tt a2(c1).} \\
{\tt a2(c2)} $\leftarrow$ {\tt a1(c2).}
\end{tabbing}
\end{minipage}
\smallskip
} %fbox
\end{minipage}
\begin{minipage}[m]{3.8in}
\noindent
The control values:\\ \ \\
\begin{tabular}{l|cccccc} 
      & {\small $a1(X)|_{\emptyset}\!\!$} & {\small $a1(X)|_{\{a2(X)\}}\!\!\!\!$} & 
        {\small $a2(X)|_{\emptyset}\!\!$} & {\small $a2(X)|_{\{a1(X)\}}\!\!\!\!$} & 
        {\small $b$} & {\small $d$}\\ \hline
\cost  &  2 & 2 & 5 & 3 & 5 & 1 \\ 
\nsols &  2 & 2 & 2 & 2 & 3 & 1 \\
\end{tabular}
\end{minipage}

\smallskip
\begin{minipage}[m]{2.9in}
\(
\begin{array}{l}
Cost(b, a1(X), a2(X))  =  5 + 3\!\cdot\!2 + 3\!\cdot\!2\!\cdot\!3 = 29 \\ 
Cost(b, a2(X), a1(X))  =  5 + 3\!\cdot\!5 + 3\!\cdot\!2\!\cdot\!2 = 32 \\
Cost(a1(X), b, a2(X))  =  2 + 2\!\cdot\!5 + 2\!\cdot\!3\!\cdot\!3 = 30 \\
Cost(a1(X), a2(X), b)  =  2 + 2\!\cdot\!3 + 2\!\cdot\!2\!\cdot\!5 = 28 \\
Cost(\underline{a2}(X), b, \underline{a1}(X))  =  5 + 2\!\cdot\!5 + 2\!\cdot\!3\!\cdot\!2 = \mbox{\bf 27} \\
Cost(a2(X), a1(X), b)  =  5 + 2\!\cdot\!2 + 2\!\cdot\!2\!\cdot\!5 = 29 
\end{array}
\)
\end{minipage}
\begin{minipage}[m]{2.9in}
\(
\begin{array}{l}
Cost(d, \underline{a1}(X), \underline{a2}(X))  =  1 + 1\!\cdot\!2 + 1\!\cdot\!2\!\cdot\!3 =  \mbox{\bf 9} \\ 
Cost(d, a2(X), a1(X))  =  1 + 1\!\cdot\!5 + 1\!\cdot\!2\!\cdot\!2 = 10 \\
Cost(a1(X), d, a2(X))  =  2 + 2\!\cdot\!1 + 2\!\cdot\!1\!\cdot\!3 = 10 \\
Cost(a1(X), a2(X), d)  =  2 + 2\!\cdot\!3 + 2\!\cdot\!2\!\cdot\!1 = 12 \\
Cost(a2(X), d, a1(X))  =  5 + 2\!\cdot\!1 + 2\!\cdot\!1\!\cdot\!2 = 11 \\
Cost(a2(X), a1(X), d)  =  5 + 2\!\cdot\!2 + 2\!\cdot\!2\!\cdot\!1 = 13 
\end{array}
\)
\end{minipage}
}
\end{center}
\end{minipage}
} % fbox
\caption{\label{fig:ex-not-simple-merging}
{\small 
We show a small program and the control values it defines.
Then we compute costs of all permutations of the sets 
$\{b, a1(X), a2(X)\}$ and $\{d, a1(X), a2(X)\}$.
Different orderings of $\{a1(X), a2(X)\}$ are consistent with minimal
orderings of these sets.
}}
\end{center}  
\end{figure} 

For example, let $\A = \{a1(X), a2(X)\}$, $\B_1 = \{b\}$, $\B_2 = \{d\}$
and the control values be as specified in Figure~\ref{fig:ex-not-simple-merging}. 
The single minimal ordering of $\A \cup \B_1$ is $\la a2(X), b, a1(X) \ra$,
while the single minimal ordering of $\A \cup \B_2$ is $\la d, a1(X), a2(X) \ra$.
There is no ordering of $\A$ consistent with both these minimal global orderings.


Since, unlike the case of Merge Sort, we cannot always identify a
single  ordering of the subset consistent with a  minimal ordering of
the whole set, our algorithm will deal with {\em sets of candidate
orderings}. 
Our requirement from such a set is that it contain at least
one local ordering consistent with a global minimal ordering, 
if such a local ordering exists
(``local'' ordering is an ordering of the set of the node,
``global'' ordering is an ordering of the set of the root). 
Such a set will be called {\em valid}.
The following definition defines valid sets formally, 
together with several other concepts.

\medskip

\begin{definition}
Let $\S_0$ be a set of subgoals and $N$ be a node in the \TREE\ of $\S_0$.
Recall that $\pi(\S)$ denotes the set of all permutations of $\S$.
\begin{enumerate}
\item
$\Ov_S \in \pi(\S_0)$ is {\em binder-consistent} with $\Ov_N \in \pi(\S(N))$ 
(denoted $BC_N(\Ov_N,\Ov_S)$),
if they are consistent, and
all subgoals of $\B(N)$ appear in $\Ov_S$ before all subgoals of $\Ov_N$:
\[ BC_N(\Ov_N,\Ov_S) \iff \exists \Ov_B \in \pi(\B(N)) : 
   Cons(\Ov_B \cc \Ov_N,\Ov_S). \]
$\Ov_S \in \pi(\S_0)$ is {\em binder-consistent} with the node $N$ 
(denoted $BC_N(\Ov_S)$),
if it is binder-consistent with some ordering of $\S(N)$:
\[ BC_N(\Ov_S) \iff \exists \Ov_N \in \pi(\S(N)) : 
   BC_N(\Ov_N,\Ov_S). \]

\item
$\Ov_N \in \pi(\S(N))$ is {\em min-consistent} with $\Ov_S \in \pi(\S_0)$
(denoted $MC_{N,\S_0}(\Ov_N,\Ov_S)$),
if they are binder-consistent, and $\Ov_S$ is minimal:
\[ MC_{N,\S_0}(\Ov_N,\Ov_S) \iff BC_N(\Ov_N,\Ov_S) \wedge 
   Min(\Ov_S,\S_0). \]
$\Ov_N \in \pi(\S(N))$ is {\em min-consistent}
(denoted $MC_{N,\S_0}(\Ov_N)$),
if it is min-consistent with some ordering of $\S_0$:
\[ MC_{N,\S_0}(\Ov_N) \iff \exists \Ov_S \in \pi(\S_0) : 
   MC_{N,\S_0}(\Ov_N,\Ov_S).\]

\item
An ordering $\Ov_N \in \pi(\S(N))$ is {\em MC-contradicting}, if it is not 
min-consistent:
\[ \mbox{MCC}_{N,\S_0}(\Ov_N) \iff \neg MC_{N,\S_0}(\Ov_N). \]

\item
Two orderings $\Ov_1, \Ov_2 \in \pi(\S(N))$ are {\em MC-equivalent},
if one of them is min-consistent iff the other one is:
\[ \mbox{MCE}_{N,\S_0}(\Ov_1, \Ov_2) \iff [ MC_{N,\S_0}(\Ov_1) \iff 
   MC_{N,\S_0}(\Ov_2) ]. \]

\item
A set of orderings $\C_N \subseteq \pi(\S(N))$ is {\em valid},
if $\C_N$ contains a min-consistent ordering
(when at least one min-consistent ordering of $\S(N)$ exists):
\[ Valid_{N,\S_0}(\C_N) \iff [\exists \Ov'_N \in \pi(\S(N)) : 
   MC_{N,\S_0}(\Ov'_N)] \rightarrow
   [\exists \Ov_N \in \C_N : MC_{N,\S_0}(\Ov_N)]. \]
\end{enumerate}
\end{definition}

An important property of valid sets is that a valid set of orderings
of the root of  
$DTree(\S_0,\emptyset)$ must contain a minimal ordering of $\S_0$.
Indeed, in the root $\S(N) = \S_0$, and consistency becomes identity.
Also, $\B(N) = \emptyset$, so that binder-consistency becomes consistency,
and min-consistency becomes minimality.
Since there always exists a minimal ordering of $\S_0$,
a valid set of orderings of the root must contain a minimal ordering
of $\S_0$. 



 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{The Outline of the Divide-and-Conquer Algorithm}
\label{sec:algorithm-outline}

We propose an algorithm that is based on producing valid sets of orderings.
Each node in a \TREE\ produces a valid set for its associated set of subgoals,
and passes it to its parent node.
After the valid set of the root node is found, 
we compare costs of all its members, and return the cheapest one.

The set of orderings produced by the algorithm for a node $N$
is called a {\em candidate set} of $N$.
Its members are called {\em candidate orderings} of $N$, or simply {\em candidates}.
To find a candidate set of $N$, 
we first  consider  the set of all possible orderings of $\S(N)$
that are consistent with candidates of $N$'s children.
This set is called the {\em consistency set} of $N$.
Given the candidate sets of $N$'s children, the consistency set of $N$ is defined
uniquely.
A candidate set of $N$ is usually not unique.

\medskip

\begin{definition}
Let $N$ be a node in a \TREE\ of $\S_0$. 
The {\em consistency set} of $N$,
denoted $ConsSet(N)$, and the {\em candidate set} of $N$,
denoted $CandSet(N)$, are defined recursively:
\begin{itemize}
\item
If $N$ is a leaf, its consistency set contains all permutations of $\S(N)$:
\[ ConsSet(N) = \pi(\S(N)). \]
\item
If $N$ is an AND-node, and its child nodes are $N_1,N_2,\ldots N_k$,
we define the consistency set of $N$ as the set of all possible 
orderings of $\S(N)$ consistent with candidates of $N_1,N_2,\ldots N_k$:
\[ ConsSet(N) = \left\{ \Ov_N \in \pi(\S(N)) \ \left| \ 
  \forall i\ (1 \leq i \leq k),\ \exists \Ov_i \in CandSet(N_i) : Cons(\Ov_i,\Ov_N) 
  \right. \right\}.\]
\item
If $N$ is an OR-node, and its child node corresponding to every binder 
$A \in \S(N)$ is $N_A$,
then the consistency set of $N$ is obtained by adding binders as
the first elements to the candidates of the children:
\[ ConsSet(N) = \left\{ A \cc \Ov_A \ \left| \ A \in \S(N),\ \Ov_A \in CandSet(N_A) 
    \right. \right\}. \]

\item
A candidate set of $N$ is any set of orderings produced by removing 
MC-contradicting and MC-equivalent orderings out of the consistency set of $N$,
while keeping at least one representative for each group of MC-equivalent 
orderings:
\begin{eqnarray*}
CandSet(N) \subseteq ConsSet(N),\\
\Ov_N \in (ConsSet(N) \setminus CandSet(N)) &\Rightarrow&
   \mbox{MCC}_{N,\S_0}(\Ov_N)\ \vee \\ 
 & &  \left[ \exists \Ov'_N \in CandSet(N) :\ 
      \mbox{MCE}_{N,\S_0}(\Ov_N, \Ov'_N) \right].
\end{eqnarray*}
(In other words, if some ordering is rejected, it is either MC-contradicting,
or MC-equivalent to some other ordering, which is not rejected.)
\end{itemize}
\end{definition}

There are two kinds of orderings which can be removed from
$ConsSet(N)$ while retaining its validity: {\em MC-contradicting} and
{\em MC-equivalent} orderings.
Removal of an MC-contradicting ordering cannot change the number of
min-consistent orderings in the set;
if we remove an MC-equivalent ordering, then even if it is min-consistent,
some other min-consistent ordering is retained in the set.
If there exists a min-consistent ordering of the set of the node, then
its candidate set must contain a min-consistent ordering, and therefore
the candidate set is valid.

Note that when our algorithm treats an OR-node, the binder of each child
is always placed as the first subgoal of the produced ordering of this node.
On higher levels the inner order of subgoals in the ordering does not change
(consistency is preserved).
Therefore, our algorithm can only produce binder-consistent orderings.
This explains the choice of the names {\em ``binder''} and {\em ``binding set''}:
the subgoals of $\B(N)$ bind some common variables of  $\S(N)$, 
since they stand to the left of them in any global ordering that our algorithm 
produces.
In particular, if $\S(N)$ is independent under $\B(N)$, 
then the subgoals of $\B(N)$ bind all the shared free variables of $\S(N)$.

To implement the {\bf DPart} function, we can use the Union-Find data
structure \cite[Chapter 22]{cormen:91}, where subgoals are elements,
and indivisible sets are groups. 
In the beginning, every subgoal constitutes a group by itself. 
Whenever we discover that two subgoals share a free variable not bound
by subgoals of the binding set, we unite their groups into one. 
To complete the procedure, we need a way to determine which variables
are bound by the given binding set.
Section~\ref{sec:practical-issues} contains a discussion of this
problem and proposes some practical solutions.
Finally, we collect all the indivisible subgoals into a separate group.
These operations can be implemented in $O(n \alpha(n,n))$ amortized time,
where $\alpha(n,n)$ is the inverse Ackermann function, which can
be considered $O(1)$ for all values of $n$ that can appear in realistic
logic programs.
Thus, the whole process of finding the divisibility partition of $n$ subgoals
can be performed in $O(n)$ average time.

\begin{figure}[t]
\begin{center}
\fbox{
\begin{minipage}{0.9\textwidth}
\begin{center}
\begin{minipage}{0.85\textwidth}

\ \medskip
\begin{algorithm}
\ 
\label{alg:ordering-algorithm-skeleton}
\end{algorithm}

\begin{tabbing}
\TABLINE{5mm}
{\bf Order}$(\S_0)$  \\
\>  $RootCandSet$ $\leftarrow$ {\bf CandidateSet}$(\S_0, \emptyset)$\\
\>  Return the cheapest member of $RootCandSet$
\end{tabbing}


\begin{tabbing}
\TABLINE{5mm}
{\bf CandidateSet}$(\S, \B)$\\
\>  case ($\S$ under $\B$) \\
\>  \underline{independent}: \\
\>  \>  \>  let {\em ConsSet}$_N$ $\leftarrow$ $\pi(\S)$ \\
\>  \>  \>  let {\em CandSet}$_N$ $\leftarrow$ {\bf ValidLeafFilter}({\em ConsSet}$_N$)\\
\>  \underline{divisible}:  \\
\>  \>  \>  let $\{\S_1,\S_2,\ldots\S_k\} \leftarrow \mbox{\bf DPart}(\S,\B)$ \\
\>  \>  \>  loop for $i = 1$ to $k$ \\
\>  \>  \>  \>  let $\C_i \leftarrow$ {\bf CandidateSet}$(\S_i, \B)$\\
\>  \>  \>  let {\em ConsSet}$_N$ $\leftarrow$ 
                $\left\{ \Ov_N \in \pi(\S(N)) \ | \ 
          \forall i=1 \ldots k,\ \exists \Ov_i \in \C_i : 
                Cons(\Ov_i,\Ov_N) \right\}$ \\
\>  \>  \>  let {\em CandSet}$_N$ $\leftarrow$ 
    {\bf ValidANDFilter}($\mbox{\em ConsSet}_N,\{\S_1,\ldots\S_k\},\{\C_1,\ldots\C_k\}$)\\
\>  \underline{indivisible}: \\
\>  \>  \>  loop for $A \in \S$ \\
\>  \>  \>  \>  let $\C(A) \leftarrow$ 
               {\bf CandidateSet}$(\S\setminus\{A\}, \B\cup\{A\})$\\
\>  \>  \>  \>  let $\C'(A) \leftarrow 
               \left\{ A \cc \Ov_A \ |\ \Ov_A \in \C(A) \right\}$ \\
\>  \>  \>  let {\em ConsSet}$_N$ $\leftarrow$ $\bigcup_{A \in \S} \C'(A)$\\
\>  \>  \>  let {\em CandSet}$_N$ $\leftarrow$ {\bf ValidORFilter}({\em ConsSet}$_N$)\\
\>  Return {\em CandSet}$_N$
\end{tabbing}

\medskip
\end{minipage}
\end{center}
\end{minipage}
} % fbox
\caption{\label{fig:algorithm-skeleton}
{\small 
The skeleton of the \DC\ ordering algorithm.
For each type of node in a \TREE, a consistency set is created and refined 
through validity filters.
The produced candidate set of the root is valid; hence, its cheapest member
is a minimal ordering of the given set.
}}
\end{center}
\end{figure}



The formal listing of the ordering algorithm discussed 
above is shown in Figure~\ref{fig:algorithm-skeleton}.
The algorithm does not specify explicitly how candidate sets
are created from consistency sets.
To complete this algorithm, we must provide the three filtering procedures -- 
\mbox{\bf ValidLeafFilter}, \mbox{\bf ValidANDFilter} and \mbox{\bf ValidORFilter}.
Trivially, we can define them all as null filters that return the 
sets they receive unchanged.
In this case the candidate set of every node will contain all the
permutations of its subgoals, and will surely be valid.
This will, however, greatly increase the ordering time.
Our intention is to reduce the sizes of candidate sets as far as possible,
while keeping them valid.


In the following two subsections we discuss the filtering procedures.
Section~\ref{sec:elimination-contradicting} discusses detection of
MC-contradicting orderings, and
Section~\ref{sec:elimination-equivalent} discusses detection of
MC-equivalent orderings. 
Finally, in Section~\ref{sec:algorithm-complete} we present the complete
ordering algorithm, incorporating the filters into the skeleton of
Algorithm~\ref{alg:ordering-algorithm-skeleton}.




\subsection{Detection of MC-Contradicting Orderings}
\label{sec:elimination-contradicting}

In this subsection we show sufficient conditions for an ordering to be
MC-contradicting.
Such orderings can be safely discarded, leaving the set of orderings valid, 
but reducing its size.
The subsection is divided into three parts, one for each type of node
in a \TREE.



%;;;;;;;;;;;;;;;;;;;;;;;;  INDEPENDENT SET  ;;;;;;;;;;;;;;;;;;;;;;;;;;

\subsubsection{Detection of MC-Contradicting Orderings in Leaves}

The following lemma shows that subgoals in a min-consistent ordering
of a leaf node must be sorted by $cn$.

\begin{lemma}
\label{lemma:contradicting-independent}
\ \\
Let $\S_0$ be a set of subgoals, 
$N$ be a leaf in the \TREE\ of $\S_0$.
Let $\Ov_N$ be an ordering of $\S(N)$.
If the subgoals of $\Ov_N$ are not sorted by $cn$ under $\B(N)$, 
then $\Ov_N$ is MC-contradicting.
\end{lemma}

\begin{proof}
Let $\Ov_S$ be any ordering of $\S_0$, binder-consistent with $\Ov_N$.
We show that $\Ov_S$ cannot be a minimal ordering of $\S_0$, thus
$\Ov_N$ is not min-consistent. 

$\Ov_N$ is not sorted by $cn$, i.e., it contains an adjacent 
cn-inverted pair of subgoals $\la A_1, A_2 \ra$.
(Recall that a pair is cn-inverted if the first element has a larger
$cn$ value than the second one -- Section~\ref{sec:sorting-correctness}).
Since $\Ov_S$ is consistent with $\Ov_N$, we can write
$\Ov_S = \Xv \cc A_1 \cc \Yv \cc A_2 \cc \Zv$,
where $\Xv$, $\Yv$ and $\Zv$ are (possibly empty) sequences of subgoals.
Since $\Ov_S$ is binder-consistent with $\Ov_N$, $\B(N) \subseteq \Xv$.

If $\Yv$ is empty, then $A_1$ and $A_2$ are adjacent in $\Ov_S$.
Since $\B(N) \subseteq \Xv$, $A_1$ and $A_2$ are independent under $\Xv$.
Therefore, the cost 
of the whole ordered sequence can be reduced by transposing $A_1$ and $A_2$, 
according to Lemma~\ref{lemma:independent-adjacent}
(they are adjacent, independent and cn-inverted).

If $\Yv$ is not empty, then no subgoal of $\Yv$ belongs to $\S(N)$, 
since otherwise it would appear in $\Ov_N$ between $A_1$ and $A_2$.
By Corollary~\ref{corollary:interleaving-independent},
$\Yv$ is mutually independent of both $A_1$ and $A_2$ under $\Xv$.

\begin{itemize}
\item 
If $cn(\Yv)|_{\Xv} < cn(A_1)|_{\Xv}$ then, by Lemma~\ref{lemma:independent-adjacent},
a transposition of $\Yv$ with $A_1$ produces an ordering with lower cost.
\item
Otherwise, $cn(\Yv)|_{\Xv} \geq cn(A_1)|_{\Xv}$.
Since the pair $\la A_1, A_2 \ra$ is cn-inverted, $cn(A_1)|_{\Xv} > cn(A_2)|_{\Xv}$.
Hence, $cn(\Yv)|_{\Xv} > cn(A_2)|_{\Xv}$, and transposition of $\Yv$ with
$A_2$ reduces the cost, by Lemma~\ref{lemma:independent-adjacent}.
\end{itemize}
In either case, there is a way to reduce the cost of $\Ov_S$. 
Therefore, $\Ov_S$ cannot be minimal, and $\Ov_N$ is MC-contradicting.
\hfill $\Box$
\end{proof}







\subsubsection{Detection of MC-Contradicting Orderings in AND-nodes}

%;;;;;;;;;;;;;;;;;;;;;;;;;;   D I V I S I B L E    ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Every member of the consistency set of an AND-node 
is consistent with some combination of candidates of its child nodes.
If there are $k$ child nodes, and for each child $N_i$ the sizes
of subgoal and candidate sets are $|\S(N_i)| = n_i$
and $|\mbox{\em CandSet}(N_i)| = c_i$, 
then the total number of possible consistent orderings is
\mbox{$c_1 \cdot c_2 \cdot \ldots c_k \cdot
 \frac{(n_1+n_2+\ldots+n_k)!}{n_1!\cdot n_2!\ldots\cdot n_k!}$}.
Fortunately, most of these orderings are MC-contradicting and can be
discarded from the candidate set.
The following lemma states that it is forbidden to insert other
subgoals between two cn-inverted sub-sequences. 
If such insertion takes place, the ordering is MC-contradicting and
can be safely discarded.

\begin{lemma}
\label{lemma:block}
\ \\
Let $\S_0$ be a set of subgoals, $N$ a node in the \TREE\ of $\S_0$,
and $\Ov_S$ an ordering of $\S_0$, binder-consistent with an
ordering $\Ov_N$ of $\S(N)$.

If $\Ov_N$ contains an adjacent cn-inverted pair of sub-sequences 
$\la\Av_1,\Av_2\ra$,
$\Av_1$ and $\Av_2$ appear in $\Ov_S$ not mixed with other subgoals,
and $\Av_1$ and $\Av_2$ are not adjacent in $\Ov_S$,
then $\Ov_S$ is not minimal.
\end{lemma}

\begin{proof}
Let $\Ov_S$ be such an ordering of $\S_0$, binder-consistent with $\Ov_N$:
\[ \Ov_S = \Xv \cc \Av_1 \cc \Yv \cc \Av_2 \cc \Zv, \]
where $\Yv$ is not empty.
No subgoal of $\Yv$ belongs to $\S(N)$, since otherwise it would stand in $\Ov_N$
between $\Av_1$ and $\Av_2$.
$\Ov_S$ is binder-consistent with $\Ov_N$; therefore, $\B(N) \subseteq \Xv$.
By Corollary~\ref{corollary:interleaving-independent},
$\Yv$ must be mutually independent of both $\Av_1$ and $\Av_2$ under $\Xv$,
and by Lemma~\ref{lemma:independent-adjacent} a transposition of $\Yv$ with
either $\Av_1$ or $\Av_2$ reduces the cost -- exactly as in the proof of  
Lemma~\ref{lemma:contradicting-independent}.
\hfill $\Box$
\end{proof}

\bigskip

If a pair of adjacent subgoals $\la A_i, A_{i+1} \ra$ is cn-inverted,
then by the previous lemma any attempt to insert subgoals inside 
it results in a non-minimal global ordering.
Thereupon we may join $A_i$ and  $A_{i+1}$ into a {\em block} $A_{i,i+1}$, which
can further participate in a larger block. 
The formal recursive definition of a block follows.
For convenience, we consider separate subgoals to be blocks of length~1.

\medskip

\begin{definition} \ 
\begin{enumerate}
\item
A sub-sequence $\Av$ of an ordered sequence of subgoals is a {\em block}
if it is either a single subgoal, or $\Av = \Av_1 \cc \Av_2$,
where $\la\Av_1,\Av_2\ra$ is a cn-inverted pair of blocks.
\item
A block is {\em maximal} ({\em max-block}) if it is not a sub-sequence
 of a larger block.  
\item
Let $N$ be a node in a \TREE, $M$ be some descendant of $N$,
$\Ov_N \in \pi(\S(N))$ and $\Ov_M \in \pi(\S(M))$ be two consistent
orderings of these nodes.
A block $\Av$ of $\Ov_M$ is {\em violated} in $\Ov_N$ if there are two
adjacent subgoals in $\Av$ that are not adjacent in $\Ov_N$
(in other words, alien subgoals are inserted between the subgoals of
the block).
\item
Let $N$ be a node, $M$ be its descendant, 
$\Ov_N \in \pi(\S(N))$ and $\Ov_M \in \pi(\S(M))$ be two consistent
orderings of these nodes.
$\Ov_M$ is called the {\em projection} of $\Ov_N$ on $M$.
We shall usually speak about projection of an ordering on a child node.
\end{enumerate}
\end{definition}

The concept of max-block is similar to the {\em maximal indivisible block}
introduced by \citeA{simon:75} in the context of satisficing search.
The following corollary presents the result of Lemma~\ref{lemma:block}
in a more convenient way.

\begin{corollary}
\label{corollary:block-violated}
Let $N$ be a node in a \TREE, $M$ be one of its children,
$\Ov_N$ be an ordering of $N$, 
and $\Ov_M$ be the projection of $\Ov_N$ on $M$.
If $\Ov_M$ contains a block that is violated in $\Ov_N$,
then $\Ov_N$ is MC-contradicting.
\end{corollary}
\begin{proof}
Let $\Av$ be the smallest block of $\Ov_M$ violated in $\Ov_N$.
According to the definition of a block, $\Av = \Av_1 \cc \Av_2$, where
$\Av_1$ and $\Av_2$ are not violated in $\Ov_N$, and the pair
$\la \Av_1, \Av_2 \ra$ is cn-inverted.
Let $\Ov_S$ be any ordering of the root node binder-consistent with $\Ov_N$.
$\Ov_S$ violates $\Av$, since $\Ov_N$ violates $\Av$.
To show that $\Ov_N$ is MC-contradicting, we must prove that $\Ov_S$ is not minimal.
\begin{itemize}
\item
If $\Av_1$ and $\Av_2$ are not violated in $\Ov_S$,
then they are not adjacent in $\Ov_S$, and
$\Ov_S$ is not minimal, by Lemma~\ref{lemma:block}.
\item
Otherwise, $\Av_1$ or $\Av_2$ is violated in $\Ov_S$.
Without loss of generality, let it be $\Av_1$.
Let $\Av'$ be the smallest sub-block of $\Av_1$ violated in $\Ov_S$.
According to the definition of a block, $\Av' = \Av'_1 \cc \Av'_2$, where
the pair $\la\Av'_1,\Av'_2\ra$ is cn-inverted, 
$\Av_1$ and $\Av_2$ are not violated and not adjacent in $\Ov_S$.
By Lemma~\ref{lemma:block}, $\Ov_S$ is not minimal.
\hfill $\Box$
\end{itemize}
\end{proof}

\smallskip

For example, if control values of subgoals are as shown in 
Figure~\ref{fig:ex-not-simple-merging},
then $\la a1(X),a2(X) \ra$ is a block, since
$\cn(a1(X))|_{\emptyset} = \frac{2-1}{2} = \frac{1}{2}$,
$\cn(a2(X))|_{\{a1(X)\}} = \frac{2-1}{3} = \frac{1}{3}$.
As one can see from the figure, insertion of $b$ or $d$ inside this block 
results in a non-minimal ordering.

As was already noted above, the consistency set of an AND-node can be large.
In many of its orderings, however, blocks of projections are violated, 
and we can discard these orderings as MC-contradicting.
In the remaining orderings, no block of a projection is violated, and
each such ordering can be represented as a sequence of 
max-blocks of the projections.
In each projection, its max-blocks stand in $cn$-ascending order
(otherwise, there is an adjacent cn-inverted pair of blocks, and a 
larger block can be formed, which contradicts their maximality).
As the following lemma states, in the parent AND-node these blocks 
must also be ordered by their $cn$ values; otherwise, the ordering is 
MC-contradicting.


\begin{lemma}
\label{lemma:contradicting-divisible}
If an ordering of an AND-node contains an adjacent cn-inverted pair 
of max-blocks of its projections on the children,
then this ordering is MC-contradicting.
\end{lemma}
\begin{proof}
If these blocks are violated in the binder-consistent global ordering,
the global ordering is not minimal by Corollary~\ref{corollary:block-violated}.
If the blocks are not violated, the proof is similar to the proof of 
Lemma~\ref{lemma:contradicting-independent}.
\hfill $\Box$
\end{proof}

\medskip


The two sufficient conditions for detection of MC-contradicting orderings
expressed in Corollary~\ref{corollary:block-violated} and 
Lemma~\ref{lemma:contradicting-divisible} allow us to reduce the size of
the candidate set significantly.
Assume, for example, that the set of our current node $N$
is split into two mutually independent subsets whose candidates are
$\la a_1,a_2\ra$ and  
$\la b_1,b_2 \ra$ (one candidate for each child).
There are six possible orderings of $\S(N)$, all shown in 
Figure~\ref{fig:merging6}.
Assume that both $\la a_1,a_2\ra$ and $\la b_1,b_2 \ra$ are blocks,
and $cn(\la a_1,a_2\ra)|_{\B(N)} < cn(\la b_1,b_2 \ra)|_{\B(N)}$.
Out of six consistent orderings, four (2--5) can be rejected due to
block violation, and one of the remaining two (number 6) puts the blocks
in the wrong order.
So, only one ordering (number 1) can be left in the candidate set of $N$.
Even if neither $\la a_1,a_2\ra$ nor $\la b_1,b_2 \ra$ are blocks,
Lemma~\ref{lemma:contradicting-divisible} dictates a unique
interleaving of their elements (max-blocks), assuming that 
$cn(a_1)|_{\B(N)}$ $\neq$ $cn(a_2)|_{\B(N) \cup \{a_1\}}$ $\neq$ 
$cn(b_1)|_{\B(N)}$ $\neq$ $cn(b_2)|_{\B(N) \cup \{b_1\}}$.


\begin{figure}
\begin{center}
\fbox{
\begin{minipage}{0.9\textwidth}

\begin{center}
\epsfig{figure=figs/pictures/merging6.eps,width=5.5in}
\end{center}

\end{minipage}
} % fbox
\caption{\label{fig:merging6}
{\small 
The possible ways to combine $\langle$a$_1$, a$_2\rangle$ 
and $\langle$b$_1$, b$_2\rangle$
}}
\end{center}  
\end{figure}




% ;;;;;;;;;;;;;;;;;;;;;  INDIVISIBLE ;;;;;;;;;;;;;;;;;;;;;;;;;;;

\subsubsection{Detection of MC-Contradicting Orderings in OR-nodes}
\label{sec:contradicting-indivisible}

The following lemma states that if a block has a cheaper permutation,
then the ordering is MC-contradicting (and can be discarded from the
candidate set).

\begin{lemma}
\label{lemma:contradicting-indivisible}
Let $N$ be a node in the \TREE\ of $\Sv_0$, $\Ov_N \in \pi(\Sv(N))$.
Let $\Av$ be a leading block of $\Ov_N$: $\Ov_N = \Av \cc \Rv$.
If there is a permutation of $\Av$, $\Av'$, 
such that $\cost(\Av')|_{\B(N)} < \cost(\Av)|_{\B(N)}$,
then $\Ov_N$ is MC-contradicting.
\end{lemma}
\begin{proof}
Let $\Ov_S \in \pi(\Sv_0)$ be binder-consistent with $\Ov_N$.
If $\Av$ is violated in $\Ov_S$, $\Ov_S$ cannot be minimal
(Corollary~\ref{corollary:block-violated}).
Otherwise, $\Av$ occupies a continuous segment in $\Ov_S$, and
its replacement by a cheaper permutation reduces the cost of the
global ordering (Lemma~\ref{lemma:cheaper-permutation}). 
Thus, $\Ov_S$ cannot be minimal. 
\hfill $\Box$
\end{proof}

\medskip

This check should be done only for leading blocks of OR-nodes:
\begin{itemize}
\item
Every ordering of a leaf node that has not been rejected due to
Lemma~\ref{lemma:contradicting-independent} must be sorted by $cn$.
Consequently, it contains no cn-inverted adjacent pair of subgoals,
and no block of size $\geq$ 2 can be formed. 
\item
Every ordering of an AND-node that has not been rejected due to
Corollary~\ref{corollary:block-violated} 
or Lemma~\ref{lemma:contradicting-divisible}
must have its blocks  unbroken and in cn-ascending order.
Consequently, new blocks cannot be formed here either.
\item
In OR-nodes, new blocks can be formed when we add a binder as the first
element of an ordering, if the $cn$ value of the binder is greater than
that of the subsequent block.
All new blocks start from the binder, and we must 
perform the permutation test only on the leading max-block of an ordering.
\end{itemize}
 






%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\subsection{Detection of MC-Equivalent Orderings}
\label{sec:elimination-equivalent}

In the previous subsection we presented sufficient conditions for detecting
MC-contradicting orderings.
In this subsection we specify sufficient conditions for identifying MC-equivalent
orderings. 
Recall that two orderings of a node are MC-equivalent if minimal consistency
of one implies minimal consistency of the other.
Finding such sufficient conditions will allow us to
eliminate orderings without loss of validity of the candidate set.
We start with defining a specialization of the MC-equivalence relation:
{\em blockwise equivalence}.
We then show that orderings whose max-blocks are sorted by $cn$ are
blockwise-equivalent, and therefore MC-equivalent.

\medskip

\begin{definition}
Let $\S_0$ be a set of subgoals and
$N$ be a node in the \TREE\ of $\S_0$.
Let $\Ov_1$ and $\Ov_2$ be two orderings of $\S(N)$ with an
equal number of max-blocks.
Let $\Ov_S$ be an ordering of $\S_0$, binder-consistent with $\Ov_1$,
where blocks of $\Ov_1$ are not violated.

$\Ov_S|_{\Ov_1}^{\Ov_2}$ is the
ordering  obtained by replacing in $\Ov_S$ every max-block 
of $\Ov_1$ with a max-block of $\Ov_2$, while preserving the order of
max-blocks (the $i$-th max-block of $\Ov_1$ is replaced by the 
$i$-th max-block of $\Ov_2$).

$\Ov_1$ and $\Ov_2$ are {\em blockwise-equivalent} if the following
condition holds:
$\Ov_1$ is min-consistent with $\Ov_S$ iff
$\Ov_2$ is min-consistent with $\Ov_S|_{\Ov_1}^{\Ov_2}$.

\end{definition}

\medskip

As can be easily seen, if two orderings are blockwise-equivalent, then
they are MC-equivalent.
Now we show that a transposition of adjacent, mutually independent cn-equal 
max-blocks in an ordering of a node  produces a blockwise-equivalent ordering.
The proof of the following lemma is found in Appendix~\ref{sec:app:proofs}.

\begin{lemma}
\label{lemma:transposition-blocks-equivalent}
\ \\
Let $\S_0$ be a set of subgoals,
$N$ be a node in the \TREE\ of $\S_0$,
$\Ov_N = \Qv \cc \Av_1 \cc \Av_2 \cc \Rv$ be an ordering of $\S(N)$,
where $\Av_1$ and $\Av_2$ are max-blocks, 
mutually independent and cn-equal under the bindings of $\B(N) \cup \Qv$.
Then $\Ov_N$ is blockwise-equivalent with 
$\Ov'_N = \Qv \cc \Av_2 \cc \Av_1 \cc \Rv$.
\end{lemma}

\begin{corollary} 
\label{corollary:independent-sorted-are-equivalent}
All sorted by $cn$ orderings of a leaf node are blockwise-equivalent.
\end{corollary}

For example, if $\S(N) = \{A,B,C,D\}$, 
$cn(A)|_{\B(N)}=0.1$, $cn(B)|_{\B(N)}=cn(C)|_{\B(N)}=0.3$, $cn(D)|_{\B(N)}=0.5$, 
then the orderings $\la A,B,C,D\ra$ and $\la A,C,B,D\ra$ are blockwise-equivalent,
and we can remove from the candidate set any one of them (but not both).

\begin{corollary} 
\label{corollary:divisible-sorted-are-equivalent}
All orderings of an AND-node,
where blocks of projections are not violated and
adjacent max-blocks from different children projections are cn-ordered,
are blockwise-equivalent.
\end{corollary}

For example, if the candidates of the children are $\Av\cc\Bv$ and 
$\Cv\cc\Dv$, where $\Av,\Bv,\Cv,\Dv$ are max-blocks, $cn(\Av)|_{\B(N)}=0.1$, 
$cn(\Bv)|_{\B(N)\cup\Av}=cn(\Cv)|_{\B(N)}=0.3$ and
$cn(\Dv)|_{\B(N)\cup\Cv}=0.5$, then the orderings
$\Av\cc\Bv\cc\Cv\cc\Dv$ and $\Av\cc\Cv\cc\Bv\cc\Dv$ are blockwise-equivalent,
and we can remove from the candidate set any one of them (but not both).


To prove both Corollaries~\ref{corollary:independent-sorted-are-equivalent}
and~\ref{corollary:divisible-sorted-are-equivalent}, we note that in each case 
one of the mentioned orderings can be obtained from the other by a finite number
of transpositions of adjacent, mutually independent and cn-equal max-blocks.
According to Lemma~\ref{lemma:transposition-blocks-equivalent},
each such transposition yields a blockwise-equivalent ordering.
It is easy to show that blockwise equivalence is transitive.

The following corollary states that subgoals within a block can be
permuted, provided that the cost of the block is not changed.

\begin{corollary} 
\label{corollary:indivisible-perm-blocks-are-equivalent}
All orderings of a node,
identical up to cost-preserving permutations of subgoals inside blocks,
are blockwise-equivalent.
\end{corollary}

The proof of the corollary follows immediately from 
Lemma~\ref{lemma:cheaper-permutation}.
For example, if the set is $\{a(X),b(X)\}$, and the control values are as
in the first counter-example of Proposition~\ref{prop:cannot-sort-dependent}, i.e.
$cn(a(X)|_{\emptyset}) = cn(b(X)|_{\emptyset}) = \frac{1}{2}$,
and $cn(a(X)|_{\{b(X)\}}) = cn(b(X)|_{\{a(X)\}}) = 0$, 
then in both possible orderings, $\la a(X), b(X) \ra$ and $\la b(X), a(X) \ra$,
the two subgoals are united into a block, and these blocks have equal cost.
In any global ordering containing the block $\la a(X), b(X) \ra$,
we can replace this block with $\la b(X), a(X) \ra$ without changing
the total cost. 
Therefore $\la a(X), b(X) \ra$ is blockwise-equivalent to $\la b(X), a(X) \ra$.

The sufficient condition expressed in 
Corollary~\ref{corollary:indivisible-perm-blocks-are-equivalent}
should be checked only in OR-nodes, since in leaves and
AND-nodes no new blocks are created, as was argued in
Section~\ref{sec:contradicting-indivisible}.






% ;;;;;;;;;;;;;;;   A L G O R I T H M   --   U P D A T E D ;;;;;;;;;;;;;;;;;;;;

\subsection{The Revised Ordering Algorithm}
\label{sec:algorithm-complete}


In the two preceding subsections we saw several sufficient conditions
of MC-contradiction and MC-equivalence, summarized 
in Table~\ref{table:sufficient-conditions}.
These results permit us to close the
gaps in Algorithm~\ref{alg:ordering-algorithm-skeleton}
by providing the necessary validity filters.
Each filter tests the sufficient conditions of MC-contradiction and
MC-equivalence on every ordering in the consistency set.
If some of these sufficient conditions hold, the ordering is rejected.
The formal listing of these procedures is shown in 
Figure~\ref{fig:validity-filters}.

\begin{table}[t]
\begin{center}
\begin{tabular}{|l|l|l|l|}
\hline
Node & Set  & MC-contradicting & blockwise-equivalent \\
\hline
Leaf & Independent & Subgoals not sorted by $cn$  & Subgoals sorted by $cn$     \\
     &             & {\em --- Lemma~\ref{lemma:contradicting-independent}} & {\em --- Corollary~\ref{corollary:independent-sorted-are-equivalent}} \\
\hline
     &             & Contains violated blocks  &   Max-blocks not violated, \\
AND  & Divisible   & {\em --- Corollary~\ref{corollary:block-violated}} & sorted by $cn$   \\  
     &             & Max-blocks not sorted by $cn$ & {\em --- Corollary~\ref{corollary:divisible-sorted-are-equivalent}}   \\
     &             & {\em --- Lemma~\ref{lemma:contradicting-divisible}}  &   \\
\hline
     &             & The leading max-block has    & Cost-preserving permutations \\
OR   & Indivisible & a cheaper permutation        & of blocks     \\
     &             & {\em --- Lemma~\ref{lemma:contradicting-indivisible}}  & {\em --- Corollary~\ref{corollary:indivisible-perm-blocks-are-equivalent}}     \\
\hline
\end{tabular}
\caption{\label{table:sufficient-conditions}
\small 
Summary of sufficient conditions for detection of MC-contradicting and
blockwise-equivalent orderings.
}
\end{center}
\end{table}



\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{\textwidth}
\begin{tabbing}
\TABLINE{5mm}
\\
{\bf ValidLeafFilter}($\mbox{\em ConsSet}_N$)\\
\>  let {\em CandSet}$_N \leftarrow \emptyset$ \\
\>  loop for $\Ov_N \in \mbox{\em ConsSet}_N$ \\
\>  \>  if $\Ov_N$ is sorted by $cn$ \\
\>  \>  and there is no $\Ov'_N \in \mbox{\em CandSet}_N$ which is sorted by $cn$ \\
\>  \>  then $\mbox{\em CandSet}_N \leftarrow \mbox{\em CandSet}_N \cup \{\Ov_N\}$\\
\>  Return $\mbox{\em CandSet}_N $\\
\\
{\bf ValidANDFilter}($\mbox{\em ConsSet}_N,\{\S_1,\ldots \S_k\},\{\C_1,\ldots \C_k\}$)\\
\>  let {\em CandSet}$_N \leftarrow \emptyset$ \\
\>  loop for $\Ov_N \in \mbox{\em ConsSet}_N$ \\
\>  \>  loop for $i = 1$ to $k$\\
\>  \>  \>  let $\Ov_i$ be the projection of $\Ov_N$ on $\S_i$\\
\>  \>  if $\forall i$ $\Ov_i \in \C_i$\\
\>  \>  and max-blocks of $\Ov_i$-s are not violated in $\Ov_N$,\\
\>  \>  and max-blocks of $\Ov_i$-s are ordered by $cn$ in $\Ov_N$,\\
\>  \>  and there is no $\Ov'_N \in \mbox{\em CandSet}_N$ consistent with 
            all $\Ov_i$-s,\\
\>  \>  then $\mbox{\em CandSet}_N \leftarrow \mbox{\em CandSet}_N \cup \{\Ov_N\}$\\
\>  Return $\mbox{\em CandSet}_N $\\
\\
{\bf ValidORFilter}({\em ConsSet}$_N$)\\
\>  let {\em CandSet}$_N \leftarrow \emptyset$ \\
\>  loop for $\Ov_N \in \mbox{\em ConsSet}_N$ \\
\>  \>  if $\Ov_N$ does not start with a block having a cheaper permutation,\\
\>  \>  and there is no $\Ov'_N \in \mbox{\em CandSet}_N$, 
        identical to $\Ov_N$ up to \\
\>  \>  \>  \> cost-preserving permutations in blocks,\\
\>  \>  then $\mbox{\em CandSet}_N \leftarrow \mbox{\em CandSet}_N \cup \{\Ov_N\}$\\
\>  Return $\mbox{\em CandSet}_N $\\
\end{tabbing}
\end{minipage}
} % fbox
\caption{\label{fig:validity-filters}
{\small 
The three filter procedures that convert a consistency set into a candidate set.
Together with Algorithm~\protect\ref{alg:ordering-algorithm-skeleton},
they form a complete ordering algorithm.
The efficiency of the algorithm can be improved, as we shall see in
Algorithm~\protect\ref{alg:ordering-algorithm}.
}}
\end{center}  
\end{figure}


While the generate-and-test approach described above served us well for 
methodological purposes, it is obviously not practical because of its
computational limitations.
For example, for an independent set of size $n$, the algorithm creates
$n!$ orderings, then rejects $n!-1$ and keeps only one.  
This process takes $O(n! \cdot n)$ time and produces an ordering
which is sorted by $cn$.
The same result could be obtained in just $O(n \log n)$ time, by a
single sorting.
So, instead of uncontrolled creation of orderings and selective 
rejection, we want to perform a selective creation of orderings.
In other words, we want to revise our algorithm to deal directly with
candidate sets, instead of generating large consistency sets.
The revised algorithm produces the candidate set of a node $N$ as follows:
\begin{itemize}
\item
If $N$ is a leaf,
the subgoals of $\S(N)$ are sorted by $cn$ under the bindings of 
$\B(N)$, and the produced ordering is the sole candidate of $N$.

\item
If $N$ is an AND-node,
then for each combination of its children's candidates
a candidate of $N$ is created, where the max-blocks of the 
children's candidates are ordered by $cn$.
The candidate is produced by merging:
moving in parallel on the candidates of the children and 
extracting max-blocks that are minimal by $cn$.

\item
If $N$ is an OR-node,
then for each candidate of its child an ordering of $N$ is created by
adding the binder to the left end of the child candidate.
If this results in creation of a block that has a cheaper permutation,
the ordering is rejected; otherwise, it is added to the candidate set.
It suffices to check only the leading max-block.
\end{itemize}

Note that the revised algorithm does not include a test for cost-preserving 
permutations of blocks in different orderings (expressed in
Corollary~\ref{corollary:indivisible-perm-blocks-are-equivalent}),
because of the high expense of such a test.

The revised algorithm described above contains manipulations of blocks.
For this purpose, we need an easy and efficient way to detect blocks in orderings.
Since we do not permit block violation (by 
Corollary~\ref{corollary:block-violated}), we can unite all the subgoals of a 
max-block into one entity, and treat it as an ordinary subgoal.
The procedure of joining subgoals into blocks is called {\em folding},
and the resulting sequence of max-blocks -- a {\em folded sequence}.
After subgoals are folded into a block, there is no need to unfold this block
back to separate subgoals: on upper levels of the tree, these subgoals
will again be joined into a block, unless the block is violated.
The unfolding operation is carried out only once
before returning the cheapest ordering of the set (of the root node).
The candidate sets of the nodes are now defined as sets of {\em folded} orderings.

As was already stated, 
new blocks can only be created in the candidates of OR-nodes, 
when the binder is added as the first element of the ordering,
if the $cn$ value of the binder is greater than the $cn$ value of the
first max-block of the child projection.
Therefore, in the revised algorithm we only build new blocks that start from 
the binder:
the max-blocks in the rest of the ordering remain from the child's candidate.
First we try to make a block out of the binder and the first max-block of the
child's candidate. If they are cn-ordered, we stop the folding.
If they are cn-inverted, we unite them into a larger block, and 
try to unite it with the second max-block of the child's candidate, and so on.
The produced folded ordering contains only maximal blocks:
the first block is maximal, since we could not expand it further to the right,
and the other blocks are maximal, since they were maximal in the child's
candidate.

Lemma~\ref{lemma:contradicting-indivisible} states that an ordering whose leading
max-block has a cheaper permutation is MC-contradicting.
One way to detect such a block is to exhaustively test all its
permutations, computing and comparing their costs.
This procedure is very expensive.
Instead, in our revised algorithm we employ the adjacency restriction test
(Equation~\ref{eq:adjacency-restriction}).
The test is applied to every pair of adjacent subgoals of a block, and
if some adjacent pair has a cheaper transposition, then the whole block
has a cheaper permutation, by Lemma~\ref{lemma:cheaper-permutation}.
Since blocks are created by concatenation of smaller blocks, 
it suffices to test the adjacency restriction only at the points where
blocks are joined (for other adjacent pairs of subgoals, the tests
were performed on the lower levels, when smaller blocks were formed).
The adjacency restriction test does not guarantee detection of all
not-cheapest permutations (as was shown in
Example~\ref{ex:adjacency-restriction}), but it detects such blocks in
many cases, and works in linear time. 

The final version of the \DC\ subgoal ordering algorithm is presented in
Figure~\ref{fig:algorithm-complete}.
The complete correctness proof of Algorithm~\ref{alg:ordering-algorithm} 
is found in Appendix~\ref{sec:app:correctness-proof}.



\begin{figure}
\begin{center}
\fbox{
\begin{minipage}{0.9\textwidth}

\medskip
\begin{algorithm}: The Divide-and-Conquer Algorithm
\label{alg:ordering-algorithm}
\end{algorithm}


\begin{tabbing}
\TABLINE{5mm}
{\bf Order}$(\S_0)$  \\
\>  let {\em RootCandSet} $\leftarrow$ {\bf CandidateSet}$(\S_0, \emptyset)$\\
\>  Return {\bf Unfold}(the cheapest element of {\em RootCandSet})
\end{tabbing}


\begin{tabbing}
\TABLINE{5mm}
{\bf CandidateSet}$(\S, \B)$\\
\>  let $\{\S_1,\S_2,\ldots \S_k\} \leftarrow$ {\bf DPart}$(\S,\B)$ \\
\>  case \\ 
\>  \> $\bullet$ $k=1$, {\em shared-vars}$(\S_1) = \emptyset$ ($\S$ is \underline{independent} under $\B$): \\
\>  \>  \>  Return $\left\{ \mbox{\bf Sort-by-cn}(\S, \B) \right\}$\\
\>  \> $\bullet$ $k=1$, {\em shared-vars}$(\S_1) \neq \emptyset$ ($\S$ is \underline{indivisible} under $\B$): \\
\>  \>  \>  loop for $A \in \S$ \\
\>  \>  \>  \>  let $\C(A) \leftarrow$ 
               {\bf CandidateSet}$(\S\setminus\{A\}, \B\cup\{A\})$\\
\>  \>  \>  \>  let $\C'(A) \leftarrow 
   \left\{ \mbox{\bf Fold}(A\cc\Ov_A,\B) \ \left|\ \Ov_A \in \C(A) \right.\right\}$\\
\>  \>  \>  Return $\bigcup_{A \in \S}  \C'(A)$ \\
\>  \> $\bullet$ $k>1$ ($\S$ is \underline{divisible} under $\B$): \\
\>  \>  \>  loop for $i = 1$ to $k$ \\
\>  \>  \>  \>  let $\C_i \leftarrow$ {\bf CandidateSet}$(\S_i, \B)$\\
\>  \>  \>  Return $\left\{ \mbox{\bf Merge}(\{\Ov_1, \Ov_2, \ldots \Ov_k\}, \B) 
  \ \left|\ \Ov_1 \in \C_1, \Ov_2 \in \C_2,\ldots \Ov_k \in \C_k \right.\right\}$
\end{tabbing}

\begin{tabbing}
\TABLINE{5mm}
{\bf Merge}$(\{\Ov_1, \Ov_2, \ldots \Ov_k\}, \B)$ \\
\>  let {\em min-cn-candidate} $\leftarrow$ 
        $\Ov_i$ that minimizes $cn(\mbox{first-max-block}(\Ov_i))|_{\B}$,
        $1 \leq i \leq k$ \\
\>  let {\em min-cn-block} $\leftarrow$ 
         first-max-block({\em min-cn-candidate})\\
\>  remove-first-max-block({\em min-cn-candidate})\\
\>  Return {\em min-cn-block}$\cc${\bf Merge}($\{\Ov_1, \Ov_2, \ldots \Ov_k\}, 
    \B \cup \mbox{\em min-cn-block})$
\end{tabbing}


\begin{tabbing}
\TABLINE{5mm}
{\bf Fold}$(\la A_1,A_2\ldots A_k \ra, \B)$ \\
\>  if \> $k \leq 1$ 
          or $cn(A_1)|_{\B} \leq cn(A_2)|_{\footnotesize \B \cc A_1}$\\
\>  then Return $\la A_1,A_2\ldots A_k \ra$\\
\>  else\\
\>  \>  if the last subgoal of $A_1$ and the first subgoal of $A_2$ 
  satisfy the adjacency restriction \\
\>  \>  then \\
\>  \>  \>  let $A'$ $\leftarrow$ {\bf block}($A_1, A_2$)\\
\>  \>  \>  Return {\bf Fold}$(\la A',A_3\ldots A_k \ra, \B)$\\
\>  \>  else Return $\emptyset$
\end{tabbing}


\end{minipage}
} % fbox
\caption{\label{fig:algorithm-complete}
{\small 
The revised version of the \ALG.
The candidate sets are built selectively,
without explicit creation of consistency sets.
Candidate sets contain folded orderings, and unfolding is performed
only on the returned global ordering.
The code of the {\bf Unfold} and {\bf Sort-by-cn} procedures is not listed,
due to its straightforwardness.
The merging procedure recursively extracts from the given folded orderings 
max-blocks that are minimal by $cn$.
The folding procedure joins two leading blocks into a larger one, 
as long as they are cn-inverted.
}}
\end{center}
\end{figure}





% ;;;;;;;;;;;;;;;;;;;;;;;;  S A M P L E     R U N   ;;;;;;;;;;;;;;;;;;;;;;  

\subsection{Sample Run and Comparison of Ordering Algorithms}
\label{sec:sample-run}

We illustrate the work of the \ALG, using the subgoal set
shown in Figure~\ref{fig:and-or-tree}, $\S_0 = \{a, b, c(X), d(X), e(X)\}$.
After proving $c(X)$, $d(X)$ or $e(X)$, we can assume that $X$ is bound.
Let the control values for the subgoals be as shown 
in Table~\ref{table:example-costs}.
The column $c(free)$ contains control values for the subgoal $c(X)$
when $X$ is not yet bound by the preceding subgoals (i.e., the binding set
does not contain $d(X)$ or $e(X)$). The column $c(bound)$ contains cost
values of $c(X)$ when $d(X)$ or $e(X)$ have already bound $X$.
For example, $\cost(c(X))|_{\{a,d(X)\}} = \cost(c(bound)) = 5$.
The \ALG\ traverses the \TREE\ of $\S_0$ as follows.
(The names of the nodes are as in Figure~\ref{fig:and-or-tree}.)


\begin{table}
\begin{center}
\begin{tabular}{|l|c|c|c|c|c|c|c|c|}
\hline 
      & a     & b   & c(free) & c(bound) & d(free) & d(bound) & e(free) & e(bound)\\
\hline
\cost  & 10    & 5   & 5       & 5        &      10 &        5 &      20 &    10 \\
\hline
\nsols & 0.8   & 2   & 2       & 0.5      &       4 &        1 &     0.4 &   0.1 \\
\hline
\cn    & -0.02 & 0.2 & 0.2     & -0.1     &     0.3 &        0 &   -0.03 & -0.09 \\
\hline
\end{tabular}
\caption{\label{table:example-costs}
\small 
Control values for the sample runs of the ordering algorithms.
}
\end{center}
\end{table}



\begin{enumerate}
\item
The root of the \TREE, $n1$, has empty binding set $\B(n1) = \emptyset$,
and the associated subgoal  set 
$\S(n1) = \{ a, b, c(X), d(X), e(X) \}$.
The set $\S(n1)$ is partitioned into two subsets under $\B(n1)$:
one independent -- $\{ a, b \}$,
and one indivisible -- $\{ c(X), d(X), e(X) \}$.
These two subsets correspond to two child nodes of the AND-node $n1$:
$n2$ and $n3$, both with empty binding sets.


\item
$\S(n2)$ is independent under $\B(n2)$.
Therefore, $n2$ is a leaf, and its sole candidate ordering is obtained
by sorting its subgoals by $cn$ under $\B(n2)$.
$cn(a)|_{\emptyset} = -0.02$, $cn(b)|_{\emptyset} = 0.2$, 
thus $CandSet(n2) = \{\la a, b \ra\}$.

\item
$\S(n3)$ is indivisible under $\B(n3)$. 
Therefore, $n3$ is an OR-node, and its three children are created --
one for each subgoal of $\S(n3)$ serving as the binder.
\begin{itemize}
\item 
Binder $c(X)$ yields the child node $n4$ with the associated set 
$\S(n4) = \{ d(X), e(X) \}$ and the binding set $\B(n4) = \{c(X)\}$.
$\S(n4)$ is independent under $\B(n4)$. 
Therefore, $n4$ is a leaf, and its sole candidate is obtained by
sorting its subgoals by $cn$: 
\[ cn(d(X))|_{\{c(X)\}} = 0, \ \ \ cn(e(X))|_{\{c(X)\}} = -0.09; \]
thus, the candidate of $n4$ is $\la e(X), d(X) \ra$.
\item 
Binder $d(X)$ yields the child node $n5$ with the associated set 
$\S(n5) = \{ c(X), e(X) \}$ and the binding set $\B(n5) = \{d(X)\}$.
$\S(n5)$ is independent under $\B(n5)$, and its sorting by $cn$
produces the candidate $\la c(X), e(X) \ra$.
\item 
Binder $e(X)$ yields the child node $n6$ with the associated set 
$\S(n6) = \{ c(X), d(X) \}$  and the binding set $\B(n6) = \{e(X)\}$.
$\S(n6)$ is independent under $\B(n6)$, and its sorting by $cn$
produces the candidate $\la c(X), d(X) \ra$.

\end{itemize}


\item
We now add each binder to its corresponding child's candidate
and obtain three orderings of the OR-node $n3$:
$\la c(X), e(X), d(X) \ra$,
$\la d(X), c(X), e(X) \ra$,
$\la e(X), c(X), d(X) \ra$.

\item
We now perform folding of these orderings
and check violations of the adjacency restriction,
in order to determine whether a block has a cheaper permutation.
\begin{itemize}
\item
First, we perform the folding of $\la c(X), e(X), d(X) \ra$.
The pair $\la c(X), e(X) \ra$ is cn-inverted:
$cn(c(X))|_{\emptyset} = 0.2$, $cn(e(X))|_{\{c(X)\}} = -0.09$.
We thus unite it into a block.
This block does not pass the adjacency restriction test
(Equation~\ref{eq:adjacency-restriction}):
\begin{eqnarray*}
\cost(\la c(X), e(X) \ra)|_{\emptyset} &=& 5 + 2 \cdot 10 = 25, \\
\cost(\la e(X), c(X) \ra)|_{\emptyset} &=& 20 + 0.4 \cdot 5 = 22.
\end{eqnarray*}
Therefore, this ordering is MC-contradicting and can be discarded.

\item
We perform the folding of  $\la d(X), c(X), e(X) \ra$.
$cn(d(X))|_{\emptyset} = 0.3$, $cn(c(X))|_{\{d(X)\}} = -0.1$, 
the pair is cn-inverted, and we unite it into a block.
This block does not pass the adjacency restriction test:
\begin{eqnarray*}
\cost(\la d(X), c(X) \ra)|_{\emptyset} &=& 10 + 4 \cdot 5 = 30, \\
\cost(\la c(X), d(X) \ra)|_{\emptyset} &=& 5 + 2 \cdot 5 = 15.
\end{eqnarray*}
This ordering is rejected too, even before its folding is finished.
If we continue the folding process, we shall see that the subgoal $e(X)$
must also be added to this block, since 
$cn(\la d(X), c(X) \ra)|_{\emptyset} = \frac{4 \times 0.5 - 1}{30} = 0.0333$,
and $cn(e(X))|_{\la d(X), c(X) \ra} = -0.09$.

\item
We perform the folding of $\la e(X), c(X), d(X) \ra$.
$cn(e(X))|_{\emptyset} = -0.03$, $cn(c(X))|_{\{e(X)\}}$ $=$ $-0.1$, 
the pair is cn-inverted,
and we form a block $ec(X) = \la e(X), c(X) \ra$, which passes the adjacency
restriction test:
\begin{eqnarray*}
\cost(\la e(X), c(X) \ra)|_{\emptyset} &=& 20 + 0.4 \cdot 5 = 22, \\
\cost(\la c(X), e(X) \ra)|_{\emptyset} &=& 5 + 2 \cdot 10 = 25.
\end{eqnarray*}
We compute the control values of the new block:
\begin{eqnarray*}
\cost(ec(X))|_{\emptyset} &=& 20 + 0.4 \cdot 5 = 22 \\
\nsols(ec(X))|_{\emptyset} &=& 0.4 \cdot 0.5 = 0.2 \\
cn(ec(X))|_{\emptyset} &=& \frac{0.2-1}{22} = -0.0363636
\end{eqnarray*}
$cn(d(X))|_{\{ec(X)\}} = 0$, thus the pair $\la ec(X), d(X)\ra$ is cn-ordered,
no more folding is needed, 
and we add the folded candidate $\la ec(X), d(X)\ra$ to the candidate set of $n3$.

\end{itemize}


\item
We now perform merging of the candidate set of $n2$, $\{\la a, b \ra\}$, 
with the candidate set of $n3$, $\{\la ec(X), d(X) \ra\}$.
In the resulting sequence max-blocks must be sorted by $cn$.
\[ cn(a) = -0.02, \ \ \  cn(b) = 0.2,\ \ \  
 cn(ec(X))|_{\emptyset} = -0.0363636, \ \ \  cn(d(X))|_{\{ec(X)\}} = 0. \]
The merged ordering, $\la ec(X), a, d(X), b \ra$, 
is added to the candidate set of $n1$.

\item
We compare the costs of all candidates of $n1$, and output the cheapest one.
In our case, there is only one candidate, $\la ec(X), a, d(X), b \ra$.
The algorithm returns this candidate unfolded, $\la e(X), c(X), a, d(X), b \ra$.

\end{enumerate}


\begin{table}[t]
\begin{center}
{\small
\begin{tabular}{l|c|r}
\multicolumn{1}{c|}{Cheapest prefix} & Extension/Completion & \multicolumn{1}{c}{Cost}\\ 
\hline
$\emptyset$ 
& $\la a \ra$ & 10 \\
& $\la b \ra$ & 5 \\
& $\la c(X) \ra$ & 5 \\
& $\la d(X) \ra$ & 10 \\
& $\la e(X) \ra$ & 20 \\
\hline
$\la b \ra$ 
& $\la b, a \ra$ & the adjacency restriction test fails\\
& $\la b, c(X) \ra$ & $5 + 2 \cdot 5 = 15$ \\
& $\la b, d(X) \ra$ & $5 + 2 \cdot 10 = 25$ \\
& $\la b, e(X) \ra$ & the adjacency restriction test fails\\
\hline
$\la c(X) \ra$
& $\la c(X), e(X), a, d(X), b \ra$ &
$5 + 2(10+0.1(10+0.8(5+1 \cdot 5))) = 28.6$ \\
\hline
$\la a \ra$ 
& $\la a, b \ra$    & $10 + 0.8 \cdot 5 = 14$ \\
& $\la a, c(X) \ra$ & $10 + 0.8 \cdot 5 = 14$ \\
& $\la a, d(X) \ra$ & $10 + 0.8 \cdot 10 = 18$ \\
& $\la a, e(X) \ra$ &  the adjacency restriction test fails\\
\hline
$\la d(X) \ra$
& $\la d(X), c(X), e(X), a, b \ra$ &
$10 + 4(5+0.5(10+0.1(10+0.8 \cdot 5))) = 52.8$ \\
\hline
$\la a, b \ra$
& $\la a, b, c(X) \ra$ & $14 + 0.8 \cdot 2 \cdot 5 = 22$ \\
& $\la a, b, d(X) \ra$ & $14 + 0.8 \cdot 2 \cdot 10 = 30$ \\
& $\la a, b, e(X) \ra$ &  the adjacency restriction test fails\\
\hline
$\la a, c(X) \ra$
& $\la a, c(X), e(X), d(X), b \ra$ &
$14+0.8 \cdot 2(10+0.1(5+1 \cdot 5)) = 31.6$ \\
\hline
$\la b, c(X) \ra$
& $\la b, c(X), e(X), a, d(X) \ra$ &
$15+ 2 \cdot 2(10+0.1(10+0.8 \cdot 5)) = 60.6$ \\
\hline
$\la a, d(X) \ra$
& $\la a, d(X), c(X), e(X), b \ra$ &
$18+0.8 \cdot 4(5+0.5(10+0.1\cdot 5)) = 50.8$ \\
\hline
$\la e(X) \ra$
& $\la e(X), c(X), a, d(X), b \ra$ &
$20 + 0.4(5+0.5(10+0.8(5+1 \cdot 5))) = 25.6$ \\
\hline
$\la a, b, c(X) \ra$
& $\la a, b, c(X), e(X), d(X) \ra$ &
$22+0.8 \cdot 2 \cdot 2(10+0.1 \cdot 5) = 55.6$ \\
\hline
$\la b, d(X) \ra$
& $\la b, d(X), c(X), e(X), a \ra$ &
$25 + 2 \cdot 4(5 + 0.5(10+0.1 \cdot 10)) = 109$ \\
\hline
$\la e(X), c(X), a, d(X), b \ra$
& complete ordering & \\
\hline
\end{tabular}
}
\caption{\label{table:smith+natarajan-sample-run}
{\small 
A trace of a sample run of Algorithm~\protect\ref{alg:smith+natarajan}
on the set of Figure~\protect\ref{fig:and-or-tree}.
The left column shows the cheapest prefix extracted from the list on each step,
the middle column -- its extensions or completions that are added to the list,
and the right column -- their associated costs.
}}
\end{center}  
\end{table}




For comparison, we now show how the same task is performed by 
Algorithm~\ref{alg:smith+natarajan}.
The algorithm maintains a list of prefixes, sorted by their cost values,
and which initially contains an empty sequence.
On each step the algorithm extracts from the list its cheapest element, 
and adds to the list the extensions or completions of this prefix.
Extensions are created when the set of remaining subgoals
is dependent, by appending each of the remaining subgoals  
to the end of the prefix.
Completions are created when the set of remaining subgoals
is independent, by sorting them and appending the entire resulting sequence 
to the prefix.
An extension is added to the list only when the adjacency restriction 
test succeeds on its two last subgoals.
To make the list operations faster, we can implement it as a heap
structure \cite{cormen:91}.

The trace of Algorithm~\ref{alg:smith+natarajan} on the set 
$\S_0$ is shown in Table~\ref{table:smith+natarajan-sample-run}.
The left column shows the cheapest prefix extracted from the list on each step,
the middle column -- its extensions or completions that are added to the list,
and the right column -- their associated costs.

It looks as if the \ALG\ orders the given set $\S_0$ more
efficiently than Algorithm~\ref{alg:smith+natarajan}.
We can compare several discrete measurements to show this.
For example, Algorithm~\ref{alg:ordering-algorithm} performs 4 sorting sessions,
each one with 2 elements, while Algorithm~\ref{alg:smith+natarajan} performs
5 sortings with 2 elements, and 3 sortings with 3 elements.
The adjacency restriction is tested only 3 times by 
Algorithm~\ref{alg:ordering-algorithm}, and 11 times by 
Algorithm~\ref{alg:smith+natarajan}.
Algorithm~\ref{alg:ordering-algorithm} creates totally 8 different ordered
sub-sequences, with total length 22,
while Algorithm~\ref{alg:smith+natarajan} creates 24 ordered prefixes,
with total length 55. 




% ;;;;;;;;;;;;;;;;;;;;;;; COMPLEXITY   ANALYSIS  ;;;;;;;;;;;;;;;;;;;;;;;;

\subsection{Complexity Analysis}

Both Algorithm~\ref{alg:smith+natarajan} and \AO\ find a minimal ordering,
and both sort independent subsets of subgoals whenever possible.
\AO, however, offers several advantages due to its divide-and-conquer strategy.


\begin{figure}[bt]
\begin{center}
\fbox{
\begin{minipage}{4in}

\medskip
\begin{center}
\epsfig{figure=figs/pictures/clique.eps,width=3in}
\end{center}
\smallskip
\end{minipage}
} % fbox
\caption{\label{fig:clique}
{\small 
An example of the worst case for ordering.
When all variables are initially free,
every subset of subgoals is indivisible under the binding of the rest
of subgoals, and the overall complexity
of ordering by \protect\AO\ is $O(n!)$.
}}
\end{center}  
\end{figure}
 

Let $n$ be the number of subgoals in the initial set.
For convenience, we assume that the time of computing the control values 
for one subgoal is $O(1)$; otherwise, if this time is $\tau$, all the complexities
below must be multiplied by $\tau$.
The worst case complexity of \AO\ is $O(n!)$.
Figure~\ref{fig:clique} shows an example of such a case for $n=5$.
In this set every two subgoals share a variable that does not appear
in other subgoals. Thus, other subgoals cannot bind it.
The set of the root is indivisible, and no matter which binder
is chosen, the sets of the children are indivisible.
So, in each child of the root, we must select every remaining subgoal
as the binder, and so on.
The overall complexity of this execution is $O(n!)$.
This is indeed the worst-case complexity: presence of AND-nodes in the
tree can only reduce it.

Note that even when $n$ is small,
such a complex rule body with $(^n_2)$ free variables
is very improbable in practical programs. 
Also, the worst-case complexity can be reduced to $O(n^2 \times 2^n)$,
if we move from \TREE s to {\em divisibility graphs} (DAGs), where all
identical nodes of a \TREE\ (same subgoal set, same binding set)
are represented by a single vertex.
The equivalence test of the tree nodes can be performed efficiently with
the help of trie structures \shortcite{aho:87}, where subgoals are sorted
lexicographically.


Let there be $n$ subgoals, with $v$ shared variables appearing in $m$ subgoals.
As was already noted in Section~\ref{sec:algorithm-outline},
the partition of subgoals into subsets can be performed in $O(n)$ average time,
using a Union-Find data structure \cite[Chapter 22]{cormen:91}.
In the worst possible case, there are no AND-nodes in the \TREE,
apart from the root node (whose set is divisible into a dependent set of
size $m$ and an independent set of size $n-m$).
The overall complexity of the \ALG\ in such a case is

\[\begin{array}{lllll}
T(n,m,v)
&=& O(n)                  & \mbox{---} & \mbox{divisibility partition} \\
&+& O((n-m)\log(n-m)) & \mbox{---} & \mbox{ordering of independent subgoals} \\
&+& O((\prod_{i=0}^{k}(m-i))\cdot\log(m-k))
                          & \mbox{---} & \mbox{ordering of dependent subgoals} \\
&+& O(m\cdot\prod_{i=0}^{k-1}(m-i)) & \mbox{---} & \mbox{folding} \\
&+& O(n\cdot\prod_{i=0}^{k-1}(m-i))   & \mbox{---} & \mbox{merging} 
\end{array}\]
where $k$ is the maximal possible number of bindings
performed before the remaining subset is independent.
If we assume that every subgoal binds all its free variables
(which happens very frequently in practical logic programs), then
$k = \min\{v,m-1\}$; otherwise $k = m-1$.
$k$ is equal to the maximal number of OR-nodes
on a path from the root to a leaf of the \TREE.
Therefore, the height of the \TREE\ is limited by $k+1$.
Actually, the tree can be shallower, since some binders can bind more
than one shared variable each.
This means that the number of shared
variables can decrease by more than 1 in each OR-node. 
Below we simplify the above formula for several common cases, when $k$
is small and when the abovementioned assumption holds (every subgoal
binds all its free variables after its proof terminates).
\begin{itemize}
\item 
If $v < m \ll n$:
\( T(n,m,v) = O(n \cdot m^v + n \cdot \log n) \)
\item 
If $m \leq v \ll n$:
\( T(n,m,v) = O(n \cdot m^{m-1} + n \cdot \log n) \)
\item
If $v \ll m \simeq n$:
\( T(n,m,v) = O(n^{v+1} \cdot \log n) \)
\item 
If $m \ll v \simeq n$:
\( T(n,m,v) = O(n \cdot m! + n \cdot \log n) \)
\end{itemize}
Generally, for a small number $v$ of shared variables,
the complexity of the algorithm is roughly bounded by $O(n^{v+1} \cdot \log n)$.
In particular, if all subgoals are independent ($v = 0$), 
the complexity is $O(n \log n)$.
In most practical cases, the number of shared free variables in a rule body
is relatively small, and every subgoal binds all its free variables;
therefore, the algorithm has polynomial complexity.
Note that even if a rule body in the program text contains many free
variables, most of them usually become bound after the rule head
unification is performed (i.e., before we start the ordering of the
instantiated body).







%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%                        L E A R N I N G                         %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\section{Learning Control Knowledge for Ordering}
\label{sec:learning}

The ordering algorithms described in the previous sections assume the availability
of correct values of average cost and number of solutions for various predicates 
under various argument bindings.
In this section we discuss how this control knowledge can be obtained by learning. 

Instead of static exploration of the program text 
\cite{debray:93,etzioni:93},
we adopt the approach of \citeA{markovitch:89:ordering}
and learn the control knowledge by collecting statistics on the literals
that were proved in the past.
This learning can be performed on-line or off-line. 
In the latter case, the ordering system first works with a {\em training set} of
queries, while collecting statistics.
This training set can be built on the distribution of user queries
seen in the past. 
We assume that the distribution of queries received by the system 
does not change significantly with time; hence, the past distribution
directs the system to learn relevant knowledge for the future queries.

While proving queries, the learning component accumulates information 
about the control values (average cost and number of solutions) of
various literals. 
Storing a separate value for each literal is not practical, for two reasons.
The first is the large space required by this approach.
The second is the lack of generalization:
the ordering algorithm is quite likely to encounter literals which 
have not been seen before, and whose control values are unknown.
Recall that when we transformed Equation~\ref{eq:real-cost} 
into Equation~\ref{eq:cost}, we moved from control values of
single literals to average control values over {\em sets of literals}.
To obtain the precise averages for these sets, we still needed the 
control values of individual literals.
Here, we take a different approach, that of learning and using control
values for {\em more general classes} of literals.
The estimated \cost\ (\nsols) value of a class can be defined as the 
average real cost (nsols) value of all examples of this class that were
proved in the past.

The more refined the classes, the smaller the variance of real control 
values inside each class, the more precise the \cost\ and 
\nsols\ estimations that the classes assign to their members, 
and the better orderings we obtain.
One easy way to define classes is by {\em modes} or {\em binding patterns} 
\cite{debray:88,ullman:88}:
for each argument we denote whether it is free or bound.
For example, for the predicate {\tt father} the possible classes are 
{\tt father(free,free)}, {\tt father(bound,free)}, {\tt father(free,bound)}
 and {\tt father(bound,bound)}.
Now, if we receive a literal (for example, {\tt father(abraham,X)}),
we can easily determine its binding pattern 
(in this case, {\tt father(bound,free)})
and retrieve the control information stored for this class.
Of course, to find the binding pattern of a subgoal with a given binding set,
we need a method to determine which variables are bound by the subgoals
of the binding set.
The same problem arose in $DPart$ computation
(Section~\ref{sec:algorithm-outline}). 
We shall discuss some practical ways to solve this problem
in Section~\ref{sec:practical-issues}.

For the purpose of class definition we can also use {\em regression
trees} -- a type of decision tree that classifies to continuous numeric
values and not to discrete classes \shortcite{breiman:84,quinlan:86}.
Two separate regression trees can be stored for every program predicate,
one for its \cost\ values, and one for the \nsols.
The tests in the tree nodes can be defined in various ways.
If we only use the test {\em ``is argument $i$ bound?''},
then the classes of literals defined by regression trees coincide with
the classes defined by binding patterns.
But we can also apply more sophisticated tests, both syntactic
(e.g., {\em ``is the third argument a term with functor {\tt f}?''})
and semantic (e.g., {\em ``is the third argument female?''}), which
leads to more refined classes and better estimations.
A possible regression tree for estimating the of number of solutions 
for predicate {\tt father} is shown in Figure~\ref{fig:regression-tree}. 

\begin{figure} 
\begin{center} 
\fbox{ 
\begin{minipage}{3.5in} 
 
\begin{center} 
\epsfig{figure=figs/pictures/regr-tree.eps,width=3.5in} 
\end{center} 
 
\end{minipage} 
} % fbox 
\caption{\label{fig:regression-tree} 
\protect{\small 
A regression tree that estimates the number of solutions for 
{\tt father(arg1,arg2)}.  
}} 
\end{center}  
\end{figure} 



Semantic tests about the arguments require logic inference (in the
example of Figure~\ref{fig:regression-tree} -- invoking the predicate
{\tt female} on the first argument of the literal).
Therefore, they must be as efficient as possible.
Otherwise the retrieval of control values will take too much time.
The problem of efficient learning of control values is further considered
elsewhere \cite{Ledeniov:1998:CUC}.

Several researchers applied machine learning techniques for
accelerating logic inference
\cite{cohen:90,dejong:86,langley:85,markovitch:93,minton:88,mitchell:86,mooney:93,prieditis:87}. 
 Some of these works 
used explanation-based learning or generalized caching techniques 
to avoid repeated computation.  Others utilized the acquired knowledge 
for the problem of {\em clause selection}.
None of these works, however, 
dealt with the problem of subgoal reordering.  









%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%                    E X P E R I M E N T A T I O N               %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Experimentation}
\label{sec:experimentation}


To test the effectiveness of our ordering algorithm, 
we experimented with it on various domains, and compared its performance 
to other ordering algorithms.
Most experiments were performed on randomly created artificial domains.
We also tested the performance of the system on several real domains.


\subsection{Experimental Methodology}
\label{sec:experimental-methodology}

All experiments described below consist of a training session, followed by a
testing session.
Training and testing sets of queries are randomly drawn from a fixed
distribution.
In the training session we collect the control knowledge for literal classes.
In the testing session we prove the queries of the testing set
using different ordering algorithms, 
and compare their performance using various measurements.

The goal of ordering is to reduce the time spent by the Prolog
interpreter when it proves queries of the testing set.
This time is the sum of the time spent by the ordering procedure 
({\em ordering time})
and the time spent by the interpreter ({\em inference time}).
Since the CPU time is known to be very sensitive to irrelevant factors
such as hardware, software and programming quality, we also show two
alternative discrete measurements: the total number of clause
{\em unifications}, and the total number of clause {\em reductions} performed.
The number of reductions reflects the size of the proof tree.

For experimentation we used a new version of the {\sc lassy} system 
\cite{markovitch:89:ordering}, 
using regression trees for learning, 
and the ordering algorithms discussed in this paper.




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Experiments with Artificial Domains}

In order to ensure the statistical significance of the results of
comparing different ordering algorithms, we experimented with many
different domains. 
For this purpose, we created a set of 100 artificial domains, each
with a small fixed set of predicates, but with a random 
number of clauses in each predicate, and with random rule lengths.
Predicates in the rule bodies, and arguments in both
rule heads and bodies are randomly drawn from fixed distributions.
Each domain has its own training and testing sets (these two sets do
not intersect). 

The more training examples are fed into the system on the learning
phase, the better estimations of control values it produces.
On the other hand, the learning time must be limited, because after
seeing a certain number of training examples, new examples do not bring
much new information, and additional learning becomes wasteful.
We have experimentally built a learning curve which shows the
dependence of the quality of the control knowledge on the amount of
training. 
The curve suggests that after control values were learned for
approximately 400 literals, there is no significant improvement in the
quality of ordering with new training examples. 
Therefore, in the subsequent experiments we stopped training after 600
cost values were learned. 
The training time was always small: one learned cost value 
corresponds to a complete proof of a literal.
Thus, if every predicate in a program has four clauses that define it,
then 600 cost values are learned after 2400 unifications, which is a
very small time.
 
The control values were learned by means of regression trees
(Section~\ref{sec:learning}), with simple syntactic tests
that only checked whether some argument is bound or whether some
argument is a term with a certain functor (the list of functors
was created automatically when the domain was loaded).
However, as we shall see, even these simple tests succeeded in making
good estimations of control values.


We tested the following ordering methods:
\begin{itemize}
\item {\bf Random:}
The subgoals are permuted randomly and the control knowledge is not used.

\item {\bf Algorithm~\ref{alg:prefixes}:}
Building ordered prefixes. 
Out of all prefixes that are permutation of one another,
only the cheapest one is retained.

\item {\bf Algorithm~\ref{alg:prefixes}a:}
As Algorithm~\ref{alg:prefixes}, but with best-first search method
used to define the next processed prefix.
A similar algorithm was used in the {\sc lassy} system 
of \citeA{markovitch:89:ordering}.

\item {\bf Algorithm~\ref{alg:prefixes}b:}
As Algorithm~\ref{alg:prefixes}a, but with adjacency restriction test added.
A similar algorithm was described by \citeA{smith:85}.

\item {\bf Algorithm~\ref{alg:smith+natarajan}:}
As Algorithm~\ref{alg:prefixes}b, but whenever all the subgoals that are not in
the prefix are independent (under the binding of the prefix), they are
sorted and the result is appended to the prefix as one unit.

\item {\bf \AO:} The \ALG.
\end{itemize}


In our experiments we always used the Bubble-Sort algorithm to
sort literals in independent sets. 
This algorithm is easy to implement, and it
is known to be efficient for small sets,
when the elements are already ordered, or nearly ordered.
In practice, programmers order most program rules optimally, 
and the sorting stops early.

Since the non-deterministic nature of the random method introduces
additional noise, we performed on each artificial domain 20 experiments 
with this method, and the table presents the average values of these measurements.

\begin{table}
\begin{center}
\begin{tabular}{l*5{r}l}
\hline
Ordering  & \hspace{3mm}Unifications & Reductions  & Ordering & Inference & Total  & Ord.Time\\
\cline{7-7}
Method    &              &             & Time     & Time      & Time   & Reductions\\
\hline
Random                              & 86052.06 & 27741.52 &   8.1910 &  27.385 &  35.576 & 0.00029 \\
Algorithm~\ref{alg:prefixes}        &  2600.32 &   911.04 &  504.648 &   1.208 & 505.856 & 0.55 \\
Algorithm~\ref{alg:prefixes}.a      &  2829.00 &   978.59 &  347.313 &   1.178 & 348.491 & 0.35 \\ 
Algorithm~\ref{alg:prefixes}.b      &  2525.34 &   881.12 &  203.497 &   1.137 & 204.634 & 0.23 \\
Algorithm~\ref{alg:smith+natarajan} &  2822.27 &   976.02 &   40.284 &   1.191 &  41.475 & 0.04 \\
\AO\                                &  2623.82 &   914.67 &   2.3620 &   1.102 &   3.464 & 0.0025 \\  
\hline
\end{tabular}
\caption{\label{table:ordering} 
\small 
The effect of ordering on the tree sizes and the CPU time
(mean results over 100 artificial domains).
}

\end{center}
\end{table}

Table~\ref{table:ordering} shows the obtained results over 100 domains:
the rows correspond to the ordering methods used,
and the columns to the measurements taken.
The rightmost column shows the ratio of the ordering time and the number of 
reductions performed, which reflects the average ordering time of one rule body.
The inference time was not measured separately, but was set as the difference
of the total time and the ordering time.

Several observations can be made:
\begin{enumerate}
\item
Using the \DC\ ordering algorithm helps to reduce the total time of proving
the testing set of queries by a factor of 10, compared to the random ordering.
The inference time is reduced by a factor of 25.

\item
All deterministic ordering methods have similar number of unifications
and reductions, 
and similar inference time, which is predictable, since they all 
find minimal orderings.
Small fluctuations of these values can be explained by the fact that 
some rules have several minimal orderings under the existing control knowledge, and
different ordering algorithms select different minimal orderings.
Since the control knowledge is not absolutely precise, the real execution costs of
these orderings may be different, which leads to the differences.
The random ordering method builds much larger trees, with larger inference time.

\item
When we compare the performance of the deterministic algorithms
(\ref{alg:prefixes} -- \ref{alg:ordering-algorithm}),
we see that the \ALG\ performs much better than the algorithms that build
ordered prefixes. 
In the latter ones, the ordering is expensive, and smaller inference time
cannot compensate for the increase in ordering time.
Only Algorithm~\ref{alg:smith+natarajan}, a combination of several ideas of
previous researchers, has total time comparable with the time of the random method
(though still greater).

\item 
It may seem strange that the simple random ordering method has larger
ordering time than the sophisticated \AO.
To explain this, note that the random method creates much larger proof trees 
(on average), therefore the number of ordered rules increases, and even the
cheap operations, like random ordering of a rule, sum up to a considerable time.
The average time spent on ordering of one rule is shown in the last column of
Table~\ref{table:ordering}; this value is very small in the random method.
\end{enumerate}




\subsection{Experiments with Real Domains}

We tested our ordering algorithm also on real domains obtained from various sources.
These domains allow us to compare orderings performed by our algorithm 
with orderings performed by human programmers.

The following domains were used:
\begin{itemize}
\item {\bf Moral-reasoner:}
Taken from the Machine Learning Repository at the University of California, 
Irvine\footnote{URL: http://www.ics.uci.edu/$\tilde{\ }$mlearn/MLRepository.html}.
The domain qualitatively simulates moral reasoning: whether a person can be
considered guilty, given various aspects of his character and of the 
crime performed.

\item {\bf Depth-first planner:}
Program 14.11 from the book ``The Art of Prolog'' \cite{sterling:94}.
The program implements a simple planner for the blocks world.


\item {\bf Biblical Family Database:}
A database similar to that described in Example~\ref{ex:family-uncle}.


\item {\bf Appletalk:}
A domain describing the physical layout of a local computer network
\cite{markovitch:89:thesis}.

\item {\bf Benchmark:}
A Prolog benchmark 
taken from the CMU Artificial Intelligence 
Reposi\-tory\footnote{URL: http://www.cs.cmu.edu/afs/cs.cmu.edu/project/ai-repository/ai/html/air.html}.
The predicate names are not informative: it is an example of a
program where manual ordering is difficult.


\item {\bf Slow reverse:}
Another benchmark program from the same source.



\item {\bf Geography:}
Also a benchmark program from the CMU Repository.
The domain contains many geographical facts about countries.
\end{itemize}



\begin{table}
\begin{center}
\begin{tabular}{|l|rr|rr|c|}
\hline
Domain &\multicolumn{2}{c|}{Without ordering} &\multicolumn{2}{c|}{With ordering} & Gain ratio\\
\cline{2-5}
       & unifications & seconds & unifications & seconds & (time/time)\\
\hline
Moral-reasoner      &  352180 &  98.39 &  87020 &  23.53 & 4.2 \\
Depth-first planner &   10225 &  19.01 &   9927 &  18.16 & 1.05 \\
Biblical Family     &  347827 & 112.68 & 120701 &  46.08 & 2.5 \\
Appletalk           & 5036167 &1246.30 & 640092 & 221.73 & 5.6 \\
Benchmark           &   62012 & 554.31 &  46012 & 395.04 & 1.4 \\
Slow reverse        &    6291 &  10.33 &   6291 &  11.92 & 0.9 \\
Geography           &  428480 & 141.47 & 226628 &  82.76 & 1.7 \\
\hline
\end{tabular}
\caption{\label{table:real-domains}
\small 
Experiments on real domains.
}
\end{center}
\end{table}

Table~\ref{table:real-domains} shows the results obtained.
For ordering we used the \ALG, with literal classes defined by binding patterns.
It can be seen that the \ALG\ was able to speed up the logic
inference in real domains as well.
Note that in the Slow Reverse domain the programmer's ordering was 
already optimal; thus, applying the ordering algorithm did not reduce
the tree sizes. 
Still, the overhead of the ordering is not significant.







%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%                    D I S C U S S I O N                         %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\section{Discussion}
\label{sec:discussion}

In this concluding section we discuss several issues concerning the
practical implementation of the \ALG\ and several ways to increase its
efficiency.
Then we survey some related areas of logic programming and propose the
use of the \ALG\ there.

\subsection{Practical Issues}
\label{sec:practical-issues}

In this subsection we would like to address several issues 
related to implementation and applications of the \ALG.

The computation of the $DPart$ function 
(Section~\ref{sec:dependence-definition})
requires a procedure for computing the set of variables
bound by a given binding set of subgoals.
The same procedure is needed for computing control values
(Section~\ref{sec:learning}). 
There are several possible ways to implement such a procedure.
For example:
\begin{enumerate}
\item
The easiest way is to {\em assume} that every subgoal binds all the
variables appearing in its arguments.
This simplistic assumption is sufficient for many domains,
especially the database-oriented ones. 
However, it is not appropriate when logic programs are used to
manipulate complex data structures containing free variables 
(such as difference lists).
This assumption was used for the experiments described 
in Section~\ref{sec:experimentation}.
\item
Some dialects of Prolog and other logic languages support {\em mode
declarations} provided by the user \cite{somogyi:96:algorithm}.
When such declarations are available, it is easy to infer the
binding status of each variable upon exiting a subgoal.
\item
Even when the user did not supply enough mode declarations,
they can often be inferred from the structure of the program
by means of {\em static analysis} \cite{debray:88}.
Note, however, that as was pointed out by \citeA{somogyi:96:algorithm},
no-one has yet demonstrated a mode inference algorithm that is
guaranteed to find accurate mode information for every predicate in
the program.
\item
We can {\em learn} the sets of variables bound by classes of subgoals
using methods similar to those described in Section~\ref{sec:learning}
for learning control values.
\end{enumerate}

Several researchers advocate user declarations of 
available (permitted) modes.
Such declarations can be elegantly incorporated into our algorithm
to prune branches that violate available modes.
When we fix a binder in an OR-node, we compute the set of variables
that become bound by it.
If this results in a violation of an available mode for one of the
subgoals of the corresponding child, then the whole subtree of this
child is pruned.
Note that we can detect violations even when the mode of the subgoal
is partially unknown at the moment.
For example, if all the available modes require that the first
argument be unbound, then binding of the argument by
the OR-node binder will trigger pruning, even if the binding status
of the other arguments is not yet known.
Figure~\ref{fig:algorithm-modes} shows how 
Algorithm~\ref{alg:ordering-algorithm} can be changed in order to 
incorporate declarations of available modes.
Any other correctness requirement can be treated in a similar manner:
a candidate ordering will be rejected whenever we see that it violates
the requirement.

\begin{figure}[tb]
\begin{center}
\fbox{
\begin{minipage}{0.8\textwidth}
\begin{tabbing}
\TABLINE{5mm}
\\
{\bf CandidateSet}$(\S, \B)$\\
\>  let $\{\S_1,\S_2,\ldots \S_k\} \leftarrow DPart(\S,\B)$ \\
\>  case \\ 
\>  \> $\ldots$ \\
\>  \> $\bullet$ $k=1$, {\em shared-vars}$(\S_1) \neq \emptyset$ 
       ($\S$ is \underline{indivisible} under $\B$): \\
\>  \>  \>  loop for $A \in \S$ \\
\>  \>  \>  \>  if $\B \cup \{A\}$ does not violate available modes \\
\>  \>  \>  \>  \>  in any subgoal of $\S \setminus \{A\}$ \\
\>  \>  \>  \>  then \\
\>  \>  \>  \>  \>  let $\C(A) \leftarrow$ 
                    {\bf CandidateSet}$(\S\setminus\{A\}, \B\cup\{A\})$\\
\>  \>  \>  \>  \>  let $\C'(A) \leftarrow 
   \left\{ \mbox{\bf Fold}(A\cc\Ov_A,\B) \ \left|\ \Ov_A \in \C(A) \right.\right\}$\\
\>  \>  \>  \>  else let $\C'(A) \leftarrow \emptyset$\ \ \
               (don't enter the branch) \\
\>  \>  \>  Return $\bigcup_{A \in \S}  \C'(A)$ \\
\end{tabbing}

\end{minipage}
} % fbox
\caption{\label{fig:algorithm-modes}
{\small 
Changes to Algorithm~\protect\ref{alg:ordering-algorithm} that make use
of available mode declarations.\protect\\
The rest of the algorithm remains unchanged.
}}
\end{center}
\end{figure}





\bigskip

The experiments described in Section~\ref{sec:experimentation} 
were performed with a Prolog interpreter.  
Is it possible to combine the \ALG\ with a Prolog compiler? 
There are several ways to achieve this goal.  One way is to
allow the compiler to insert code for on-line learning.
The compiled code will contain procedures for accumulating 
control values and for the \ALG. 
Alternatively, off-line learning can be implemented, with training
as a part of the compilation process.


Another method for combining our algorithm with existing Prolog
compilers is to use it for program transformation, and to process
the transformed program by a standard compiler.
Elsewhere \cite{Ledeniov:1998:CUC} we describe the method
for classifying the orderings produced by the \ALG. 
For each rule we build a classification tree, where classes are the
different orderings of the rule body, and the tests are applied to the
rule head arguments.
These are the same type of tests described in 
Section~\ref{sec:learning} for learning control values.
Figure~\ref{fig:classification-trees} shows two examples of such trees.

\begin{figure}[bt]
\begin{center} 
\fbox{ 
\begin{minipage}{\textwidth} 
 
\medskip 
\begin{minipage}{2.5in} 
\begin{center} 
\protect{\small 
A classification tree for the rule \\ 
{\tt uncle(X,Y)} 
of Example~\ref{ex:family-uncle}. 
} 
\end{center} 
\end{minipage} 
\begin{minipage}{2.8in} 
\begin{center} 
\epsfig{figure=figs/pictures/class-tree-family.eps,width=2.8in} 
\end{center} 
\end{minipage} 
 
\medskip 
 
\begin{minipage}{2.5in} 
\protect{\small 
A possible classification tree for the rule \\ 
{\tt head(X,Y)} $\leftarrow$ {\tt p1(X), p2(Y), p3(X,Y).} 
} 
\end{minipage} 
\begin{minipage}{3.2in} 
\begin{center} 
\epsfig{figure=figs/pictures/class-tree-strange.eps,width=3.2in} 
\end{center} 
\end{minipage} 
 
\medskip 
\end{minipage} 
} % fbox 
\caption{\label{fig:classification-trees} 
{\small
Examples of classification trees that learn rule body orderings.
}} 
\end{center}  
\end{figure} 

Given such a classification tree, we can write a set of Prolog rules,
where each rule has the same head as the original rule, 
and has a body built of all the tests on the path from the tree root
to a leaf node followed by the ordering at the leaf.
For example, the second tree in Figure~\ref{fig:classification-trees} 
yields the following set of rules:\\ 
\noindent 
{\tt head(X,Y)} $\leftarrow$ {\tt nonvar(X), male(X), p1(X), p3(X,Y), p2(Y).}\\ 
{\tt head(X,Y)} $\leftarrow$ {\tt nonvar(X), not(male(X)), p1(X), p2(Y), p3(X,Y).}\\ 
{\tt head(X,Y)} $\leftarrow$ {\tt var(X), nonvar(Y), p2(Y), p3(X,Y), p1(X).}\\ 
{\tt head(X,Y)} $\leftarrow$ {\tt var(X), var(Y), p3(X,Y), p1(X), p2(Y).}\\ 

>From Table~\ref{table:ordering} we can see that while the \ALG\
helped to reduce the inference time 
by a factor of 25, the total time was reduced only by a factor of 10.
This difference is caused by the additional computation of the
ordering procedure.
There is a danger that the benefit obtained by ordering will be
outweighed by the cost of the ordering process.
This is a manifestation of the so-called {\em utility problem}
\cite{minton:88,markovitch:93}.
In systems that are strongly-moded 
\shortcite<such as Mercury -->{somogyi:96:algorithm}
we can employ the \ALG\ statically at compilation time for each
one of the available modes, thus reducing the run-time ordering time
to zero.
The mode-based approach performs only syntactic tests of the subgoal
arguments. 
The classification tree method, described above, is a generalization
of the mode-based approach, allowing semantic tests as well.

Due to insufficient learning experience or lack of meaningful semantic
tests, it is quite possible that the classification trees contain
leaves with large degrees of error.
In such cases we still need to perform the ordering dynamically.
To reduce the harmfulness of the utility problem in the case of 
dynamic ordering, we can use  a cost-sensitive variation of the
\ALG\ \cite{Ledeniov:1998:CUC,Ledeniov:1998:LIF}.
This modified algorithm deals with the problem by explicit
reasoning about the economy of the control process.
The algorithm is {\em anytime}, that is, it can be stopped at any
moment and return its currently best ordering \cite{boddy:89}.
We learn a {\em resource-investment function} to compute the expected
return in speedup time for additional control time.
This function is used to determine a stopping condition
for the anytime procedure.
We have implemented this framework and found that indeed we have
succeeded in reducing ordering time, without
significant increase of inference time.




\subsection{Relationship to Other Works}

The work described in this paper is a continuation of the line of research
initiated by \citeA{smith:85} and continued by \citeA{natarajan:87}
and \citeA{markovitch:89:ordering}.
This line of research aims at finding the most efficient ordering of
a set of subgoals.  
The search for minimal-cost ordering is based on cost analysis that 
utilizes available information about the cost and number-of-solutions
of individual subgoals. 

\citeA{smith:85} performed an exhaustive search over the space of all
permutations of the given set of subgoals, using the {\em adjacency
restriction} to reduce the size of the search space 
(Equation~\ref{eq:adjacency-restriction}).
This restriction was applied on pairs of adjacent subgoals in the
global ordering of the entire set.
When applied to an {\em independent set of subgoals}, the adjacency
restriction is easily transformed into the sorting restriction:
the subgoals in a minimal ordering must be sorted by their $cn$ values.
\citeA{natarajan:87} arrived at this conclusion and presented an
efficient ordering algorithm for independent sets.

The \ALG\ uses subgoal dependence to break the set into smaller
subsets. 
Independent subsets are sorted.
Dependent subsets are recursively ordered, and the resulting orderings
are merged using a generalization of the adjacency restriction that
manipulates blocks of subgoals.
Therefore the \ALG\ is a generalization of both algorithms.

\medskip
During the last decade, a significant research effort went into
static analysis (SA) of logic programs.  
There are three types of SA that can be exploited
by the \ALG\ to reduce the ordering time.

A major part of the SA research deals with {\em program
termination} \cite{DeSchreye:94}.
The \ALG\ solves the termination problem, as a special case of
the efficiency problem (it always finds a terminating ordering, if such
orderings exist).
During learning, we set limits on the computation resources available
for subgoal execution.
If a subgoal is non-terminating (in a certain mode), the learning
module will associate a very high cost with this particular mode.
Consequently, the \ALG\ will not allow orderings with this mode of the
subgoal.
Nevertheless, while the use of static termination analysis is not
mandatory for a proper operation of the \ALG, we can exploit such
analysis to increase the efficiency of both the learning process and  
the ordering process.
During learning,
the limit that we set on the computation resources devoted to the
execution of a subgoal must be high, to increase the reliability of
the cost estimation.
However, such a high limit can lead to a significant increase in
learning time when many subgoals are non-terminating.
If termination information obtained by SA is available, we can use it
to avoid entering infinite branches of proof trees.
During ordering, termination information can serve to reduce the size
of space of orderings searched by the algorithm.
If the termination information comes in the form of allowed modes
\cite{somogyi:96:algorithm}, 
orderings that violate these modes are filtered out, as in 
the modified algorithm shown in Figure~\ref{fig:algorithm-modes}. 
If the termination information comes in the form of a partial order
between subgoals, orderings that violate this partial order can be
filtered out in a similar manner.

\medskip

The second type of SA research that can be combined with the \ALG\ 
is {\em correctness analysis}, where the program is tested against
specifications given by the user.

The {\sc folon} environment \cite{henrard:92} was designed to support
the methodology for logic program construction that aims at
reconciling the declarative semantics with an efficient implementation
\cite{deville:90}. 
The construction process starts with a specification, converts it into
a logic description and finally, into a Prolog program.
If the rules of the program are not correct with respect to the initial
specification, the system performs transformations such as reordering
literals in a clause, adding type checking literals and so on.
\fullciteA{deboeck:90} mention this reordering, but do not specify an
ordering algorithm different from the simple generate-and-test method.
\fullciteA{cortesi:97} present an analyzer for verifying the correctness
of a Prolog program relative to a specification which provides a list
of input/output annotations for the arguments and parameters that can
be used to establish program termination.
Again, no ordering algorithm is given explicitly.
The purpose of the \ALG\ is complementary to the purpose of {\sc folon},
and it could serve as an auxiliary aid to make the resulting Prolog
program more efficient.


Recently, the Mercury language was developed at the University of Melbourne
\shortcite{somogyi:96:status,somogyi:96:algorithm}.
Mercury is a strongly typed and strongly moded language.
Type and mode declarations should be supplied by the programmer
\shortcite<though recent releases of the Mercury system already support partial
inference of types and modes -- >{somogyi:96:status}.
The compiler checks that mode declarations for all predicates are satisfied;
if necessary, it {\em reorders} subgoals in the rule body to ensure
mode correctness (and rejects the program if neither ordering satisfies
the mode declaration constraints).
When the compiler performs this reordering, it does not consider the 
efficiency issue.
It often happens that several orderings of a rule body satisfy the 
mode declaration constraints: in such cases the Mercury compiler could
call the static version of the \ALG\ to select the most efficient ordering.
Another alternative is to augment the \ALG\ by mode declaration checks,
as was shown in Figure~\ref{fig:algorithm-modes}.

Note that Mercury is a purely declarative logic programming language,
and is therefore more suitable for subgoal reordering than Prolog.
It has no non-logical constructs that could destroy the declarative
semantics which give logic programs their power; in Mercury even I/O
is declarative.

\medskip

The third type of relevant SA is the {\em cost analysis} of logic
programs \shortcite{debray:93,braem:94,debray:97}.
\citeA{cortesi:97} describe a cost formula similar to
Equation~\ref{eq:cost} to select a lowest-cost ordering.
However, they used a generate-and-test approach which can sometimes be
prohibitively expensive.
Static analysis of cost and number of solutions can be used to obtain
the control values, instead of learning them.

\medskip

The efficiency of logic programs can also be increased by methods of
{\em program transformation} \cite{pettorossi:94,pettorossi:96}.
One of the most popular approaches is the ``rules+strategies'' approach,
which consists in starting from an initial program and then applying
one or more elementary {\em transformation rules}. 
Transformation strategies are meta-rules which prescribe suitable
sequences of applications of transformation rules.

One of the possible transformation rules is the {\em goal rearrangement rule}
which transforms a program by transposing two adjacent subgoals in a 
rule body.
Obviously, any ordering of a rule body can be transformed into any other
ordering by a finite number of such transpositions.
Thus, static subgoal ordering can be considered a special case of program 
transformation where only the goal rearrangement rule is used.
On the other hand, dynamic and semi-dynamic ordering methods cannot be
represented by simple transformation rules, since they make use of
run-time information (expressed in bindings that rule body subgoals obtain
through unifications of rule heads), and may order the same rule body
differently under different circumstances.

A program transformation technique called {\em compiling control}
\cite{bruynooghe:89,pettorossi:94} follows an approach different from
that of trying to improve the control strategy of logic programs.
Instead of enhancing the naive Prolog evaluator using a better
(and often more complex) computation rule, the program
is transformed so that the derived program behaves under the naive 
evaluator exactly as the initial program would behave under an enhanced 
evaluator.
Most forms of compiling control first translate the initial program into
some standard representation (for example, into an {\em unfolding tree}),
while the complex computation rule is used, and then the new program
is constructed from this representation, with the naive computation
rule in mind.

Reordering of rule body subgoals can be regarded as moving to a complex 
computation rule which selects subgoals in the order dictated by the
ordering algorithm.
In the case of the \ALG, this computation rule may be too complex
for simple use of compiling control methods.
Nevertheless, it can be easily incorporated into a special compiling
control method.
In Section~\ref{sec:practical-issues} we described a method of program
rewriting which first builds classification trees based on the
orderings that were performed in the past, and then uses these
classification trees for constructing clauses of a derived program.
The derived program can be efficiently executed under the naive computation
rule of Prolog.
This technique is in fact a kind of compiling control.
Its important property is the use of knowledge collected from
experience (the orderings that were made in the past).

One transformation method that can significantly benefit from the
\ALG\ is {\em unfolding} \cite{tamaki:84}.
During the unfolding process subgoals are replaced by their 
associated rule bodies.
Even if the initial rules were ordered optimally by a human programmer
or a static ordering procedure, the resulting combined sequence may be
far from optimal.
Therefore it could be very advantageous to use the \ALG\ for
reordering of the unfolded rule.
As the rules become longer, the potential benefit of ordering grows.
The danger of high complexity of the ordering procedure can be
overcome by using the cost-sensitive version of the \ALG\ 
(Section~\ref{sec:practical-issues}).




\subsection{Conclusions}
\label{sec:conclusions}

In this work we study the problem of subgoal ordering in logic programs.
We present both a theoretical base and a practical implementation of the ideas,
and show empirical results that confirm our theoretical predictions.
We combine the ideas of \citeA{smith:85}, \citeA{simon:75} and
\citeA{natarajan:87} into a novel algorithm for ordering of
conjunctive goals. 
The algorithm is aimed at minimizing the time which the logic
interpreter spends on the proof of the given conjunctive goal.

The main algorithm described in this paper is the \ALG\ 
(\AO, Section~\ref{sec:algorithm-complete}).
It works by dividing the sets of subgoals into smaller sets, 
producing candidate sets of orderings for the smaller sets,
and combining these candidate sets to obtain orderings of the
larger sets.
We prove that the algorithm finds a minimal ordering of the given set
of subgoals, and we show its efficiency under practical assumptions.
The algorithm can be employed statically (to reorder rule bodies in the
program text before the execution starts), 
semi-dynamically (to reorder the rule body before the reduction
is performed) or dynamically (to reorder
the resolvent after every reduction of a subgoal by a rule body).

Several researchers \cite{minker:78,warren:81,naish:85:lpj,naish:85,nie:90}
proposed various heuristics for subgoal ordering.
Though fast, these methods do not guarantee finding minimal-cost orderings.
Our algorithm provably finds a minimal-cost ordering, though the ordering itself
may take more time than with the heuristic methods.
In the future it seems promising to incorporate heuristics into the \ALG.
For example, heuristics can be used to grade binders in OR-nodes:
rather than exhaustively trying all subgoals as binders, we could try just
one, or several binders, thus reducing the ordering time.
Also, the current version of our ordering algorithm is suitable only
for finding {\em all} solutions to a conjunctive goal.
We would like to extend it to the problem of finding one solution,
or a fixed number of solutions.

Another interesting issue for further research is the adaptation of the 
\ALG\ to interleaving ordering methods (Section~\ref{sec:interlaving-static-etc}).
There, if subgoals of a rule body are added to an ordered resolvent,
it seems wasteful to start a complete ordering process; we should use
the information stored in the existing ordering of the resolvent.
Perhaps the whole \TREE\ of the resolvent should be stored, and its
nodes updated when subgoals of a rule body are added to the resolvent.


The ordering algorithm needs control knowledge for its work.
This control knowledge is the average cost and number of solutions of literals,
and it can be learned by training and collecting statistics.
We make an assumption that the distribution of queries received by the system 
does not change with time; thus, if the training set is based on the distribution
seen in the past, the system learns relevant knowledge for future queries.
We consider the issue of learning control values more thoroughly
in another paper \cite{Ledeniov:1998:CUC}, together with other issues 
concerning the \ALG\ (such as minimizing the total time, instead of 
minimizing the inference time only). 

\citeA{ullman:88} showed that the problem of ordering subgoals to obtain
termination is inherently exponential in time.
The problem we work with is substantially harder: we must not only
find an order whose execution terminates in finite time, but one that
terminates in minimal finite time. 
It is impossible to find an efficient algorithm for all cases.
The \ALG, however, is efficient in most practical cases, 
when the graph representing the subgoal dependence
(Figure~\ref{fig:subgoal-graph}) is sparsely connected.

We have implemented the \ALG\ and tested it on artificial and real domains.
The experiments show a speedup factor of up to 10 compared with random
ordering, and up to 13 compared with some alternative ordering algorithms.


The \ALG\ can be useful for many practical applications.
Formal hardware verification has become extremely important 
in the semiconductor industry.
While model checking is currently the most widely used technique,
it is generally agreed that coping with the increasing complexity of
VLSI design requires methods based on theorem proving.
The main obstacle preventing the use of automatic theorem proving is 
its high computational demands.
The \ALG\ may be used for speeding up logic inference,
making the use of automatic theorem provers more practical.

Logic has gained increasing popularity for
representation of common-sense knowledge.
It has several advantages, including flexibility and well-understood semantics.  
Indeed, the CYC project \cite{Lenat:1995} has recently moved from
frame-based representation to logic-based representation.  
However, the large scale of such knowledge bases
is likely to present significant efficiency problems to the inference engines.
Using automatic subgoal ordering techniques, such as those described
here, may help to solve these problems.

The issue of subgoal ordering obtains a new significance with the
development of Inductive Logic Programming \cite{lavrac:94,muggleton94:jlp}.
Systems using this approach, such as FOIL \cite{QuiCam95:jrnl}, 
try to build correct programs as fast as possible,
without considering the efficiency of the produced programs.
Combining the \ALG\ with Inductive Logic Programming and other techniques
for the synthesis of logic programs 
(such as the deductive and the constructive approaches)
looks like a promising direction.







%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%
%%%                            A P P E N D I X
%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\appendix

\section{Proof of Lemma~\protect\ref{lemma:transposition-blocks-equivalent}}
\label{sec:app:proofs}

In this appendix we present the proof of a lemma which was omitted
from the main text of the paper for reasons of compactness.
Before we prove it we show two auxiliary lemmas.

\begin{lemma}
\label{lemma:cn-is-average}
\ \\
Let $\Av_1$ and $\Av_2$ be two ordered sequences of subgoals,
and $\B$ a set of subgoals.
The value of $cn(\Av_1 \cc \Av_2)|_{\B}$ lies between the values
$cn(\Av_1)|_{\B}$ and $cn(\Av_2)|_{\B\cup\Av_1}$.
\end{lemma}

\begin{proof}

\noindent
\(
\begin{array}{llll}
\mbox{Denote\ } & c_1 = \cost(\vec{A_1})|_{\B}\ &
               n_1 = \nsols(\vec{A_1})|_{\B}\ &
               cn_1 = \cn(\vec{A_1})|_{\B} \\

             & c_2 = \cost(\vec{A_2})|_{\B\cup\Av_1}\ &
               n_2 = \nsols(\vec{A_2})|_{\B\cup\Av_1}\ &
               cn_2 = \cn(\vec{A_2})|_{\B,\cup\Av_1} \\

             & c_{1,2} = \cost(\Av_1 \cc \Av_2)|_{\B} 
             & n_{1,2} = \nsols(\Av_1 \cc \Av_2)|_{\B} 
             & cn_{1,2} = \cn(\Av_1 \cc \Av_2)|_{\B} 
\end{array}
\)

\begin{eqnarray*}
cn_{1,2} 
&=& \frac{n_{1,2} -1}{c_{1,2}}
    = \frac{n_1 n_2 -1}{c_{1,2}}
    = \frac{(n_1 -1) + n_1(n_2-1)}{c_{1,2}} =\\
&=& \frac{c_1\frac{n_1-1}{c_1} + n_1c_2\frac{n_2-1}{c_2}}{c_{1,2}}
    = \frac{c_1cn_1 + n_1c_2cn_2}{c_{1,2}}
    = \frac{c_1}{c_{1,2}}\cdot cn_1 + \frac{n_1c_2}{c_{1,2}}\cdot cn_2
\end{eqnarray*}

So, $cn_{1,2}$ always lies between $cn_1$ and $cn_2$
(because $\frac{c_1}{c_{1,2}}$ and $\frac{n_1c_2}{c_{1,2}}$ 
are positive and sum to 1).
More exactly, the point  $cn_{1,2}$ divides the segment $[cn_1,cn_2]$ with ratio
\[ (cn_{1,2} - cn_1) : (cn_2 - cn_{1,2}) = n_1c_2 : c_1. \]
\end{proof}

In other words, $cn_{1,2}$ is a {\em weighted average} of $cn_1$ and $cn_2$.
Note that $c_1$ is the amount of resources spent in the proof-tree of $\Bv_1$,
$n_1 c_2$ -- the resources spent in the tree of $\Bv_2$, and
$c_{1,2}$ is their sum.
So, the more time (relatively) we dedicate to the proof of $\Bv_1$,
the closer $cn_{1,2}$ is to $cn_1$.
This conclusion can be generalized to a larger number of components 
in a concatenation (the proof is by induction):
{\small 
\begin{eqnarray*}
\cn(\Av_1\cc\Av_2\cc\ldots\Av_k)|_{\B} 
&=& \frac{\cost(\Av_1)|_{\B}}{\cost(\Av_1\cc\Av_2\cc\ldots\Av_k)|_{\B}} \cdot
    \cn(\Av_1)|_{\B} + \\
&+& \frac{\nsols(\Av_1)|_{\B}\cdot\cost(\Av_2)|_{\B\cup\Av_1}}{\cost(\Av_1\cc\Av_2\cc\ldots\Av_k)|_{\B}} \cdot
    \cn(\Av_2)|_{\B\cup\Av_1} + \ldots + \\
&+& \frac{\nsols(\Av_1\cc\Av_2\cc\ldots\Av_{k-1})|_{\B} \cdot
          \cost(\Av_k)|_{\B\cup\Av_1\cup\ldots\Av_{k-1}}}{\cost(\Av_1\cc\Av_2\cc\ldots\Av_k)|_{\B}} \cdot
    \cn(\Av_k)|_{\B\cup\Av_1\cup\ldots\Av_{k-1}}
\end{eqnarray*}
\ \hfill $\Box$
} %small
\medskip


\begin{lemma}
\label{lemma:cn-equal-enter-the-same-block}
\ \\
Let $\S_0$ be a set of subgoals and
$N$ be a node in the \TREE\ of $\S_0$.
Let $\Ov_N = \Qv \cc \Av_1 \cc \Av_2 \cc \Rv$ be an ordering of $\S(N)$,
where $\Av_1$ and $\Av_2$ are cn-equal max-blocks:
$cn(\Av_1)|_{\B(N) \cup \Qv} = cn(\Av_2)|_{\B(N)\cup\Qv\cup\Av_1}$.

Let $M$ be an ancestor of $N$ and
$\Ov_M$ be an ordering of $\S(M)$ consistent with $\Ov_N$,
where $\Av_1$ and $\Av_2$ are not violated.
Then either $\Av_1$ and $\Av_2$ are both max-blocks in $\Ov_M$
and all max-blocks that stand between them are cn-equal to them,
or $\Av_1$ and $\Av_2$ belong to the same max-block in $\Ov_M$,
or $\Ov_M$ is MC-contradicting.
\end{lemma}

\begin{proof} 
By induction on the distance between $N$ and $M$.
If $M = N$, then $\Av_1$ and $\Av_2$ are max-blocks, and the lemma holds.
Let $M \neq N$, and let $M'$ be the child of $M$ whose descendant is $N$.
By inductive hypothesis, the lemma holds for $N$ and $M'$.
Let $\Ov'_M$ be the projection of $\Ov_M$ on $M'$.
$\Av_1$ and $\Av_2$ are not violated in $\Ov'_M$, since they are
not violated in $\Ov_M$.

\begin{itemize}
\item
If $\Av_1$ and $\Av_2$ are both max-blocks in $\Ov_M'$,
then by the inductive hypothesis all max-blocks that stand between them
are cn-equal to them. 
If $M$ is an OR-node, no new subgoals can enter between $\Av_1$ and $\Av_2$.
If $M$ is an AND-node, the insertion of new subgoals is possible, but if
it violates blocks, or places max-blocks not ordered by \cn, then $\Ov_M$
is MC-contradicting, by Corollary~\ref{corollary:block-violated} or
Lemma~\ref{lemma:contradicting-divisible}.
So, if  $\Ov_M$ is not MC-contradicting, then all new max-blocks inserted 
between $\Av_1$ and $\Av_2$ must be cn-equal to them both.

Assume that $\Av_1$ and $\Av_2$ are not both max-blocks in $\Ov_M$.
Without loss of generality, let $\Av_1$ be member of a larger max-block in $\Ov_M$.
We show that $\Av_2$ must also participate in the same max-block.

Since $\Av_1$ joined a larger block, there must exist another block, $\Bv$,
adjacent to $\Av_1$, such that their pair is cn-inverted. 
Let $\Bv$ stand to the left of $\Av_1$ (in the opposite case, the proof is similar):
\mbox{$\Ov_M = \Xv \cc \Bv \cc \Av_1 \cc \Yv \cc \Av_2 \cc \Zv$}.
The pair $\la \Bv, \Av_1 \ra$ is cn-inverted, i.e.,
$cn(\Bv)|_{\B(M) \cup \Xv} > cn(\Av_1)|_{\B(M) \cup \Xv \cup \Bv}$.
>From Lemma~\ref{lemma:cn-is-average}, 
$cn(\Bv \cc \Av_1)|_{\B(M) \cup \Xv} > cn(\Av_1)|_{\B(M) \cup \Xv \cup \Bv}$,
and we must add to the block $\Bv \cc \Av_1$ all
blocks from $\Yv$, because they are all cn-equal to $\Av_1$.
Also, $cn(\Av_1)|_{\B(M) \cup \Xv \cup \Bv} = 
cn(\Av_2)|_{\B(M) \cup \Xv \cup \Bv \cup \Av_1}$, 
and $\Av_2$ must also be added to the block.
Thus, $\Av_1$ and $\Av_2$ belong to the same max-block in $\Ov_M$.

\item
If $\Av_1$ and $\Av_2$ belong to the same max-block in $\Ov'_M$,
then this block is either violated in $\Ov_M$, or not.
In the former case, $\Ov_M$ is MC-contradicting, by 
Corollary~\ref{corollary:block-violated}.
In the latter case, $\Av_1$ and $\Av_2$ belong to the same max-block in $\Ov_M$.

\item
If $\Ov'_M$ is MC-contradicting, then $\Ov_M$ is MC-contradicting too
(the proof is easy).
\hfill $\Box$
\end{itemize}
\end{proof}




\noindent
Now we can prove Lemma~\ref{lemma:transposition-blocks-equivalent}:

\begin{applemma}{\ref{lemma:transposition-blocks-equivalent}}
\ \\
Let $\S_0$ be a set of subgoals,
$N$ be a node in the \TREE\ of $\S_0$ and
$\Ov_N = \Qv \cc \Av_1 \cc \Av_2 \cc \Rv$ be an ordering of $\S(N)$,
where $\Av_1$ and $\Av_2$ are max-blocks, 
mutually independent and cn-equal under the bindings of $\B(N) \cup \Qv$.
Then $\Ov_N$ is blockwise-equivalent with 
$\Ov'_N = \Qv \cc \Av_2 \cc \Av_1 \cc \Rv$.
\end{applemma}

\begin{proof}
\ \\
Let $\Sv$ be a minimal ordering of $\S_0$ binder-consistent with $\Ov_N$.
By Corollary~\ref{corollary:block-violated}, 
$\Sv$ does not violate the blocks of $\Ov_N$, in particular $\Av_1$ and $\Av_2$:
$\Sv = \Xv \cc \Av_1 \cc \Yv \cc \Av_2 \cc \Zv$.
Let $\Sv' = \Sv|_{\Ov_N}^{\Ov'_N} = \Xv \cc \Av_2 \cc \Yv \cc \Av_1 \cc \Zv$.
We must show that $\Sv'$ is minimal, which implies blockwise equivalence
of $\Ov_N$ and $\Ov'_N$.

If $\Yv$ is empty, then $Cost(\Sv) = Cost(\Sv')$ 
by Lemma~\ref{lemma:independent-adjacent}
($\Av_1$ and $\Av_2$ are adjacent, mutually independent and cn-equal;
thus, their transposition does not change the cost).

If $\Yv$ is not empty, then by Corollary~\ref{corollary:interleaving-independent}
$\Yv$ is mutually independent of both $\Av_1$ and $\Av_2$
($\Sv$ is binder-consistent with $\Ov_N$, therefore $\B(N) \subseteq \Xv$,
and consequently $\Yv \cap \B(N) = \emptyset$).
$\Yv$ can be divided into several blocks, each one of them cn-equal to 
$\Av_1$ and $\Av_2$:
since $\Sv$ is minimal, $\Ov_N$ cannot be MC-contradicting,
and the claim follows from Lemma~\ref{lemma:cn-equal-enter-the-same-block}.
By Lemma~\ref{lemma:cn-is-average},
$cn(\Yv)|_{\Xv} = cn(\Av_1)|_{\Xv} = cn(\Av_2)|_{\Xv}$.
By Lemma~\ref{lemma:independent-adjacent}:
\[
\begin{array}{lllll}
Cost(\Sv) 
 &=& Cost(\Xv \cc \Av_1 \cc \Yv   \cc \Av_2 \cc \Zv) &=&\ //\ swap (Y, A_2) \\
 &=& Cost(\Xv \cc \Av_1 \cc \Av_2 \cc \Yv   \cc \Zv) &=&\ //\ swap (A_1, A_2) \\
 &=& Cost(\Xv \cc \Av_2 \cc \Av_1 \cc \Yv   \cc \Zv) &=&\ //\ swap (A_1, Y) \\
 &=& Cost(\Xv \cc \Av_2 \cc \Yv   \cc \Av_1 \cc \Zv) &=& Cost(\Sv')
\end{array}
\]
Minimality of $\Sv'$ implies blockwise equivalence of $\Ov_N$ and $\Ov'_N$.
\hfill $\Box$
\end{proof}








%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                %%%
%%%         C O R R E C T N E S S       P R O O F                  %%%
%%%                                                                %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Correctness of the \DC\ Algorithm}
\label{sec:app:correctness-proof}

In this section we show that the \ALG\ is correct,
i.e., given a set of subgoals $\S_0$, it returns its minimal ordering.
It suffices to show that the candidate set of the root node of 
$DTree(\S_0,\emptyset)$ is valid. 
In such a case, as follows from the definition 
of valid sets, it must contain a minimal ordering.
The algorithm returns one of the cheapest candidates of the root.
Therefore, if the candidate set of the root is valid, the \ALG\ must return
a minimal ordering of $\S_0$.

We start by defining {\em strong validity} of sets of orderings.
We then prove that strong validity implies validity.
Finally, we use induction to prove a theorem, 
showing that the candidate set produced for each node in the \TREE\ 
is strongly valid.

\medskip

\begin{definition}
Let $\S_0$ be a set of subgoals, $N$ be a node in the \TREE\ of $\S_0$. 
The set $\C_N \subseteq \pi(\S(N))$ is {\em strongly valid},
if every ordering in $\pi(\S(N)) \setminus \C_N$ is either MC-contradicting
or blockwise-equivalent to some member of $\C_N$,
unless no ordering of $\S(N)$ is min-consistent.
\begin{tabbing}
$StronglyValid_{N,\S_0}(\C_N) \iff$ \\
$[ \exists \Ov'_N \in \pi(\S(N)):\ MC_{N,\S_0}(\Ov'_N) ] \rightarrow
[ \Ov_N \in \pi(\S(N))\setminus\C_N$ \= 
$\rightarrow MCC_{N,\S_0}(\Ov_N) \vee$ \\
 \> $( \exists \Ov''_N \in \C_N \wedge MCE_{N,\S_0}(\Ov_N,\Ov''_N) ) ]$
\end{tabbing}
\end{definition}


\begin{lemma}
\label{lemma:strongly-valid-is-valid}
A strongly valid set of orderings is valid.
\end{lemma}

\begin{proof}
Let $\S_0$ be a set of subgoals,
$N$ be a node in the \TREE\ of $\S_0$,
$\C(N)$ be a strongly valid set of orderings of $N$.

If there is no min-consistent ordering of $N$,
then $\C(N)$ is valid, by the definition of a valid set
(Section~\ref{sec:valid-orderings}).

Otherwise, there exists at least one minimal ordering of $\S_0$, 
binder-consistent with $N$.
Every ordering in $\pi(\S(N)) \setminus \C(N)$ is 
either MC-contradicting or blockwise-equivalent to some member of  $\C(N)$.
To prove that $\C(N)$ is valid,
we must show that it contains an ordering $\Ov_N$, which is binder-consistent with
some minimal ordering $\Sv$ of $\S_0$.

Let $\Sv'$ be a minimal ordering of $\S_0$, binder-consistent with $N$.
Let $\Ov'_N$ be the projection of $\Sv'$ on $N$.
If $\Ov'_N \in \C(N)$, we are done ($\Ov_N = \Ov'_N$, $\Sv = \Sv'$).
Otherwise, $\Ov'_N \in \pi(\S(N)) \setminus \C(N)$.
$\Ov'_N$ cannot be MC-contradicting (it is min-consistent to $\Sv'$), therefore  
it must be blockwise-equivalent to some $\Ov_N'' \in \C(N)$.
Blocks of $\Ov'_N$ are not violated in $\Sv'$, since $\Sv'$ is minimal
(Corollary~\ref{corollary:block-violated}).
Therefore the substitution $\Sv'' = \Sv'|_{\Ov'_N}^{\Ov_N''}$ is well defined. 
$\Sv''$ is minimal, 
since $\Sv'$ is minimal and $\Ov'_N$ and $\Ov''_N$ are blockwise-equivalent.
$\Sv''$ is binder-consistent with $\Ov''_N$, since $\Sv'$ was binder-consistent
with $\Ov'_N$.
Thereupon $\Sv''$ and $\Ov_N''$ satisfy the requirements of validity
($\Ov_N = \Ov''_N$, $\Sv = \Sv''$).
\hfill $\Box$
\end{proof}

\medskip

\begin{theorem}
\label{theorem:correctness-valid-sets}
\ \\
Let $\S_0$ be a set of subgoals.
For each node $N$ of the \TREE\ of $\S_0$,
\AO\ creates a strongly valid candidate set of orderings.
\end{theorem}

\begin{proof} By induction on the height of $N$'s subtree.
\begin{description}
\item[Inductive base:]
$N$ is a leaf node, which means that $\S(N)$ is independent under $\B(N)$.
The candidate set of $N$ contains one element, whose subgoals are sorted by $cn$.
All orderings that belong to $\pi(\S(N)) \setminus CandSet(N)$
are either not sorted by $cn$,
and hence are MC-contradicting (Lemma~\ref{lemma:contradicting-independent}),
or are sorted by $cn$, 
and hence are blockwise-equivalent to the candidate 
(Corollary~\ref{corollary:independent-sorted-are-equivalent}).
Consequently, $CandSet(N)$ is strongly valid.

\item[Inductive hypothesis:]
For all children of $N$, \AO\ produces strongly valid candidate sets.

\item[Inductive step:]
An internal node in a \TREE\ is either an AND-node or an OR-node.
\begin{enumerate}
\item 
$N$ is an AND-node. 
Let $N_1,N_2,\ldots N_k$ be the children of $N$.
First we show that $ConsSet(N)$ is strongly valid.

Let $\Ov_N \in \pi(\S(N)) \setminus ConsSet(N)$.
For all $1 \leq i \leq k$, let $\Ov_i$ be the projection of $\Ov_N$ on $N_i$.
The set of projections $\{\Ov_1,\Ov_2,\ldots \Ov_k\}$
can belong to one of the three following types, with regard to $\Ov_N$.
\begin{enumerate}
\item
The sets of the first type contain at least one MC-contradicting projection.
In such a case $\Ov_N$ is MC-contradicting too.
Assume the contrary: there exists a minimal ordering $\Sv$ of $\S_0$,
binder-consistent with $\Ov_N$.
Let $\Ov_i$ be an MC-contradicting projection.
Since $\Ov_i$ is consistent with $\Ov_N$, it is also consistent with $\Sv$.
Since $\B(N_i) = \B(N)$, all subgoals of $\B(N_i)$ appear in $\Sv$ before 
subgoals of $\S(N_i)$. Therefore, $\Ov_i$ is binder-consistent with $\Sv$,
and since $\Sv$ is minimal, $\Ov_i$ is min-consistent and 
not MC-contradicting -- a contradiction.

\item
The sets of the second type do not contain MC-contradicting projections,
but in $\Ov_N$ some block of some projection
is violated, or max-blocks from different projections are not ordered by $cn$. 
In such a case, $\Ov_N$ is MC-contradicting, by 
Corollary~\ref{corollary:block-violated} 
and Lemma~\ref{lemma:contradicting-divisible}.

\item
The sets of the third type do not contain MC-contradicting projections,
and max-blocks of the projections are not violated in $\Ov_N$ 
and are sorted by $cn$.

Every projection $\Ov_i$ either belongs to $CandSet(N_i)$, or not.
If $\Ov_i \not\in CandSet(N_i)$, then there exists 
$\Ov'_i \in CandSet(N_i)$ such that $\Ov_i$ is blockwise-equivalent to $\Ov'_i$
(because $CandSet(N_i)$ is strongly valid by the inductive hypothesis,
and $\Ov_i$ is not MC-contradicting). 
If $\Ov_i \in CandSet(N_i)$, we can set $\Ov'_i = \Ov_i$.
%Note that all projections cannot be candidates, since otherwise 
%$\Ov_N \in ConsSet(N)$, by the definition of consistency sets, which leads
%to a contradiction.

Let $\Ov'_N = \Ov_N|_{\Ov_1}^{\Ov_1'}|_{\Ov_2}^{\Ov_2'}\ldots|_{\Ov_k}^{\Ov_k'}$.
This substitution is well defined, since each $\Ov_i$ has the same number of
max-blocks as $\Ov'_i$, and max-blocks of the projections are not violated in $\Ov_N$.
Let $\Sv$ be a minimal ordering of $\S_0$, binder-consistent with $\Ov_N$.
Since $\Sv$ is minimal,  blocks of $\Ov_1$ are not violated in $\Sv$.
Since $\Ov_1$ is blockwise-equivalent to $\Ov_1'$,
the ordering $\Sv_1 = \Sv|_{\Ov_1}^{\Ov_1'}$ is well-defined and minimal.
In $\Sv_1$ the positions of the subgoals from $\B(N)$ did not change; thus,
$\Ov_2$ is min-consistent with $\Sv_1$, and 
blockwise equivalence of $\Ov_2$ and $\Ov_2'$ entails minimality of the ordering
$\Sv_2 = \Sv_1|_{\Ov_2}^{\Ov_2'} = \Sv|_{\Ov_1}^{\Ov_1'}|_{\Ov_2}^{\Ov_2'}$.
We continue with other $\Ov_i$-s, and finally obtain that
$\Sv' = \Sv|_{\Ov_1}^{\Ov_1'}|_{\Ov_2}^{\Ov_2'}\ldots|_{\Ov_k}^{\Ov_k'}$ 
is minimal.
>From the definition of $\Ov'_N$, $\Sv' = \Sv|_{\Ov_N}^{\Ov'_N}$
(note that we introduced blockwise equivalence and strong validity only
to be able to perform this transition).
$\Sv'$ is minimal, therefore $\Ov_N$ is blockwise-equivalent to $\Ov'_N$.
$\Ov'_N \in ConsSet(N)$, since all its projections are candidates of the 
child nodes.
Thereupon, $\Ov_N$ is blockwise-equivalent to a member of $ConsSet(N)$.
\end{enumerate}
So, $ConsSet(N)$ is strongly valid.
To prove that $CandSet(N)$ is strongly valid, it suffices to show that
all the members of $ConsSet(N)$ that are not included in
$CandSet(N)$ by \AO, are either MC-contradicting or
blockwise-equivalent to members of $CandSet(N)$. 
Such orderings can be of three types:
\begin{enumerate}
\item
Orderings that violate blocks of the children projections.
They are MC-contradicting by Corollary~\ref{corollary:block-violated}.
\item
Orderings that do not violate blocks, 
but where max-blocks of children projections are not ordered by $cn$.
They are MC-contradicting by Lemma~\ref{lemma:contradicting-divisible}.
\item
Orderings that do not violate blocks and have them sorted by $cn$.
For each combination of projections, 
one consistent ordering of $N$ is retained in the candidate set,
and all the other are rejected.
By Corollary~\ref{corollary:divisible-sorted-are-equivalent},
the rejected orderings are blockwise-equivalent to the retained candidate.
\end{enumerate}
Consequently, $CandSet(N)$ is strongly valid.


\item
$N$ is an OR-node.
Again, we start with showing that $ConsSet(N)$ is strongly valid.

Let \mbox{$\Ov_N \in \pi(\S(N)) \setminus ConsSet(N)$}.
$\Ov_N$ is constructed from a binder $H$ and a ``tail'' sequence $\Tv$:
\mbox{$\Ov_N = H \cc \Tv$}. 
Let $N_H$ be the child of $N$ that corresponds to the binder $H$.
By the inductive hypothesis, $CandSet(N_H)$ is strongly valid. 
$\Tv \not\in CandSet(N_H)$, since otherwise $\Ov_N \in ConsSet(N)$.
Therefore, $\Tv$ is either MC-contradicting, or 
blockwise-equivalent to some $\Tv' \in CandSet(N_H)$.
If $\Tv$ is MC-contradicting, $\Ov_N$ is MC-contradicting too 
(proof by contradiction, as for AND-nodes).
If $\Tv$ is blockwise-equivalent to $\Tv'$, then
$\Ov_N = H\cc\Tv$ is blockwise-equivalent to $H\cc\Tv' \in ConsSet(N)$
(the proof is easy).
Hence, $ConsSet(N)$ is strongly valid.
The only orderings of $ConsSet(N)$ that are not included in $CandSet(N)$
by the \ALG\ have cheaper permutations of their leading max-blocks,
and therefore are MC-contradicting, 
by Lemma~\ref{lemma:contradicting-indivisible}.
Hence, $CandSet(N)$ is strongly valid.
\hfill $\Box$
\end{enumerate} % AND/OR node
\end{description} % inductive step
\end{proof}

\begin{corollary}
The candidate set found by \AO\ for the root node is valid.
\end{corollary}


\begin{corollary}
\AO\ finds a minimal ordering of the given set of subgoals.
\end{corollary}





\bibliographystyle{theapa}
\bibliography{../../../library/oleg}

\end{document}


