\documentstyle[jair,twoside,11pt,theapa,epic,eepic,times]{article}
\renewcommand{\shortcite}[1]{\citeyear{#1}}

\jairheading{12}{2000}{271-315}{2/00}{5/00}
\ShortHeadings{Compilability and Expressive Power of 
  Planning Formalisms}
{Nebel}
\firstpageno{271}

\title{On the Compilability and Expressive Power \\ of Propositional
  Planning Formalisms}


\author{\name Bernhard Nebel \email nebel@informatik.uni-freiburg.de \\
  \addr Institut f{\"u}r Informatik, Albert-Ludwigs-Universit{\"a}t,
  Georges-K{\"o}hler-Allee, D-79110 Freiburg, Germany}


%% ------------------------- definitions -------------------------

%% -- theorems and such
\newenvironment{proof}{\noindent {\bf Proof.}}%
{\hfill \rule[0.3ex]{1ex}{1ex} \par \addvspace{\bigskipamount}}
\newenvironment{proofsk}{\noindent {\bf Proof Sketch.}}%  
{\hfill \rule[0.3ex]{1ex}{1ex} \par \addvspace{\medskipamount}}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}      
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{example}{Example}

%%-- general typesetting commands
\newcommand{\emdef}{\bf}
\newcommand{\sym}[1]{{\sf #1}}

%%-- layout commands
% used in tables to reposition table entry half a line higher
\newcommand{\raisehalf}[1]{\raisebox{2ex}{#1}}

%%-- planning systems/formalisms
\newcommand{\strips}{{\sc strips}}
\newcommand{\blackbox}{{\sc blackbox}}
\newcommand{\tweak}{{\sc tweak}}
\newcommand{\adl}{{\sc adl}}
\newcommand{\ucpop}{{\sc ucpop}}
\newcommand{\ipp}{{\sc ipp}}
\newcommand{\graphplan}{{\sc graphplan}}
\newcommand{\Graphplan}{{\sc Graphplan}}
\newcommand{\satplan}{{\sc satplan}}
\newcommand{\cps}{{\sc cps}}
\newcommand{\psn}{{\sc psn}}
\newcommand{\gtweak}{{\sc gt}}
\newcommand{\sasplus}{{\sc sas}$^+$}

\newcommand{\BOOL}{${\cal B}$}
\newcommand{\LITERALS}{${\cal L}$}
\newcommand{\INCOMPLETE}{${\cal I}$}
\newcommand{\CONDITIONAL}{${\cal C}$}
\newcommand{\STRIPS}{${\cal S}$}
\newcommand{\PL}{{${\cal S_{BIC}}$}}
\newcommand{\PLu}{{$\cal S_{BI}$}}
\newcommand{\PLc}{{$\cal S_{BC}$}}
\newcommand{\PLl}{{$\cal S_{LIC}$}}
\newcommand{\classPLl}{{$[\cal S_{LIC}]$}}
\newcommand{\PLa}{{$\cal S_{IC}$}}
\newcommand{\PLuc}{{$\cal S_{B}$}}
\newcommand{\PLul}{{$\cal S_{LI}$}}
\newcommand{\PLlu}{\PLul}
\newcommand{\classPLlu}{{$[\cal S_{LI}]$}}
\newcommand{\PLlc}{{$\cal S_{LC}$}}
\newcommand{\PLac}{{$\cal S_{C}$}}
\newcommand{\PLau}{{$\cal S_{I}$}}
\newcommand{\PLluc}{{$\cal S_{L}$}}
\newcommand{\PLauc}{{$\cal S$}}
%\newcommand{\plc}{{$\cal C$}}
%\newcommand{\plu}{{$\cal U$}}
%\newcommand{\pll}{{$\cal L$}}
%\newcommand{\pla}{{$\cal A$}}

\newcommand{\spec}{\sqsubseteq}


%%-- logical symbols
\newcommand{\atomalph}{\Sigma}
\newcommand{\allatoms}{{\bf \atomalph}}
\newcommand{\allatomssubset}{{\bf S}}
\newcommand{\propatomalph}{{P}}
\newcommand{\literals}[1]{\widehat{#1}}
\newcommand{\litalph}{\literals{\atomalph}}
\newcommand{\alphabet}[1]{\sigma{#1}}
\newcommand{\loglang}{{\cal L}_{\atomalph}}
\newcommand{\litset}{L}
\newcommand{\litsetm}{K}
\newcommand{\nl}[1]{{\it neg}(#1)}
\newcommand{\pl}[1]{{\it pos}(#1)}
\newcommand{\negated}[1]{\neg #1}
\newcommand{\atomvar}{p}
\newcommand{\atomvarq}{q}
\newcommand{\atomvaru}{u}
\newcommand{\atomvarv}{v}
\newcommand{\atomvarx}{x}
\newcommand{\litvar}{l}
\newcommand{\powerset}[1]{{\bf 2}^{#1}}
\newcommand{\formulaset}{{\Gamma}}
\newcommand{\trans}{\theta}
\newcommand{\formula}{\varphi}
\newcommand{\Formula}{\Phi}
\newcommand{\formulaq}{\psi}
\newcommand{\subformula}{\psi}
\newcommand{\Subformula}{\Psi}
\newcommand{\subformulaq}{\gamma}
\newcommand{\truth}{\top}
\newcommand{\falsity}{\bot}
\newcommand{\mod}[1]{{\it Mod}(#1)}
\newcommand{\copysym}[1]{\widetilde{#1}}
\newcommand{\copyksym}[1]{#1'}
\newcommand{\copyaddksym}[1]{#1_{+}}
\newcommand{\copydelksym}[1]{#1_{-}}
\newcommand{\copyneg}{\sim\!}
\newcommand{\scopy}[1]{#1^{\#}}
\newcommand{\cwa}{{\it CWA}}
\newcommand{\clauseset}{{\bf C}}
\newcommand{\allclauses}{{\bf A}}
\newcommand{\allclausealph}{{\bf D}}


%% -- planning related symbols
\newcommand{\univlits}{{\bf U}}
\newcommand{\planfx}{{\cal X}}
\newcommand{\planfy}{{\cal Y}}
\newcommand{\statespec}{S}
\newcommand{\state}{s}
\newcommand{\pre}{\mbox{\it pre}}
\newcommand{\post}{\mbox{\it post}}
\newcommand{\block}{\mbox{\it block}}
\newcommand{\test}{\mbox{\it test}}
\newcommand{\res}{{\it R}}
\newcommand{\Result}{{\it Res}}
\newcommand{\opset}{{\bf O}}
\newcommand{\goal}{{\bf G}}
\newcommand{\initial}{{\bf I}}
\newcommand{\newinitial}{{\bf J}}
\newcommand{\effimpl}{\Rightarrow}
\newcommand{\Eff}{{\it A}}
\newcommand{\Pot}{{\it P}}
\newcommand{\op}{o}
\newcommand{\plan}{{\Delta}}
\newcommand{\domainstructure}{{\Xi}}
\newcommand{\domainstructuretuple}{\langle\atomalph,\opset\rangle}
\newcommand{\planinstance}{{\Pi}}
\newcommand{\planinstancetuple}{\langle\domainstructure,\initial,\goal\rangle}
\newcommand{\famdom}{{\bf \Xi}}
\newcommand{\seq}[1]{#1^{\star}}
\newcommand{\size}[1]{||#1||}
\newcommand{\card}[1]{|#1|}
\newcommand{\cons}{\mbox{\it cons}}
\newcommand{\testop}{\mbox{\it test}}
\newcommand{\newgoal}{g}
\newcommand{\opcons}{o_g}
\newcommand{\unknownset}{\Upsilon}
\newcommand{\unknownfun}{U}
\newcommand{\unknownlitfun}{\upsilon}
\newcommand{\choiceset}{{\bf P}}
\newcommand{\choice}{P}
\newcommand{\chosenset}{{\bf Q}}
\newcommand{\copying}{c}
\newcommand{\msucc}{s}
\newcommand{\cycle}{c}

%% -- complexity classes & problems & compilation functions 
\newcommand{\classX}{{\sf X}}
\newcommand{\PH}{{\sf PH}}
\newcommand{\Poly}{{\sf P}}
\newcommand{\NP}{{\sf NP}}
\newcommand{\PSPACE}{{\sf PSPACE}}
\newcommand{\coNP}{{\sf coNP}}
\newcommand{\instance}{I}
\newcommand{\advice}{a}
\newcommand{\poly}{{\sf poly}}
\newcommand{\Ppoly}{{\sf P/poly}}
\newcommand{\NPpoly}{{\sf NP/poly}}
\newcommand{\coNPpoly}{{\sf coNP/poly}}
\newcommand{\NC}{{\sf NC}}
\newcommand{\NCone}{{\sf NC}$^1$}
\newcommand{\AC}{{\sf AC}}
\newcommand{\ACzero}{{\sf AC}$^0$}
\newcommand{\DLOGTIME}{{\sf DLOGTIME}}
\newcommand{\planex}{{\sc planex}}
%\newcommand{\fisex}{{\sc fisex}}
%\newcommand{\sat}{{\sc sat}}
%\newcommand{\threesat}{{\sc 3sat}}
%\newcommand{\cnfsat}{{\sc cnf-sat}}
\newcommand{\comp}{F}
\newcommand{\compfun}{{\bf f}}
\newcommand{\compdsfun}{f_{\xi}}
\newcommand{\compifun}{f_{i}}
\newcommand{\compgfun}{f_{g}}
\newcommand{\transfun}{t}
\newcommand{\transifun}{t_{i}}
\newcommand{\transgfun}{t_{g}}
\newcommand{\transxfun}{t_{x}}
\newcommand{\compfuntuple}{\langle
  \compdsfun,\compifun,\compgfun,\transifun,\transgfun\rangle}
\newcommand{\compilable}{\preceq}
\newcommand{\red}{r}
\newcommand{\word}{w}
\newcommand{\circuit}{C}
\newcommand{\famcircuits}{{\bf C}}
\newcommand{\edges}{E}
\newcommand{\vertices}{V}
\newcommand{\node}{v}
\newcommand{\gtype}{{\it type}}
\newcommand{\var}{x}

%% -- knowledge compilation
\newcommand{\problem}{P}
\newcommand{\problemq}{Q}
\newcommand{\fixedpart}{f}
\newcommand{\varyingpart}{v}
\newcommand{\askalg}{{\em ASK}}
\newcommand{\datafixed}{D_f}

%% ------------------------- end of definitions -------------------------

\begin{document}
\maketitle


\begin{abstract}
  The recent approaches of extending the \graphplan{} algorithm to handle more
  expressive planning formalisms raise the question of what the formal meaning
  of ``expressive power'' is. We formalize the intuition that expressive power
  is a measure of how concisely planning domains and plans can be expressed in
  a particular formalism by introducing the notion of ``compilation schemes''
  between planning formalisms.  Using this notion, we analyze the
  expressiveness of a large family of propositional planning formalisms,
  ranging from basic \strips{} to a formalism with conditional effects,
  partial state specifications, and propositional formulae in the
  preconditions.  One of the results is that conditional effects cannot be
  compiled away if plan size should grow only linearly but can be compiled
  away if we allow for polynomial growth of the resulting plans. This result
  confirms that the recently proposed extensions to the \graphplan{} algorithm
  concerning conditional effects are optimal with respect to the
  ``compilability'' framework.  Another result is that general propositional
  formulae cannot be compiled into conditional effects if the plan size should
  be preserved linearly.  This implies that allowing general propositional
  formulae in preconditions and effect conditions adds another level of
  difficulty in generating a plan.
\end{abstract}


\section{Introduction}

\Graphplan{} \cite{blum:furst:ai-97} and \satplan{}
\cite{kautz:selman:aaai-96} are among the most efficient planning systems
nowadays.  However, it is generally felt that the planning formalism
supported by these systems, namely, propositional basic \strips{}
\cite{fikes:nilsson:ai-71}, is not {\em expressive} enough. For this
reason, much research effort
\cite{anderson:et:al:aips-98,gazen:knoblock:ecp-97,kambhampati:et:al:ecp-97,koehler:et:al:ecp-97}
has been devoted in extending \graphplan{} in order to handle more powerful
planning formalisms such as \adl{} \cite{pednault:kr-89}.

There appears to be a consensus on how much {\em expressive power} is
added by a particular language feature.  For example, everybody seems
to agree that adding negative preconditions does not add very much to
the expressive power of basic \strips, whereas conditional effects are
considered as a significant increase in expressive power
\cite{anderson:et:al:aips-98,gazen:knoblock:ecp-97,kambhampati:et:al:ecp-97,koehler:et:al:ecp-97}.
However, it is unclear how to measure the expressive power in a more
formal way.  Related to this problem is the question of whether
``compilation'' approaches to extend the expressiveness of a planning
formalism are optimal.  For example, Gazen and Knoblock
\shortcite{gazen:knoblock:ecp-97} propose a particular method of
compiling operators with conditional effects into basic \strips{}
operators. This method, however, results in exponentially larger
operator sets.  While most people
\cite{anderson:et:al:aips-98,kambhampati:et:al:ecp-97,koehler:et:al:ecp-97}
agree that we cannot do better than that, nobody has proven yet that a
more space-efficient method is impossible.

In order to address the problem of measuring the relative expressive
power of planning formalisms, we start with the intuition that a
formalism $\planfx$\label{D:planfx} is {\em at least as expressive} as another
formalism $\planfy$ if {\em planning domains} and the corresponding
{\em plans} in formalism $\planfy$ can be {\em concisely expressed} in
the formalism $\planfx$. This, at least, seems to be the underlying
intuition when expressive power is discussed in the planning
literature.

\begin{sloppypar}
B\"ackstr\"om \shortcite{backstrom:ai-95} proposed to measure the
expressiveness of planning formalisms using his {\em ESP-reductions}.
These reductions are, roughly speaking, polynomial many-one
reductions\footnote{We assume that the reader has a basic knowledge of
  complexity theory \cite{garey:johnson:79,papadimitriou:94}, and is
  familiar with the notion of {\em polynomial many-one reductions} and
  the {\em complexity classes} \Poly,\label{D:Poly} \NP,\label{D:NP} \coNP,\label{D:coNP} and \PSPACE\label{D:PSPACE}. All
  other notions will be introduced in the paper when needed.}  on
planning instances that {\em do not change the plan length}.  Using
this notion, he showed that all of the propositional variants of basic
\strips{} not containing conditional effects or arbitrary logical
formulae can be considered as expressively equivalent.  However,
taking our point of view, ESP-reductions are too restrictive for two
reasons. Firstly, plans must have identical size, while we might want
to allow a moderate growth.  Secondly, requiring that the
transformation can be computed in polynomial time is overly
restrictive. If we ask for how concisely something can be {\em
  expressed}, this does not necessarily imply that there exists a
polynomial-time transformation.  In fact, one formalism might be as
expressive as another one, but the mapping between the formalisms
might not be computable at all. This, at least, seems to be the
usual assumption made when the term {\em expressive power} is discussed
\cite{baader:ecai-90,cadoli:et:al:kr-96,erol:et:al:amai-96,gogic:et:al:ijcai-95}. 
\end{sloppypar}

Inspired by recent approaches to measure the expressiveness of
knowledge representation formalisms
\cite{cadoli:et:al:kr-96,gogic:et:al:ijcai-95}, we propose to address
the questions of how expressive a planning formalism is by using the
notion of {\em compiling} one planning formalism into another one. A
compilation scheme from one planning formalism to another differs from
a polynomial many-one reduction in that it is not required that the
compilation is carried out in polynomial time. However, the result
should be expressible in polynomial space.  Furthermore, it is
required that the operators of the planning instance can be translated
{\em without} considering the initial state and the goal. While this
restriction might sound unnecessarily restrictive, it turns out that
existing practical approaches to compilation
\cite{gazen:knoblock:ecp-97} as well as theoretical approaches
\cite{backstrom:ai-95} consider only {\em structured} transformations
where the operators can be transformed independently from the initial
state and the goal description. From a technical point of view this
restriction guarantees that compilations are non-trivial. If the
entire instance could be transformed, a compilation scheme could
decide the existence of a plan for the source instance and then
generate a small solution-preserving instance in the target formalism,
which would lead to the unintuitive conclusion that all planning
formalisms have the same expressive power.

As mentioned in the beginning, not only the space taken up by the domain
structure is important, but also the space used by the plans. For this reason,
we distinguish between compilation schemes in whether they preserve plan size
{\em exactly}, {\em linearly}, or {\em polynomially}.

Using the notion of {\em compilability}, we analyze a wide range of
propositional planning formalisms, ranging from basic \strips{} to a
planning formalism containing {\em conditional effects}, {\em
  arbitrary boolean formulae}, and {\em partial state specifications}.
As one of the results, we identify two equivalence classes of planning
formalisms with respect to {\em polynomial-time} compilability
preserving plan size exactly. This means that adding a language
feature to a formalism without leaving the class does not increase the
expressive power and should not affect the principal efficiency of the
planning method. However, we also provide results that {\em separate}
planning formalisms using results from computational complexity theory
on circuit complexity and non-uniform complexity classes. Such
separation results indicate that adding a particular language feature
adds to the expressive power and to the difficulty of integrating the
feature into an existing planning algorithm.
For example, we prove that conditional effects cannot be compiled away
and that boolean formulae cannot be compiled into conditional
effects---provided the plans in the target formalism are allowed to
grow only linearly.

This answers the question posed in the beginning. The compilation
approach proposed by Gazen and Knoblock
\shortcite{gazen:knoblock:ecp-97} cannot be more space efficient, even
if we allow for linear growth of the plans in the target
formalism.\footnote{Note that Gazen and Knoblock's
  \shortcite{gazen:knoblock:ecp-97} translation scheme also generates
  planning operators that depend on the initial state and the goal
  description. However, these operators simply code the initial state
  and the goal description and do nothing else. For this reason, we
  can ignore them here.}  Allowing for polynomial growth of the plans,
however, the compilation scheme can be more space efficient.
Interestingly, it seems to be the case that a compilation scheme that
allows for polynomially larger plans is similar to the implementation
of conditional effects in the \ipp{} system
\cite{koehler:et:al:ecp-97}, Kambhampati and colleagues' 
\shortcite{kambhampati:et:al:ecp-97} planning system, and Anderson
and colleagues'  \shortcite{anderson:et:al:aips-98} planning system.

The rest of the paper is structured as follows. In
Section~\ref{S:formalisms}, we introduce the range of propositional
planning formalisms analyzed in this paper together with general
terminology and definitions. Based on that, we introduce the notion of
compilability between planning formalisms in
Section~\ref{S:compilability}. In Section~\ref{S:linear:compilability}
we present polynomial-time compilation schemes between different
formalisms that preserve the plan size exactly, demonstrating that
these formalisms are of identical expressiveness. For all of the
remaining cases, we prove in Section~\ref{S:uncompilability} that
there cannot be any compilation scheme preserving plan size linearly,
even if there are no bounds on the computational resources of the
compilation process.  In Section~\ref{S:polynomial:compilability} we
reconsider the question of identical expressiveness by using
compilation schemes that allow for polynomial growth of the plans.
Finally, in Section~\ref{S:conclusions} we summarize and discuss the
results.


\section{Propositional Planning Formalisms}
\label{S:formalisms}

First, we will define a very general propositional planning formalism, which
appears almost as expressive as the propositional variant of \adl{}
\cite{pednault:kr-89}. This formalism allows for arbitrary boolean formulae
as preconditions, conditional effects and partial state specifications.
Subsequently, we will specialize this formalism by imposing different
syntactic restrictions.

\subsection{A General Propositional Planning Formalism}
\label{S:P:formalism}

Let $\allatoms$\label{D:allatoms} be the countably infinite set of {\emdef propositional atoms}
or {\emdef propositional variables}.  Finite subsets of $\allatoms$ are
denoted by $\atomalph$.\label{D:atomalph} Further, $\litalph$\label{D:litalph} is defined to be the set
consisting of the constants $\truth$\label{D:truth} (denoting truth) and $\falsity$\label{D:falsity} (denoting
falsity) as well as atoms and negated atoms, i.e., the {\emdef literals}, over
$\atomalph$.  The {\emdef language of propositional logic} over the logical
connectives $\wedge, \vee$, and $\neg$ and the propositional atoms $\atomalph$
is denoted by $\loglang$.\label{D:loglang}  A {\emdef clause} is a disjunction of literals.
Further, we say that a formula $\formula \in \loglang$\label{D:formula} is in {\emdef
  conjunctive normal form} (CNF) if it is a conjunction of clauses. It is in
{\emdef disjunctive normal form} (DNF) if it is a disjunction of conjunctions
of literals.

Given a set of literals $\litset$,\label{D:litset} by $\pl{\litset}$\label{D:pl} we refer to the {\emdef
  positive literals} in $\litset$, by $\nl{\litset}$\label{D:nl} we refer to the {\emdef
  negative literals} in $\litset$, and by $\alphabet(\litset)$\label{D:alphabet} to the atoms
used in $\litset$, i.e., $\alphabet(\litset) = \{ \atomvar \in \atomalph \: |
\: \atomvar \in \litset \mbox{\ or\ } \neg \atomvar \in \litset\}$.\label{D:atomvar}  Further,
we define $\negated{\litset}$ to be the {\emdef element-wise negation} of
$\litset$, i.e.,
\[ \negated{\litset} = \{ \atomvar\:|\:\neg \atomvar \in \litset \} \cup
\{ \neg \atomvar\:|\:\atomvar \in \litset \}.\]

A {\emdef state} $\state$\label{D:state} is a {\em truth-assignment} for the atoms in
$\atomalph$. In the following, we also identify a state with the set of atoms
that are true in this state.  A {\emdef state specification} $\statespec$\label{D:statespec} is a
subset of $\litalph$, i.e., it is a {\em logical
  theory} consisting of literals only. It is called {\emdef consistent} iff it
does not contain complementary literals or $\falsity$.  In general, a state
specification describes many states, namely all those that satisfy
$\statespec$, which are denoted by $\mod{\statespec}$.\label{D:mod} Only in case that
$\statespec$ is {\emdef complete}, i.e., for each $\atomvar \in \atomalph$ we
have either $\atomvar \in \statespec$ or $\neg \atomvar \in \statespec$,
$\statespec$ has precisely one model, namely $\pl{\statespec}$.  By abusing
notation, we will refer to the {\emdef inconsistent} state specification by
$\falsity$,\label{D:illegal:state} which is the {\emdef ``illegal'' state specification}.

{\emdef Operators} are pairs $\op = \langle \pre, \post \rangle$.\label{D:op}
We use the notation $\pre(\op)$\label{D:pre} and $\post(\op)$\label{D:post} to
refer to the first and second part of an operator $\op$, respectively.
The {\emdef precondition} $\pre$ is an element of
$\powerset{\loglang}$, i.e., it is a set of propositional formulae.
The set $\post$, which is the set of {\emdef postconditions},
consists of {\emdef conditional effects}, each having the form\label{D:effimpl}
\[ \formulaset \effimpl \litset, \]
where the elements of $\formulaset \subseteq {\loglang}$\label{D:formulaset} are called {\emdef effect conditions}
and the elements of $\litset \subseteq
{\litalph}$ are called {\emdef effects}. If $\formulaset$ or $\litset$
are singleton sets, e.g., $\{\atomvar\} \effimpl \{\atomvarq\}$, we
often omit the curly brackets and write $\atomvar \effimpl \atomvarq$.

\begin{example}
\label{Ex:1}
In order to illustrate the various notions, we will use as a running
example planning problems connected with the production of camera-ready
manuscripts from  
\LaTeX{} source files---somewhat simplified, of course.
As the set of atoms $\atomalph$, we choose the following set:
\[ \atomalph = \{ \!\! \begin{array}[t]{l} \sym{tex}, \sym{aux},  \sym{dvi}, \sym{log}, \sym{ps}, \sym{bib}, \sym{bbl},
\sym{blg}, \sym{ind}, \sym{idx}, \sym{ilg} \\
\sym{dvi\_ind\_ok}, \sym{dvi\_cite\_ok}\}. \end{array}
\]
These propositional atoms have the following intended meaning. The atoms in
the first line represent the presence of the corresponding files, and the
atoms in the second line signify that the index and citations are correct in
the dvi-file.  Based on that, we define the following
operators: $\sym{bibtex}$, $\sym{latex}$, $\sym{makeindex}$.
The first of these operators is very simple. The precondition for its
execution is that a $\sym{bib}$- and an $\sym{aux}$-file exist. After the successful
execution, a $\sym{bbl}$- and a $\sym{blg}$-file will have been produced:
\[ \sym{bibtex}  =  \Bigl\langle \Bigl\{ \sym{aux}, \sym{bib} \Bigr\},
\Bigl\{ \truth \effimpl \{ \sym{bbl}, \sym{blg}\} \Bigr\}\Bigr\rangle.\]
The $\sym{makeindex}$ operator is similar:
\[ \sym{makeindex}  =  \Bigr\langle \Bigl\{ \sym{idx} \Bigr\}, \Bigl\{
\truth \effimpl \{ \sym{ind}, \sym{ilg}\} \Bigr\}\Bigr\rangle. \] Finally, the
$\sym{latex}$ operator is a bit more complicated. As a precondition it needs
the presence of the $\sym{tex}$-file and it produces as its effect
$\sym{aux}$-, $\sym{idx}$-, $\sym{dvi}$, and $\sym{log}$-files
unconditionally. In addition, we know that the citations will be correct if a
$\sym{bbl}$-file is present and that the index will be correct if an
$\sym{ind}$-file is present:
\[ \sym{latex}  =  \Bigl\langle \!\! \begin{array}[t]{l}
  \Bigl\{ \sym{tex} \Bigr\}, \\
  \Bigl\{ \!\! \begin{array}[t]{l}
    \truth \effimpl \{ \sym{aux}, \sym{idx}, \sym{dvi}, \sym{log} \}, \\
    \sym{bbl} \effimpl \sym{dvi\_cite\_ok}, \\
    \neg     \sym{bbl} \effimpl \neg \sym{dvi\_cite\_ok}, \\
    \sym{ind} \effimpl \sym{dvi\_ind\_ok}, \\
    \neg \sym{ind} \effimpl \neg \sym{dvi\_ind\_ok}
  \Bigr\} \Bigr\rangle.
  \end{array}
  \end{array}
\]
\end{example}

The semantics of operators is given by {\em state-transition
  functions}, i.e., mappings from states to states. Given a state
$\state$ and a set of postconditions $\post$,
$\Eff(\state,\post)$\label{D:Eff:state} denotes the {\emdef active
  effects} in $\state$:
\[ \Eff(\state,\post) = \bigcup \{ \litset\:|\:(\formulaset \effimpl \litset)
\in \post, \state \models \formulaset\}. \]
The {\emdef state-transition function} $\trans_{\op}$ induced by the
operator $\op$ is defined as follows:
\begin{eqnarray*}
\trans_{\op}\colon & & \powerset{\atomalph}  \rightarrow 
{\powerset{\atomalph}} \\
 \trans_{\op}(\state) & = & \left\{\begin{array}{ll}
\state - \negated{\nl{\Eff(\state,\post(\op))}} \cup \pl{\Eff(\state,\post(\op))}
& \mbox{if } \state \models \pre(\op) 
\mbox{\ and } \\
& \Eff(\state,\post(\op)) \not\models \falsity \\
\mbox{undefined} & \mbox{otherwise}
\end{array}\right.
\end{eqnarray*}
In words, if the precondition of the operator is satisfied in 
state $\state$ and the active effects are consistent, 
then state $\state$ is mapped to the state $\state'$ which differs
from $\state$ in that the truth values of {\em active effects} are
forced to become true for positive effects and forced to become false
for negative effects. If the precondition is not satisfied or the set of
active effects is inconsistent, the
result of the function is undefined.

In the planning formalism itself, we do not work on states but on {\em state
  specifications}. In general, this can lead to
semantic problems.  By restricting ourselves to state specifications that are
sets of literals, however, the syntactic manipulations of the state
specifications can be defined in a way such that they are {\em sound}
in Lifschitz' 
\shortcite{lifschitz:raap-86} sense.

\begin{sloppypar}
Similarly to the active effects with respect to states,  we define 
a corresponding function with respect to state specifications:
\[ \Eff(\statespec,\post) = \bigcup \{ \litset\:|\:(\formulaset \effimpl \litset)
\in \post, \statespec \models \formulaset\}.\label{D:Eff:state:specification} \]
Further, we define the {\emdef potentially active effects} as follows:
\[ \Pot(\statespec,\post) = \bigcup_{\state \models \statespec} \Eff(\state,\post).\label{D:Pot} \]
If for a state specification $\statespec$ and an operator $\op =
\langle \pre,\post \rangle$, we have $\Eff(\statespec,\post) \neq
\Pot(\statespec,\post)$,\footnote{Note that this can only happen if
  the state specification is incomplete.} it means that the state
specification resulting from the application of the state-transition
functions might not be representable as a theory consisting of
literals only.  For this reason, we consider such an operator
application as illegal, resulting in the illegal state specification
$\falsity$. We could be more liberal at this point and consider an
operator application to a state specification only as illegal if the
set of states resulting from applying the state-transition functions
could definitely not be represented as a theory consisting of literals
only.  Alternatively, we could consider all atoms mentioned in
$\Pot(\statespec,\post) - \Eff(\statespec,\post)$ as ``unsafe'' after
the application of the operator and delete the literals
$\neg(\Pot(\statespec,\post) - \Eff(\statespec,\post))$ from the state
specification, but consider the resulting state specification still as
``legal'' if  $\Pot(\statespec,\post)$ is consistent. Since there
does not seem to exist a standard model for the execution of
conditional effects in the presence of partial state specifications,
we adopt the first alternative as one arbitrary choice. It should be
noted, however, that this decision influences some of the results we
present below.
\end{sloppypar}

Similarly to the rule that $\Eff(\statespec,\post) \neq
\Pot(\statespec,\post)$ leads to an illegal state specification, we require that if the
precondition is not satisfied by all states in $\mod{\statespec}$ or if the
state specification is already inconsistent, the result of applying $\op$ to
$\statespec$ results in $\falsity$. This leads to the definition of the
function $\res$,\label{D:res} which defines the outcome of applying an operator $\op$ from
the set of operators $\opset$\label{D:opset} to a state specification:
\begin{eqnarray*}
\res \colon & \!\!\!\!\!\! & \powerset{\litalph} \times \opset  \rightarrow 
 \powerset{\litalph} \\
 \res(\statespec,\op) & \!\!\! = \!\!\! & \left\{\!\!\begin{array}{ll}\statespec -
 \negated{\Eff(\statespec,\post(\op))} \cup \Eff(\statespec,\post(\op))
& \!\!\!\begin{array}[t]{l}
 \mbox{if } \statespec \not\models \falsity \mbox{\ and} \\
 \statespec \models \pre(\op) \mbox{\ and\ }\\
  \Eff(\statespec,\post(\op)) \not\models \falsity \mbox{\ and} \\
  \Eff(\statespec,\post(\op)) \!\!=\!\!  \Pot(\statespec,\post(\op)) \\
\mbox{}
\end{array} \\
\falsity & \!\!\! \begin{array}{l} \mbox{otherwise} \end{array}
\end{array}\right.
\end{eqnarray*}

\begin{example}
\label{Ex:2}
Using the propositional atoms and operators from Example~\ref{Ex:1},
we assume the following two state specifications $\sym{S}_1 = \{
\sym{tex}, \sym{ind} \}$, and $\sym{S}_2 = \{ \sym{tex}, \sym{ind},
\sym{bbl}, \sym{blg} \}$. If we try to apply the operator
$\sym{latex}$ to $\sym{S}_1$, we notice that this results in
$\falsity$ because 
\begin{eqnarray*}
\Eff(\sym{S}_1,\post(\sym{latex})) & = & \{ \sym{aux}, \sym{idx}, \sym{dvi}, \sym{log}, \sym{dvi\_ind\_ok} \}, \\
\Pot(\sym{S}_1,\post(\sym{latex})) & = & \Eff(\sym{S}_1,\post(\sym{latex}))
  \cup \{ 
  \sym{dvi\_cite\_ok}, \neg \sym{dvi\_cite\_ok} \},
\end{eqnarray*}
i.e., we have $\Eff(\sym{S}_1,\post(\sym{latex})) \neq
\Pot(\sym{S}_1,\post(\sym{latex})).$ On the other hand, we can apply
$\sym{bibtex}$ successfully to $\sym{S}_1$:
$\res(\sym{S}_1,\sym{bibtex}) = \sym{S}_2.$ 
\end{example}

It is easily verified that the syntactic operation on a state
specification using the function $\res$ corresponds to state
transitions on the states described by the specification.

\begin{proposition}
Let $\statespec$ be a state specification, $\op$ be an
operator, and $\trans_{\op}$ be the induced state-transition function.
If $\res(\statespec,\op) \not\models \falsity$, then 
\[ \mod{\res(\statespec,\op)} =  \{ \state'\:|\: \state' = \trans_{\op}(\state),
\state \models \statespec \}.\]
If $\res(\statespec,\op) \models \falsity$, then either
\begin{enumerate}
\item $\mod{\statespec} = \emptyset$, or
\begin{sloppypar}
\item there are two states $\state_1, \state_2 \in \mod{\statespec}$ such
  that $\Eff(\state_1,\post(\op)) \neq \Eff(\state_2,\post(\op))$, or
\end{sloppypar}
\item there exists a state $\state \in \mod{\statespec}$ such that $\trans_{\op}(\state)$ is undefined.
\end{enumerate}
\end{proposition}
In other words, whenever $\res(\statespec,\op)$ results in a ``legal''
specification, this specification describes the states that result from the
application of the state-transition function $\trans_{\op}$
to the states that satisfy the
original state specification $\statespec$. Further, if $\res(\statespec,\op)$
is illegal, there are good reasons for it.

A  {\emdef planning instance} is a tuple
\[ \planinstance = \planinstancetuple,\label{D:planinstance} \]
where 
\begin{itemize}
\item $\domainstructure = \domainstructuretuple$\label{D:domainstructure} is the {\emdef domain
    structure} consisting of a finite set of propositional atoms $\atomalph$
  and a finite set of operators $\opset$,
\item $\initial \subseteq \litalph$\label{D:initial} is the {\emdef initial state
    specification}, and
\item $\goal \subseteq \litalph$\label{D:goal} 
 is the {\emdef goal
    specification}.\footnote{We could have been more liberal requiring
    that $\goal \subseteq \loglang$. We have not done that in order to allow
    for a ``fair'' comparison with restricted planning
    formalisms.}
\end{itemize}
When we talk about the {\emdef size of an instance}, symbolically
$\size{\planinstance}$,\label{D:size} in the following, we mean the size of a (reasonable)
encoding of the instance.

In the following, we use the notation $\seq{\opset}$\label{D:seq:opset}{} to refer to the {\emdef 
set of finite sequences} of operators. Elements $\plan$\label{D:plan}{} of $\seq{\opset}$ are
called {\emdef plans}. Then $\size{\plan}$ denotes the size
of the plan, i.e., the number of operators in $\plan$. We say that $\plan$ is
a {\emdef $c$-step plan} if $\size{\plan} \leq c$.  The result of applying $\plan$ to a
state specification $\statespec$ is recursively defined as follows:\label{D:Result}
\begin{eqnarray*}
\Result\colon & & \powerset{\litalph} \times \seq{\opset} \rightarrow
\powerset{\litalph} \\
\Result(\statespec,\langle \rangle) & = & \statespec \\
\Result(\statespec,\langle \op_1, \op_2, \ldots, \op_n \rangle) & = &
\Result(\res(\statespec,\op_1), \langle \op_2, \ldots, \op_n\rangle)
\end{eqnarray*}
A sequence of operators $\plan$ is said to be a {\emdef plan for
  $\planinstance$} or a {\emdef solution of $\planinstance$} iff 
\begin{enumerate}
\item $\Result(\initial,\plan) \not\models \falsity$ and
\item $\Result(\initial,\plan) \models \goal$.
\end{enumerate}

\begin{example}
\label{Ex:3}
Let $\atomalph$ and $\opset$ be the propositional atoms and operators
introduced in Example~\ref{Ex:1} and consider the following planning
instance: $\planinstance=\langle \langle \atomalph, \opset\rangle, \{ \sym{tex}, \sym{bib},
\neg \sym{ind} 
\}, \{\sym{dvi}, \sym{dvi\_cite\_ok}\}\rangle.$
In words, given a latex source file ($\sym{tex}$) and a bibliography
database ($\sym{bib}$), we want to generate a dvi file ($\sym{dvi}$)
such that the citations in this file are correct
($\sym{dvi\_cite\_ok}$). Furthermore, we do not know anything about
the existence of a bbl-file or aux-file etc., but we know that there
is no index file yet ($\neg \sym{ind}$). The plan 
$\plan = \langle \sym{bibtex}, \sym{latex} \rangle$ is a solution of
$\planinstance$ because the plan does not result in an illegal state
specification and
the resulting state specification entails $\sym{dvi}$ and
$\sym{dvi\_cite\_ok}$. 
\end{example}

Plans satisfying (1) and (2) above are ``sound.'' In order to state
this more precisely, we extend the notion of state transition
functions for operators to state transition functions for plans.  Let
$\trans_{\plan}$ be the state transition function corresponding to the
composition of primitive state-transition functions induced by the
operators in $\plan = \langle \op_1, \ldots, \op_n\rangle$, i.e.,
\begin{eqnarray*}
\trans_{\langle\op_1,\ldots,\op_n\rangle} & = & \trans_{\op_1} \circ \ldots \circ \trans_{\op_n},
\end{eqnarray*}
such that $\trans_{\langle\op_1,\ldots,\op_n\rangle}(s)$ is defined iff
$\trans_{\langle\op_1,\ldots,\op_i\rangle}(s)$ is defined for every $i$, $1 \leq i
\leq n$. Using this notion, one can easily prove---using induction over the
plan length---that any plan for an instance $\planinstance$ is {\emdef
  sound} in Lifschitz' \shortcite{lifschitz:raap-86} sense, i.e., corresponds
to the application of state transition functions to the initial states.

\begin{proposition}
\begin{sloppypar}
Let $\planinstance = \planinstancetuple$ be a
planning instance and $\plan = \langle \op_1, \ldots, \op_n\rangle$ be an
element of $\seq{\opset}$. If $\Result(\initial,\plan)$
is consistent, then
\[ \mod{\Result(\initial,\plan)} = \{\state' \:|\: \state' =
\trans_{\plan}(\state), \state \models \initial\}. \] 
If
$\Result(\initial,\plan)$ is inconsistent, then either 
\begin{enumerate}
\item $\mod{\initial} = \emptyset$, or
\item there exists a (possibly empty) prefix $\langle \op_1, \ldots, \op_i
  \rangle$ ($0 \leq i \leq n-1$) of $\plan$ such that $\statespec =
  \Result(\initial,\langle \op_1,\ldots,\op_i\rangle)$ and either
\begin{enumerate}
\item there are two states $\state_1, \state_2 \in \mod{\statespec}$ such
  that $\Eff(\state_1,\post(\op_{i+1})) \neq \Eff(\state_2,\post(\op_{i+1}))$, or
\item there exists a state $\state \in \mod{\statespec}$ such that $\trans_{\op_{i+1}}(\state)$ is undefined.
\end{enumerate}
\end{enumerate}
\end{sloppypar}
\end{proposition}


\subsection{A Family of Propositional Planning Formalisms}

The propositional variant of standard \strips{} \cite{fikes:nilsson:ai-71},
which we will also call \STRIPS\label{D:STRIPS}{} in what follows, is a planning formalism
that requires {\em complete state specifications}, {\em unconditional
  effects}, and {\em propositional atoms} as formulae in the precondition
lists. Less restrictive planning formalisms can have the following additional
features:
\begin{description}
\item[Incomplete state specifications (\INCOMPLETE):] The state
  specifications may not be complete.
\item[Conditional Effects (\CONDITIONAL):] Effects can be conditional.
\item[Literals as formulae (\LITERALS):] The formulae in preconditions and
  effect conditions can be literals.
\begin{sloppypar}
\item[Boolean formulae (\BOOL):] The formulae in preconditions and
  effect conditions can be arbitrary boolean formulae.
\end{sloppypar}
\end{description}
These extensions can also be combined. We will use combinations of letters
to refer to such multiple extensions. For instance, \PLluc{} refers to the
formalism \STRIPS\label{D:STRIPSx}{} extended by literals in the precondition lists,
\PLa{} refers to the
formalism allowing for incomplete state specifications and conditional
effects,
 and \PL{}, finally, refers to the general planning formalism
introduced in Section~\ref{S:P:formalism}.

\begin{example}
\label{Ex:4}
When we consider the planning instance $\planinstance$ from
Example~\ref{Ex:3}, it becomes quickly obvious that this instance has been
expressed using \PLl{}. The initial state specification is {\em incomplete},
the operator $\sym{latex}$ contains {\em conditional
  effects} and negative {\em literals} in some effect
conditions. However, we do not need general {\em Boolean formulae} to express the
instance.
\end{example}

Figure~\ref{F:partial:order}
\begin{figure}[htb] 
\begin{center}
\setlength{\unitlength}{0.00083333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(3437,3870)(0,-10)
\path(2322,171)(1572,921)
\blacken\path(1678.066,857.360)(1572.000,921.000)(1635.640,814.934)(1678.066,857.360)
\path(2322,171)(3072,921)
\blacken\path(3008.360,814.934)(3072.000,921.000)(2965.934,857.360)(3008.360,814.934)
\path(2322,171)(2322,921)
\blacken\path(2352.000,801.000)(2322.000,921.000)(2292.000,801.000)(2352.000,801.000)
\path(1422,1146)(222,2046)
\blacken\path(336.000,1998.000)(222.000,2046.000)(300.000,1950.000)(336.000,1998.000)
\path(2322,1146)(372,2121)
\blacken\path(492.748,2094.167)(372.000,2121.000)(465.915,2040.502)(492.748,2094.167)
\path(1422,1146)(1422,2046)
\blacken\path(1452.000,1926.000)(1422.000,2046.000)(1392.000,1926.000)(1452.000,1926.000)
\path(3222,1146)(1422,2046)
\blacken\path(1542.748,2019.167)(1422.000,2046.000)(1515.915,1965.502)(1542.748,2019.167)
\path(3222,1146)(2322,2046)
\blacken\path(2428.066,1982.360)(2322.000,2046.000)(2385.640,1939.934)(2428.066,1982.360)
\path(2322,1146)(2322,2046)
\blacken\path(2352.000,1926.000)(2322.000,2046.000)(2292.000,1926.000)(2352.000,1926.000)
\path(3222,1146)(3222,2046)
\blacken\path(3252.000,1926.000)(3222.000,2046.000)(3192.000,1926.000)(3252.000,1926.000)
\path(222,2346)(1122,2946)
\blacken\path(1038.795,2854.474)(1122.000,2946.000)(1005.513,2904.397)(1038.795,2854.474)
\path(1422,2346)(1422,2946)
\blacken\path(1452.000,2826.000)(1422.000,2946.000)(1392.000,2826.000)(1452.000,2826.000)
\path(1422,2346)(2322,2946)
\blacken\path(2238.795,2854.474)(2322.000,2946.000)(2205.513,2904.397)(2238.795,2854.474)
\path(3222,2346)(2322,2946)
\blacken\path(2438.487,2904.397)(2322.000,2946.000)(2405.205,2854.474)(2438.487,2904.397)
\path(3222,2346)(3222,2946)
\blacken\path(3252.000,2826.000)(3222.000,2946.000)(3192.000,2826.000)(3252.000,2826.000)
\path(2322,2346)(1422,2946)
\blacken\path(1538.487,2904.397)(1422.000,2946.000)(1505.205,2854.474)(1538.487,2904.397)
\path(2322,2346)(3222,2946)
\blacken\path(3138.795,2854.474)(3222.000,2946.000)(3105.513,2904.397)(3138.795,2854.474)
\path(1422,3246)(2322,3696)
\blacken\path(2228.085,3615.502)(2322.000,3696.000)(2201.252,3669.167)(2228.085,3615.502)
\path(2322,3246)(2322,3696)
\blacken\path(2352.000,3576.000)(2322.000,3696.000)(2292.000,3576.000)(2352.000,3576.000)
\path(3222,3246)(2322,3696)
\blacken\path(2442.748,3669.167)(2322.000,3696.000)(2415.915,3615.502)(2442.748,3669.167)
\put(2322,3771){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PL}}}}}
\put(2322,3021){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLc}}}}}
\put(1422,2121){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLlc}}}}}
\put(2322,2121){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLlu}}}}}
\put(3222,2121){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLuc}}}}}
\put(147,2121){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLa}}}}}
\put(1422,996){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLac}}}}}
\put(2322,996){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLau}}}}}
\put(3222,996){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLluc}}}}}
\put(1422,3021){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLl}}}}}
\put(3222,3021){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLu}}}}}
\put(2322,21){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLauc}}}}}
\end{picture}
}

\caption{Planning formalisms partially ordered by syntactic restrictions}
\label{F:partial:order}
\end{center}
\end{figure}
 displays the partial order on propositional planning formalisms defined in
this way. 
In the sequel we say that $\planfx$ {\emdef is a specialization} of
$\planfy$,
written $\planfx \spec \planfy$,\label{D:spec} iff $\planfx$ is identical to $\planfy$ or below $\planfy$ in the diagram
depicting the partial order.

\begin{sloppypar}
Comparing this set of planning formalisms with the one B\"ackstr\"om
\shortcite{backstrom:ai-95} analyzed,\footnote{We do not consider planning
  formalisms identical to the \sasplus\ formalism \cite{backstrom:nebel:ci-95},
  since we do not allow for multi-valued state variables.} one notices that
despite small differences in the presentation of the planning formalisms:
\begin{itemize}
\item \PLauc{} is the same as {\em common propositional strips} (\cps),
\item \PLluc{} is the same as {\em propositional strips with negative
    goals} (\psn), and
\item \PLul{} is the same as {\em ground Tweak} (\gtweak).
\end{itemize}
\end{sloppypar}

\subsection{The Computational Complexity of Planning in the \STRIPS-Family}

While one would expect that planning in \PLauc{} is much easier than planning
in \PL, it turns out that this is not the case, provided one takes a
computational complexity perspective.  

In analyzing the computational complexity
of planning in different formalisms, we consider, as usual, the problem of
deciding whether there {\em exists a plan} for a given instance---the {\emdef
  plan existence problem} (\planex).\label{D:planex} We will use a prefix referring to the
planning formalism if we consider the existence problem in a particular
planning formalism.

\begin{theorem}
  $\planfx$-\planex{} is \PSPACE-complete for all  $\planfx$ with  \PLauc{}
  $\spec \planfx \spec$  \PL{}.
\end{theorem}
\begin{proof}
\PSPACE-hardness of \PLauc-\planex{} follows from a result by Bylander
\citeyear
[Corollary
3.2]{bylander:ai-94}. 

Membership of \PL-\planex{} in \PSPACE{} follows because we could, step by
step, guess a sequence of operators, verifying at each step that the
operator application leads to a legal follow up state specification and that
the last operator application leads to a state specification that entails the
goal specification. For each step, this verification can be carried out in
polynomial space. The reason for this is that all the conditions in the
definition of $\res$ are verified by polynomially many calls to an \NP-oracle.
Therefore, \PL{} can be decided on a non-deterministic machine in polynomial
space, hence it is a member of \PSPACE.

From that it follows that the plan existence problem for all formalisms that
are in expressiveness between \PLauc{} and \PL---including both
formalisms---is \PSPACE-complete.
\end{proof}

\section{\sloppy Expressiveness and Compilability between Planning Formalisms}
\label{S:compilability}

Although there is no difference in the computational complexity between the
formalisms in the \PL-family, there might nevertheless be a difference in how
concisely planning domains and plans can be expressed. In order to investigate
this question, we introduce the notion of {\em compiling planning formalisms.}


\subsection{Compiling Planning Formalisms}

As mentioned in the Introduction, we will consider a planning formalism
$\planfx$ {\em as expressive as} another formalism $\planfy$ if {planning
  domains} and {plans} formulated in formalism $\planfy$ are {\em concisely
  expressible} in $\planfx$.  We formalize this intuition by making use of
what we call {\em compilation schemes}, which are {\em solution preserving
  mappings} with {\em polynomially sized results} from $\planfy$ domain
structures to $\planfx$ domain structures. While we restrict the size of the
result of a compilation scheme, we do not require any bounds on the
computational resources for the compilation. In fact, for measuring the {\em
  expressibility}, it is irrelevant whether the mapping is polynomial-time
computable, exponential-time computable, or even non-recursive. At least, this
seems to be the idea when the notion of {\em expressive power} 
 is discussed in similar contexts 
\cite{baader:ecai-90,erol:et:al:amai-96,gogic:et:al:ijcai-95,cadoli:et:al:kr-96}. 
If we want to
use such compilation schemes in practice, they should be reasonably efficient,
of course. However, if we want to prove that one formalism is {\em strictly
  more expressive} than another one, we have to prove that there is no
compilation scheme regardless of how many computational resources such a
compilation scheme might use.

So far, compilation schemes restrict only the size of domain structures.
However, when measuring expressive power, the size of the generated plans
should also play a role. In B\"ackstr\"om's ESP-reductions
\shortcite{backstrom:ai-95}, the plan size must be identical. Similarly, the
translation from \PLlc{} to \PLluc{} proposed by Gazen and Knoblock
\shortcite{gazen:knoblock:ecp-97} seems to have as an implicit prerequisite
that the plan length in the target formalism should be almost the same. When
comparing the expressiveness of different planning formalisms, we might,
however, be prepared to accept some growth of the plans in the target
formalism. For instance, we may accept an additional constant number of
operators, or we may even be satisfied if the plan in the target formalism is
linearly or polynomially larger. This leads to the schematic picture of
compilation schemes as displayed in Figure~\ref{F:knowledge:compilation}.

\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{0.00058333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(6638,2739)(0,-10)
\path(326,1812)(1226,1812)(1226,912)
        (326,912)(326,1812)
\path(776,2112)(776,1812)
\blacken\path(746.000,1932.000)(776.000,1812.000)(806.000,1932.000)(746.000,1932.000)
\path(776,912)(791,612)
\blacken\path(755.045,730.352)(791.000,612.000)(814.970,733.348)(755.045,730.352)
\path(3251,2712)(4151,2712)(4151,1812)
        (3251,1812)(3251,2712)
\path(2351,1512)(3251,1962)
\blacken\path(3157.085,1881.502)(3251.000,1962.000)(3130.252,1935.167)(3157.085,1881.502)
\path(3251,912)(4151,912)(4151,12)
        (3251,12)(3251,912)
\path(2366,1167)(3266,717)
\blacken\path(3145.252,743.833)(3266.000,717.000)(3172.085,797.498)(3145.252,743.833)
\path(1901,1512)(3251,2187)
\blacken\path(3157.085,2106.502)(3251.000,2187.000)(3130.252,2160.167)(3157.085,2106.502)
\path(1901,1212)(3251,537)
\blacken\path(3130.252,563.833)(3251.000,537.000)(3157.085,617.498)(3130.252,563.833)
\path(1001,2262)(3251,2262)
\blacken\path(3131.000,2232.000)(3251.000,2262.000)(3131.000,2292.000)(3131.000,2232.000)
\path(1001,462)(3251,462)
\blacken\path(3131.000,432.000)(3251.000,462.000)(3131.000,492.000)(3131.000,432.000)
\path(4151,2262)(4826,2262)
\blacken\path(4706.000,2232.000)(4826.000,2262.000)(4706.000,2292.000)(4706.000,2232.000)
\path(4151,462)(4826,462)
\blacken\path(4706.000,432.000)(4826.000,462.000)(4706.000,492.000)(4706.000,432.000)
\dashline{60.000}(4826,2037)(4826,237)
\dashline{60.000}(6176,2037)(6626,237)
\path(4826,312)(4826,162)
\path(6626,312)(6626,162)
\path(6176,2112)(6176,1962)
\path(4826,2112)(4826,1962)
\blacken\path(4826,2037)(6176,2037)(6176,1962)
        (4826,1962)(4826,2037)
\path(4826,2037)(6176,2037)(6176,1962)
        (4826,1962)(4826,2037)
\blacken\path(4826,237)(6626,237)(6626,162)
        (4826,162)(4826,237)
\path(4826,237)(6626,237)(6626,162)
        (4826,162)(4826,237)
\put(2351,1287){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}\goal}}}}}
\put(1901,1287){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}\initial}}}}}
\put(776,1362){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}compi-}}}}}
\put(776,1137){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}lation}}}}}
\put(3701,2262){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\planfy$}}}}}
\put(3701,2037){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}Planning}}}}}
\put(3701,462){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\planfx$}}}}}
\put(3701,237){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}Planning}}}}}
\put(776,2187){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\domainstructure$}}}}}
\put(776,387){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\domainstructure'$}}}}}
\put(5201,2187){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\plan$}}}}}
\put(5201,387){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\plan'$}}}}}
\end{picture}
}

\caption{The compilation framework}
\label{F:knowledge:compilation}
\end{center}
\end{figure}

Although Figure~\ref{F:knowledge:compilation} gives a good picture of the {\em
  compilation framework}, it is not completely accurate. First of all, a
compilation scheme may introduce some auxiliary propositional atoms that are
used to control the execution of newly introduced operators. These atoms
should most likely have an initial value and may appear in the goal
specification of planning instances in the target formalism. We will assume
that the compilation scheme takes care of this and adds some literals to the
initial state and goal specifications.
  
Additionally, some translations of the initial state and goal specifications
may be necessary. If we want to compile a formalism that permits for literals
in preconditions and goals to one that requires atoms, some trivial
translations are necessary. Similarly, if we want to compile a formalism that
permits us to use partial state specification to a formalism that requires
complete state specifications, a translation of the initial state specification
is necessary. However, such {\em state translation functions} should be very limited. They should depend only on the set of symbols in the source
formalism, should be ``context-independent,'' i.e., the translation of a
literal in a state specification should not depend on the whole specification,
and they should be efficiently computable.

While the compilation framework is a theoretical tool to measure
expressiveness, it has, of course, practical relevance.  Let us assume that we
have a reasonably fast planning system for a planning formalism $\planfx$ and
we want to add a new feature to $\planfx$ resulting in formalism $\planfy$. If
we can come up with an {\em efficient} compilation scheme from $\planfy$ to
$\planfx$, this means we can easily integrate the new feature---either by
using the compilation scheme or by modifying the planning algorithm minimally.
If no compilation scheme exists, we probably would have problems integrating
this feature.  Finally, if only computationally expensive compilation schemes
exist, we have an interesting situation. In this case, the off-line
compilation costs may be high. However, since the compiled domain structure
can be used for different initial and goal state specifications, the high
off-line costs may be compensated by the efficiency gain resulting from using
the $\planfx$ planning algorithm.\footnote{This means that compilation schemes
  between planning formalisms are similar to knowledge compilations
  \cite{cadoli:donini:aicom-97}, where the fixed part of a computational
  problem is the domain structure and the variable part consists of the
  initial state and goal specifications. The main difference to the knowledge
  compilation framework is that we also take the (size of the) result into
  account. In other words we compile function problems instead of decision
  problems.}  As it turns, however, this situation does not arise in analyzing
compilability between the \PL{} formalisms. Either we can identify a
polynomial-time compilation scheme or we are able to prove that no compilation
scheme exists.


\subsection{Compilation Schemes}

Assume a tuple of functions $\compfun = \langle \compdsfun, \compifun,
\compgfun, \transifun, \transgfun \rangle$\label{D:compfun} that induce a function $\comp$ from
$\planfx$-instances $\planinstance=\planinstancetuple$ to $\planfy$-instances
$\comp(\planinstance)$ as follows:
\[\comp(\planinstance) =  \bigr\langle 
\compdsfun(\domainstructure),
\compifun(\domainstructure) \cup  \transifun(\atomalph,\initial), 
\compgfun(\domainstructure) \cup \transgfun(\atomalph,\goal) \bigr\rangle.\label{D:comp}\label{D:compxfun}\label{D:transxfun}\] 
If the following three conditions are satisfied, we call $\compfun$ a {\emdef
  compilation scheme from $\planfx$ to $\planfy$}:
\begin{enumerate}
\item
\label{I:compilation:reduction}
there exists a plan for
$\planinstance$ iff there exists a plan for $\comp(\planinstance)$;
\item 
\label{I:translation}
the {\emdef state-translation functions} $\transifun$ and $\transgfun$ are
{\emdef modular}, i.e., for $\atomalph = \atomalph_1 \cup \atomalph_2$,
$\statespec \subseteq \litalph$, and $\statespec \not\models \falsity$, the
functions $\transxfun$ (for $x=i,g$) satisfy
\[ \transxfun(\atomalph,\statespec) = \transxfun(\atomalph_1,\statespec \cap
\literals{\atomalph_1}) \cup \transxfun(\atomalph_2,\statespec \cap \literals{\atomalph_2}),\] and
they are polynomial-time computable;
\item 
\label{I:compilation:size}
and the size of the results of $\compdsfun, \compifun$, and $\compgfun$ is
polynomial in the size of the arguments.
\end{enumerate}

Condition (\ref{I:compilation:reduction}) states that the function $\comp$
induced by the compilation scheme $\compfun$ is solution-preserving.
Condition (\ref{I:translation}) states requirements on the {\em on-line
  state-translation functions}. The result of these functions should be
computable {\em element-wise}, provided the state specification is consistent.
Considering the fact that these functions depend only on the original set of
symbols and the state specification, this requirement does not seem to be very
restrictive. Since the state-translation functions are on-line functions, we
also require that the result should be efficiently
computable.\footnote{Although it is hard to imagine a modular
  state-translation function that is not polynomial time computable, some
  pathological function could, e.g., output translations that have exponential
  size in the {\em encoding} of the symbols.} Finally,  condition
(\ref{I:compilation:size}) formalizes the idea that $\compfun$ is a
compilation.  For a {\em compilation} it is much more important that the
result can be {\em concisely represented}, i.e., in polynomial space, than
that the compilation process is fast.
Nevertheless, we are also interested in {\em efficient compilation schemes}.
We say that $\compfun$ is a {\emdef polynomial-time compilation scheme} if
$\compdsfun, \compifun$, and $\compgfun$ are polynomial-time
computable functions.

In addition to the resource requirements on the compilation process, we will
distinguish between different compilation schemes according to the effects on
the size of the plans solving the instance in the target formalism.  If a
compilation scheme $\compfun$ has the property that for every plan $\plan$
solving an instance $\planinstance$ there exists a plan $\plan'$ solving
$\comp(\planinstance)$ such that $\size{\plan'} \leq \size{\plan} + k$ for
some positive integer constant $k$, $\compfun$ is a {\emdef compilation scheme
  preserving plan size exactly} (up to additive constants). If $\size{\plan'}
\leq c \times \size{\plan} + k$ for positive integer constants $c$ and $k$,
then $\compfun$ is a {\emdef compilation scheme preserving plan size
  linearly}, and if $\size{\plan'} \leq p(\size{\plan},\size{\planinstance})$
for some polynomial $p$, then $\compfun$ is a {\emdef compilation scheme
  preserving plan size polynomially}.  More generally, we say that a planning
formalism $\planfx$ is {\emdef compilable} to formalism $\planfy$ (in
polynomial 
time, preserving plan size exactly, linearly, or polynomially), if there
exists a compilation scheme with the appropriate properties. We write $\planfx
\compilable^x \planfy$ in case $\planfx$ is compilable to $\planfy$ or
$\planfx \compilable^x_p \planfy$ if the compilation can be done in polynomial
time.\label{D:compilable} The super-script $x$ can be $1$, $c$, or $p$ depending on whether the
scheme preserves plan size exactly, linearly plan, or polynomially,
respectively.

As is easy to see, all the notions of compilability introduced above
are reflexive and transitive.

\begin{proposition}
\label{P:transitivity:reflexivity}
The relations $\compilable^x$ and $\compilable^x_p$ 
are transitive and reflexive.
\end{proposition}

Furthermore, it is obvious that when moving upwards in the diagram displayed in
Figure~\ref{F:partial:order}, there is always a polynomial-time compilation
scheme preserving plan size exactly. If $\pi_i$ denotes the projection to the
$i$-th argument and $\emptyset$ the function that returns always the empty
set, the generic compilation scheme for moving upwards in the partial order is
$\compfun = \langle \pi_1, \emptyset, \emptyset, \pi_2, \pi_2
\rangle$.

\begin{proposition}
\label{P:upward:compilability}
If $\planfx \spec \planfy$, then 
$\planfx \compilable_p^1 \planfy$.
\end{proposition}



\section{Compilability Preserving Plan Size Exactly}
\label{S:linear:compilability}

Proposition~\ref{P:upward:compilability} leads to the question of whether
there exist other compilation schemes than those implied by the
specialization relation.  Because of Proposition~\ref{P:upward:compilability}
and Proposition~\ref{P:transitivity:reflexivity}, we do not have to find
compilation schemes for every pair of formalisms. It suffices to prove that
$\planfx$ is compilable to $\planfy$, in order to arrive at the conclusion
that all formalisms that are below $\planfx$  are
compilable to $\planfy$ and formalisms above $\planfy$.

A preview of the results of this section is given in
Figure~\ref{F:partial:order:pres}. We will establish two equivalence classes
such that all members of each class are compilable to each other preserving
plan size exactly. These two equivalence classes will be called \PLlu- and \PLl-class,
in symbols \classPLlu{} and \classPLl,\label{D:classPLl} naming them after their respective
largest elements.

\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{0.00083333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(3567,4097)(0,-10)
\texture{0 0 0 888888 88000000 0 0 80808 
        8000000 0 0 888888 88000000 0 0 80808 
        8000000 0 0 888888 88000000 0 0 80808 
        8000000 0 0 888888 88000000 0 0 80808 }
\put(983,2198){\shade\ellipse{1950}{3600}}
\put(983,2198){\ellipse{1950}{3600}}
\put(2708,1321){\shade\ellipse{1544}{2626}}
\put(2708,1321){\ellipse{1544}{2626}}
\path(2483,398)(1733,1148)
\blacken\path(1839.066,1084.360)(1733.000,1148.000)(1796.640,1041.934)(1839.066,1084.360)
\path(2483,398)(3233,1148)
\blacken\path(3169.360,1041.934)(3233.000,1148.000)(3126.934,1084.360)(3169.360,1041.934)
\path(2483,398)(2483,1148)
\blacken\path(2513.000,1028.000)(2483.000,1148.000)(2453.000,1028.000)(2513.000,1028.000)
\path(1583,1373)(383,2273)
\blacken\path(497.000,2225.000)(383.000,2273.000)(461.000,2177.000)(497.000,2225.000)
\path(2483,1373)(533,2348)
\blacken\path(653.748,2321.167)(533.000,2348.000)(626.915,2267.502)(653.748,2321.167)
\path(1583,1373)(1583,2273)
\blacken\path(1613.000,2153.000)(1583.000,2273.000)(1553.000,2153.000)(1613.000,2153.000)
\path(3383,1373)(1583,2273)
\blacken\path(1703.748,2246.167)(1583.000,2273.000)(1676.915,2192.502)(1703.748,2246.167)
\path(3383,1373)(2483,2273)
\blacken\path(2589.066,2209.360)(2483.000,2273.000)(2546.640,2166.934)(2589.066,2209.360)
\path(2483,1373)(2483,2273)
\blacken\path(2513.000,2153.000)(2483.000,2273.000)(2453.000,2153.000)(2513.000,2153.000)
\path(3383,1373)(3383,2273)
\blacken\path(3413.000,2153.000)(3383.000,2273.000)(3353.000,2153.000)(3413.000,2153.000)
\path(383,2573)(1283,3173)
\blacken\path(1199.795,3081.474)(1283.000,3173.000)(1166.513,3131.397)(1199.795,3081.474)
\path(1583,2573)(1583,3173)
\blacken\path(1613.000,3053.000)(1583.000,3173.000)(1553.000,3053.000)(1613.000,3053.000)
\path(1583,2573)(2483,3173)
\blacken\path(2399.795,3081.474)(2483.000,3173.000)(2366.513,3131.397)(2399.795,3081.474)
\path(3383,2573)(2483,3173)
\blacken\path(2599.487,3131.397)(2483.000,3173.000)(2566.205,3081.474)(2599.487,3131.397)
\path(3383,2573)(3383,3173)
\blacken\path(3413.000,3053.000)(3383.000,3173.000)(3353.000,3053.000)(3413.000,3053.000)
\path(2483,2573)(3383,3173)
\blacken\path(3299.795,3081.474)(3383.000,3173.000)(3266.513,3131.397)(3299.795,3081.474)
\path(1583,3473)(2483,3923)
\blacken\path(2389.085,3842.502)(2483.000,3923.000)(2362.252,3896.167)(2389.085,3842.502)
\path(2483,3473)(2483,3923)
\blacken\path(2513.000,3803.000)(2483.000,3923.000)(2453.000,3803.000)(2513.000,3803.000)
\path(3383,3473)(2483,3923)
\blacken\path(2603.748,3896.167)(2483.000,3923.000)(2576.915,3842.502)(2603.748,3896.167)
\path(2483,2573)(1583,3173)
\blacken\path(1699.487,3131.397)(1583.000,3173.000)(1666.205,3081.474)(1699.487,3131.397)
\put(2483,3998){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PL}}}}}
\put(2483,3248){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLc}}}}}
\put(1583,2348){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLlc}}}}}
\put(3383,2348){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLuc}}}}}
\put(308,2348){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLa}}}}}
\put(1583,1223){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLac}}}}}
\put(2483,1223){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLau}}}}}
\put(1583,3248){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLl}}}}}
\put(3383,3248){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLu}}}}}
\put(2483,248){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLauc}}}}}
\put(2528,2348){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLlu}}}}}
\put(3256,1238){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLluc}}}}}
\end{picture}
}

\caption{Equivalence classes of planning formalisms created by 
polynomial-time compilation schemes preserving plan size exactly}
\label{F:partial:order:pres}
\end{center}
\end{figure}

\subsection{Planning Formalisms without Conditional Effects and 
  Boolean Formulae}

First, we will show that the formalisms analyzed by B\"ackstr\"om
\shortcite{backstrom:ai-95}, namely, \PLul, \PLluc, and \PLauc{} are
polynomial-time compilable into each other preserving plan size exactly.
In fact, a fourth class can be added to this set, namely, \PLau, which
lies between \PLul{} and \PLauc.

In other words, using the notion of {\em compilability}, we get the same
equivalence class as with B\"ackstr\"om's ESP-reductions. Having a closer look
at the proofs in B\"ackstr\"om's \shortcite{backstrom:ai-95} paper reveals
that this is not surprising at all because the ESP-reductions he used could be
reformulated as compilation schemes. Since he used a quite different notation,
we will nevertheless prove this claim from first principles.

The key idea in compiling planning formalisms with literals to
formalisms that allow for atoms only is to consider $\atomvar$ and $\neg \atomvar$
as different atoms in the new formalism. For this purpose, we introduce
$\copysym{\atomalph} =
\{\copysym{\atomvar} \:|\: \atomvar \in \atomalph\}$, i.e., a disjoint copy of
$\atomalph$. Further, if $\litset \subseteq \litalph$, then $\copyneg \litset$
is a set where each negative literal $\neg \atomvar$ in $\litset$ is replaced
by $\copysym{\atomvar}$, i.e.,
\[\copyneg \litset = \left\{\begin{array}{ll}
\{ \atomvar \in \atomalph \: | \: \atomvar \in
\litset \} \cup \{ \copysym{\atomvar} \in \copysym{\atomalph} \: | \: \neg
\atomvar \in \litset\} & \mbox{if\ } \litset \not\models \falsity, \\
\falsity & \mbox{otherwise.}
\end{array}\right.\]
Using $\atomalph \cup \copysym{\atomalph}$ as the new set of atoms,
one can translate state specifications and preconditions easily. In the postconditions we
have to make sure that the intended semantics is taken care of, i.e., whenever
$\atomvar$ is added, $\copysym{\atomvar}$ must be deleted and {\em vice versa}.

Finally, we have to deal with the problem of partial state specifications.
However, this not a problem when all effects are unconditional and the
preconditions contain only atoms. In this case, we can safely assume that all
atoms with unknown truth-value are false without changing the outcome of the
application of an operator. Let $\cwa_{\atomalph}(\litset)$\label{D:cwa} denote the {\emdef
  completion} of $\litset$ with respect to $\atomalph$, i.e.,
\[ \cwa_{\atomalph}(\litset) = \{ \neg \atomvar \: | \: \atomvar \in
\atomalph, \atomvar \not\in \litset \} \cup \litset. \] Using this function,
we can transform a partial state specification into a complete specification
without changing the outcome, i.e., we get the same plans.

\begin{theorem}
\label{T:unconditional:no:formulae}
\PLul, \PLau, \PLluc, and \PLauc{} are polynomial-time compilable to each
other preserving plan size exactly.
\end{theorem}

\begin{proof}
  Since \PLauc{} $\spec$ \PLau $\spec$ \PLlu{} and \PLauc{} $\spec$ \PLluc{}
  $\spec$ \PLlu, it follows from Propositions~\ref{P:transitivity:reflexivity}
  and~\ref{P:upward:compilability} that we only have to show that \PLul{}
  $\compilable_p^1$ \PLauc{} in order to prove the claim.
  
  Let $\planinstance = \planinstancetuple$ be a
  \PLul-instance with $\domainstructure=\domainstructuretuple$. We translate
  each operator $\op \in \opset$ into the operator
  \[ \copysym{\op} = \langle \copyneg
  \pre(\op), \copyneg \post(\op) \cup \neg \copyneg \neg \post(\op) \rangle. \]
  The set of all such operators is denoted by $\copysym{\opset}$. Now we can
  define the compilation scheme $\compfun = \langle \compdsfun, \compifun,
  \compgfun, \transifun, \transgfun\rangle$ as follows:
\begin{eqnarray*}
\compdsfun(\domainstructure) & = & \langle \atomalph \cup
\copysym{\atomalph}, \: \copysym{\opset}\rangle, \\
\compifun(\domainstructure) & = & \emptyset, \\
\compgfun(\domainstructure) & = & \emptyset, \\
\transifun(\atomalph,\initial) & = & \cwa_{\atomalph
  \cup \copysym{\atomalph}}(\copyneg \initial), \\
\transgfun(\atomalph,\goal) & = & \copyneg \goal.
\end{eqnarray*}
The scheme $\compfun$ obviously satisfies conditions
(\ref{I:translation}) and (\ref{I:compilation:size}), all the
functions can be computed in polynomial time, and
$\comp(\planinstance)$ is  a \PLauc-instance.


Let $\statespec \subseteq \litalph$. Then it is obvious that
\[ \transifun(\atomalph,\res(\statespec,\op)) =
\res(\transifun(\atomalph,\statespec),\copysym{\op}).\]
Let $\copysym{\plan} = \langle \copysym{\op_1}, \ldots,
\copysym{\op_n}\rangle$ denote a sequence of operators corresponding to a
sequence of operators $\plan = \langle\op_1, \ldots, \op_n \rangle$.
Using induction on plan length, it is easy to show that
\begin{center}
$\plan$ is a plan for $\planinstance$ iff $\copysym{\plan}$ is a plan
for $\comp(\planinstance)$, 
\end{center}
i.e., condition (\ref{I:compilation:reduction}) on compilation schemes
is also 
satisfied.
This means, $\compfun$ is in fact a compilation scheme. Further, since the
plan size does not change, the compilation scheme preserves plan size
exactly.
Finally,
because all functions in $\compfun$ can be computed in time polynomial in
their arguments, $\compfun$ is a polynomial-time compilation scheme.
\end{proof}

One view on this result is that it does not matter whether,  from an
expressivity point of view, we allow for atoms only or for
literals and it does not matter whether we have complete or partial
state specification---provided propositional formulae and conditional
effects are not allowed.

\subsection{\sloppy Planning Formalisms with Conditional Effects but without
  Boolean Formulae}
  

Interestingly, the view spelled out above generalizes to the case
where conditional effects are allowed. Also in this case it does not
matter whether only atoms or also literals are allowed and whether we
have partial or complete state specifications. In proving that,
however, there are two additional complications. Firstly, one must
compile conditional effects over partial state specifications to
conditional effects over complete state specifications. This is a
problem because the condition $\Eff(\statespec,\post(\op)) =
\Pot(\statespec,\post(\op))$ in the definition of the function $\res$
must be tested. Secondly, when compiling a formalism with literals
into a formalism that allows for atoms only, the condition
$\Eff(\statespec,\post(\op)) \not\models \falsity$ in the definition
of $\res$ must be taken care of. For this reason, we will prove this
result in two steps.

As a first step, we show that \PLl{} can be compiled to \PLlc.  The problem in
specifying such a compilation scheme is that the execution of an operator
$\op$ on a partial state specification leads to the illegal state if
$\Eff(\statespec,\post(\op)) \neq \Pot(\statespec,\post(\op))$. 

When considering our running example (Ex.~\ref{Ex:1}), things are quite
obvious. When a state specification does not contain the literal or the
negation of the literal that is mentioned in the effect condition, then the
illegal state specification results. For example, if a state specification
does neither contain $\sym{bbl}$ nor $\neg \sym{bbl}$, then the result of
executing $\sym{latex}$ is $\falsity$. In the general case, however, things
are less straightforward because effect literals can be produced by  more
than one conditional rule and an effect condition can consist of more than one
literal. 

Assuming without loss of generality
(using a polynomial transformation) that the effects are all singleton sets,
we have to check the following condition. Either one of the conditional
effects with the same effect literal is activated---i.e., the effect condition
is entailed by the partial state---or all of the conditional effects with the
same effect literal are {\em blocked}, i.e., each effect condition contains a literal that is inconsistent with the state specification. If this is true, the
original operator satisfies $\Eff(\statespec,\post(\op)) = \Pot(\statespec,\post(\op))$, otherwise
the resulting state specification is inconsistent. For example, consider the
following \PLl{} operator:
\begin{eqnarray*}
\op_i & =  &
 \langle  \truth, \{ \{ \atomvar, \neg \atomvarq\} \effimpl \{\neg
\atomvar\}, \{ \atomvaru, \atomvarv \} \effimpl \{ \neg \atomvar \} \}
\rangle.
\end{eqnarray*}
The application of this operator satisfies $\Eff(\statespec,\post(\op)) =
\Pot(\statespec,\post(\op))$  iff either
\begin{enumerate}
\item $\atomvar$ and $\neg \atomvarq$ are true in the state specification, or
\item $\atomvaru$ and $\atomvarv$ are true in the state specification, or
\item one of $\atomvar$ and $\neg \atomvarq$ is false {\em and} one of $\atomvaru$ and
  $\atomvarv$ is false.
\end{enumerate}
In all other cases, we get $\Eff(\statespec,\post(\op)) \neq \Pot(\statespec,\post(\op))$ and the
result is the illegal state.
In order to test for this condition in a formalism with complete states we
introduce four new sets of atoms: 
\begin{eqnarray*}
\copyksym{\atomalph} & = & \{ \copyksym{\atomvar} \:|\: \atomvar \in
\atomalph\}, \\
\copyaddksym{\atomalph} & = &
\{\copyaddksym{\atomvar} \:|\: \atomvar \in \atomalph\}, \\
\copydelksym{\atomalph} & = &
\{ \copydelksym{\atomvar} \:|\: \atomvar \in \atomalph\}, \\
\unknownset & = & \{ \atomvarx_{i,j} \:|\: \mbox{for the $j$th conditional
  effect of $\op_i$}\}.
\end{eqnarray*}

The atom $\copyksym{\atomvar}$ is true if either $\atomvar$ or $\neg \atomvar$
is part of the original partial state specification. The atom
$\copyaddksym{\atomvar}$ is set true by an operator if one of the conditional
effects adds $\atomvar$ or if $\atomvar$ does not appear as an effect in the
operator.  The atom $\copydelksym{\atomvar}$ is 
set true by an operator if one of the
conditional effects deletes $\atomvar$ or if $\neg \atomvar$ does not appear as an effect
in the operator.  Finally, atoms of the form $\atomvarx_{i,j}$ are added by
an action if the $j$th conditional effect in the $i$th operator is blocked by
some effect condition.  Using these new atoms, we could translate the above
operator to
\begin{eqnarray*}
  \copysym{\op_i} & = & \langle \truth, \:
    \{ \!\!\begin{array}[t]{l}
      \{\copyksym{\atomvar}, \copyksym{\atomvarq}, \atomvar, \neg \atomvarq\}
      \effimpl \{ \copyksym{\atomvar}, \copydelksym{\atomvar}, \neg\atomvar\}, \\
      \{\copyksym{\atomvaru}, \copyksym{\atomvarv}, \atomvaru, \atomvarv\}
      \effimpl \{ \copyksym{\atomvar}, \copydelksym{\atomvar}, \neg\atomvar\}, \\
      \{\copyksym{\atomvar}, \neg \atomvar\} \effimpl \{\atomvarx_{i,1}\}, \\
    \{\copyksym{\atomvarq}, \atomvarq\} \effimpl \{\atomvarx_{i,1}\}, \\
    \{\copyksym{\atomvaru}, \neg \atomvaru\} \effimpl \{\atomvarx_{i,2}\},
    \\
    \{\copyksym{\atomvarv}, \neg \atomvarv\} \effimpl \{\atomvarx_{i,2}\},
    \\
    \truth \effimpl \copyaddksym{\atomalph} \cup \copydelksym{\atomalph} -
    \{\copydelksym{\atomvar}\}, \\
    \truth \effimpl \{ \atomvarx_{m,j} \in \unknownset\:|\: m \neq i\}\}\rangle.
  \end{array}
\end{eqnarray*}
Let $\unknownlitfun(i,j)$ be a function that returns $\copyaddksym{\atomvar}$
or $\copydelksym{\atomvar}$, if $\atomvar$ or $\neg \atomvar$, respectively, is
the effect of the $j$th conditional effect in the $i$th operator.  Assuming
now that the atoms from $\copyksym{\atomalph}$ are set according to their
intended semantics and that the previous operator deleted all atoms from
$\copyaddksym{\atomalph} \cup \copydelksym{\atomalph} \cup \unknownset$, the
following {\em test} operator checks whether the original operator would have
led to an inconsistent result:
\begin{eqnarray*}
\testop & = & \biggl\langle \truth, \biggl\{ \{\neg \atomvarx_{i,j}, \neg
\unknownlitfun(i,j) \} \effimpl \falsity \: | \: \atomvarx_{i,j} \in
\unknownset\biggr\}\biggr\rangle.
\end{eqnarray*}
Whenever we have $\neg\atomvarx_{i,j}$, it means the $j$th conditional effect
in the $i$th operator (which must be the previously executed operator) was not
blocked. If in addition to that the effect of this conditional effect was not
activated, i.e., $\neg \unknownlitfun(i,j)$ is true, we would have
$\Eff(\statespec,\post(\op)) \neq \Pot(\statespec,\post(\op))$ in the original formalism. For this
reason, we force the illegal state. Conversely, if either $\atomvarx_{i,j}$ is
true for all $i$ and $j$ or if it is false for one $j$, but
$\unknownlitfun(i,j)$ is true, we would have $\Eff(\statespec,\post(\op)) =
\Pot(\statespec,\post(\op))$ in the original formalism and do not need to force the
illegal state.

We now could force, by using some extra literals, that after each operator
$\copysym{\op_i}$ the {\em test} operator is applied. This would result in a
compilation scheme that preserves plan size only {\em linearly}.  However, it
is possible to do better than that. The key idea is to merge the test operator
for the $i$th step into the operator of step $i+1$.

\begin{lemma}
\label{L:pa:to:pac}
\PLl{} is polynomial-time compilable to \PLlc{} preserving plan size exactly.
\end{lemma}

\begin{proof}
  Let $\planinstance = \planinstancetuple$ be a \PLl-instance with
  $\domainstructure=\domainstructuretuple$. Without loss of generality, we
  assume that the postconditions of operators $\op_i \in \opset$ have the
  following form:\label{D:litvar}
\[  \post(\op_i) = \{ \litset_{i,1} \effimpl
\litvar_{i,1}, \ldots, \litset_{i,m_i} \effimpl \litvar_{i,m_{i}} \},\] with
$\litset_{i,j} \subseteq \literals{\atomalph}$ and $\litvar_{i,j} \in
\litalph$.

First, we introduce a number of new sets of symbols that are pairwise disjoint
and disjoint from $\atomalph$:
\begin{eqnarray*}
\copyksym{\atomalph} & = & \{ \copyksym{\atomvar} \:|\: \atomvar \in
\atomalph\}, \\
\copyaddksym{\atomalph^0} & = &
\{\copyaddksym{\atomvar^0} \:|\: \atomvar \in \atomalph\}, \\
\copyaddksym{\atomalph^1} & = &
\{\copyaddksym{\atomvar^1} \:|\: \atomvar \in \atomalph\}, \\
\copydelksym{\atomalph^0} & = &
\{ \copydelksym{\atomvar^0} \:|\: \atomvar \in \atomalph\}, \\
\copydelksym{\atomalph^1} & = &
\{ \copydelksym{\atomvar^1} \:|\: \atomvar \in \atomalph\}, \\
\unknownset^0 & = & \{ \atomvarx_{i,j}^0 \:|\: \mbox{for the $j$th conditional
  effect of $\op_i$}\}, \\
\unknownset^1 & = & \{ \atomvarx_{i,j}^1 \:|\: \mbox{for the $j$th conditional
  effect of $\op_i$}\}.
\end{eqnarray*}
For a given set of literals $\litset \subseteq  \litalph$, $\copyksym{\litset}$ denotes
the set of primed literals, i.e., $\copyksym{\litset} = \{ \copyksym{\atomvar}
\: | \: \atomvar \in \litset\} \cup  \{ \neg \copyksym{\atomvar}
\: | \: (\neg \atomvar) \in \litset\} $ and the function $\msucc(\cdot)$
denotes the successor function modulo 2, i.e., $\msucc(k) = (k+1) \bmod 2$.
Further, the functions $\unknownlitfun^k$ for $k=0,1$ shall be functions from
$\unknownset^k$ to $\copyaddksym{\atomalph^k} \cup \copydelksym{\atomalph^k}$
such that 
\[ \unknownlitfun^k(i,j) = \left\{\!\!\begin{array}{ll}
\copyaddksym{\atomvarq^k} \in \copyaddksym{\atomalph^k} & \mbox{if } (\litset_{i,j}
\effimpl \atomvarq) \in \post(\op_i), \\
\copydelksym{\atomvarq^k} \in \copydelksym{\atomalph^k} & \mbox{if } (\litset_{i,j}
\effimpl \neg \atomvarq) \in \post(\op_i).
\end{array}
\right.\]
Now let ${\post^k(\op_i)}$ for $k=0,1$ be defined as follows
\[ {\post^k(\op_i)} = \!\!\! \begin{array}[t]{l}
\{ \litset \cup \alphabet(\copyksym{\litset}) \effimpl \{ \atomvar,
\copyksym{\atomvar}, \copyaddksym{\atomvar}^k\} \: | \: \atomvar \in \atomalph, (\litset
\effimpl  \atomvar ) \in \post(\op_i) \} \: \cup \\
\{ \litset  \cup \alphabet(\copyksym{\litset}) \effimpl \{ \neg
\atomvar,
\copyksym{\atomvar}, \copydelksym{\atomvar}^k\} \: | \: \atomvar \in \atomalph, (\litset
\effimpl  \neg \atomvar ) \in \post(\op_i) \},
\end{array}\]
let $\block^k(\op_i)$ for $k=0,1$ be defined as
\[ \block^k(\op_i) =  \!\!\! \begin{array}[t]{l}
\{ \{\atomvarq, \copyksym{\atomvarq} \} \effimpl
\atomvarx_{i,j}^k \: | \: (\litset_{i,j} \effimpl \litvar_{i,j}) \in
\post(\op_i), (\neg \atomvarq) \in \litset_{i,j} \} \: \cup \\
\{ \{\neg \atomvarq, \copyksym{\atomvarq} \} \effimpl
\atomvarx_{i,j}^k \: | \: (\litset_{i,j} \effimpl \litvar_{i,j}) \in
\post(\op_i), \atomvarq \in \litset_{i,j} \},
\end{array}\]
and let $\test^k$ be defined as
\[ test^k = \{  \{ \neg \atomvarx_{i,j}^{\msucc(k)}, \neg
\unknownlitfun^{\msucc(k)}(i,j)\} \effimpl \falsity \: | \: 
\atomvarx_{i,j}^{\msucc(k)} \in \unknownset^{\msucc(k)}\}.\]
Further, let $\cycle^1$, $\cycle^2$, and $\newgoal$ be fresh symbols not
appearing in $\atomalph \cup \copyksym{\atomalph} \cup
\copyaddksym{\atomalph^k} \cup \copydelksym{\atomalph^k}
\cup \unknownset^k$.
Now we can define the pair of compiled operators ${\op}_{i}^k$ ($k=0,1$) corresponding
to the original operator $\op_i \in \opset$:
\[ {\op}_{i}^{k} = \langle \pre(\op_i) \cup \{ \cycle^k \}, \!\!\!
\begin{array}[t]{l}
{\post^k(\op_i)} \cup \block^k(\op_i) \cup \test^k \:
\cup \\
\{  \truth  \effimpl \{ \neg \cycle^k, \neg \newgoal, \cycle^{s(k)} \} \}\: 
\cup \\
\{ \truth \effimpl \copyaddksym{\atomalph^{k}} \cup
  \copydelksym{\atomalph^{k}} - \{ \unknownlitfun^{k}(i,j) \} \} \: \cup \\
\{ \truth \effimpl \{ \atomvarx_{m,j}^k \in \unknownset^k \: | \: m \neq i\}
\} \: \cup \\
\{ \truth \effimpl \neg \copyaddksym{\atomalph^{\msucc(k)}} \cup \neg
  \copydelksym{\atomalph^{\msucc(k)}} \cup \neg \unknownset^{\msucc(k)} \}.
\end{array}\] 

This pair of compiled operators achieves the intended effects and keeps track
of fully known atoms using $\post^k$, checks which conditional effects are
blocked using $\block^k$, tests whether the execution of the previous operator
satisfied the condition $\Eff(\statespec,\post(\op)) = \Pot(\statespec,\post(\op))$ using $\test^k$,
and setup the bookkeeping atoms for the next step. Using the atoms $\cycle^k$,
it is enforced that executing and testing is merged by parallelizing the
test on step $i$ and execution of step $i+1$. In order to check the execution
of the last step, we need an extra checking step:
\[ \op_{\newgoal}^{k} = \langle \{ \cycle^k \}, \test^k \cup \{ \truth \effimpl
\{\newgoal,\neg \cycle^k \}\} \rangle.
\]

Now we can specify a compilation scheme $\compfun$ from \PLl{} to \PLlc{} 
as follows:
\begin{eqnarray*}
\compdsfun(\domainstructure) & = & \langle \!\!
\begin{array}[t]{l}
\atomalph \cup \copyksym{\atomalph} \cup \copyaddksym{\atomalph^0} \cup
\copyaddksym{\atomalph^1} \cup \copydelksym{\atomalph^0} \cup
\copydelksym{\atomalph^1} \cup
\unknownset^0 \cup \unknownset^1 \cup
\{\newgoal,
\cycle^0, \cycle^1\}, \\  \bigcup \: \{
\op_{i}^0 , \op_{i}^1 \: | \: \op_i \in \opset \} \cup \{
\op_{\newgoal}^{0}, \op_{\newgoal}^{1} \}\rangle, 
\end{array}
\\ 
\compifun(\domainstructure) & = & \{ \neg \newgoal, \cycle^0,
\neg \cycle^1 \} \cup \neg \copyaddksym{\atomalph^0} \cup \neg \copyaddksym{\atomalph^1} \cup \neg
\copydelksym{\atomalph^0} \cup \neg
\copydelksym{\atomalph^1}  \cup \neg \unknownset^0 \cup \neg \unknownset^1, \\
\compgfun(\domainstructure) & = & \{ \newgoal \}, \\
\transifun(\atomalph, \initial) & = &
\cwa_{\atomalph}(\initial)  \cup \cwa_{\copyksym{\atomalph}}(\{
  \copyksym{\atomvar} \: | \: \atomvar \in \atomalph, \{ \atomvar, \neg \atomvar\}
  \cap  \initial \neq \emptyset \}), \\
\transgfun(\atomalph, \goal) &  = &  \goal.
\end{eqnarray*}
The scheme $\compfun$ obviously satisfies conditions
(\ref{I:translation}), i.e., that the state-translation functions are modular,
and (\ref{I:compilation:size}), i.e., that the compilation functions have
polynomially sized results. Further, all the
functions can be  computed in polynomial time, and
$\comp(\planinstance)$ is a \PLlc-instance.

\begin{sloppypar}
Assume $\statespec \subseteq \litalph$. Then it is obvious that 
\[ \transifun(\atomalph,\Result(\statespec,\langle \op_i\rangle)) \cap 
(\litalph  \cup
\literals{\copyksym{\atomalph}}) =
\Result(\transifun(\atomalph,\statespec) \cup
\compifun(\domainstructure),\langle{\op_i^0}\rangle) \cap (\litalph \cup
\literals{\copyksym{\atomalph}}),\] 
provided $\Result(\statespec,\langle\op_i\rangle) \not\models \falsity$. In case $\Result(\statespec,\langle\op_i\rangle)
\models \falsity$, either
$\Result(\transifun(\atomalph,\statespec) \cup
\compifun(\domainstructure),\langle{\op^0_i}\rangle) \models \falsity$ or
$\Eff(\statespec,\post(\op_i)) \neq \Pot(\statespec,\post(\op_i))$.
In the latter case, the application of any operator to
$\Result(\transifun(\atomalph,\statespec),\langle{\op_i^0}\rangle)$ leads to an
inconsistent state because of the conditional effects in $\test^1$, which is
part of all postconditions of operators applicable in this
state. Additionally, the same is true for the relation between $\transifun(\atomalph,\Result(\statespec,\langle
\op_i,\op_j))$ and $\Result(\transifun(\atomalph,\statespec) \cup
\compifun(\domainstructure), \langle \op_i^0, \op_j^1 \rangle)$.
\end{sloppypar}

Let $\copyksym{\plan} = \langle \copyksym{\op_1}, \ldots,
\copyksym{\op_n}\rangle$ denote a sequence of operators corresponding to a
sequence of operators $\plan = \langle\op_1, \ldots, \op_n \rangle$. Using
induction on the plan length, it can be easily shown that
\begin{center}
  $\plan$ is a plan for $\planinstance$ iff $\copyksym{\plan}; \op^k_{\newgoal}$ is a plan
  for $\comp(\planinstance)$.
\end{center}
Further, since any plan solving the instance $\comp(\planinstance)$ must have
$\op_{\newgoal}^k$ as the last operator, it follows that
\begin{center}
  there exists a plan for $\planinstance$ iff there exists a plan for
  $\comp(\planinstance)$.
\end{center}
From that it follows immediately that $\compfun$ is a polynomial-time compilation scheme from \PLl{} to
\PLlc{} preserving plan size exactly, which proves the claim.
\end{proof}

Having proved that \PLl{} can be compiled to \PLlc{} preserving plan size
exactly, it seems worth noting that this result depends on the semantics
chosen for executing conditional operators on partial state specifications.
For example, if we use an alternative semantics that deletes all the literals
in $\neg (\Pot(\statespec,\post(\op)) - \Eff(\statespec,\post(\op))$
provided $\Pot(\statespec,\post(\op))$ is consistent,
then there exists probably
only a compilation scheme that preserves plan size linearly. If we use a
semantics where the resulting state specification is legal when the
application of all state-transformation functions leads to a theory that can
be represented as a set of literals, it seems unlikely that there exists a
scheme that preserves plan size polynomially. The reason for this pessimistic
conjecture is that under this semantics it appears to be \coNP-hard to
determine whether the state specification resulting from applying a
\PLl-operator is legal.

As a second step in  showing that partial state specifications
and literals can be compiled away, we show that we can compile \PLlc{} to
\PLac. The key idea in the proof is the same as in the proof of
Theorem~\ref{T:unconditional:no:formulae}. We replace each negative literal
$\neg \atomvar$ by a new atom $\copysym{\atomvar}$. In order to detect
inconsistencies introduced by conditional effects, we add to each
postcondition conditional effects of the form $\{\atomvar,\copysym{\atomvar}\}
\effimpl \falsity$. Further, to check that the last operator in a plan does not
introduce any inconsistencies, we force the application of a ``checking''
operator that contains the same conditional effects.

\begin{lemma}
\label{L:pl:to:pa}
\PLlc{} is polynomial-time compilable to \PLac{} preserving plan size exactly.
\end{lemma}

\begin{proof}
  Let $\planinstance = \planinstancetuple$ be a
  \PLlc-instance with $\domainstructure=\domainstructuretuple$. Since $\planinstance$ is a \PLlc-instance, the 
  postconditions of all operators $\op \in \opset$ have the following form:
\[\post(\op) = \{ \litset_{1} \effimpl
\litsetm_{1}, \ldots, \litset_{m} \effimpl \litsetm_{m} \},\] 
with $\litset_j, \litsetm_j \subseteq \litalph$. 

As in the proof of Theorem~\ref{T:unconditional:no:formulae},
$\copysym{\atomalph}$ shall be a disjoint copy of $\atomalph$, and $\copyneg
\litset$ is the set of atoms where each negative literal $\neg \atomvar$ is
replaced by the atom $\copysym{\atomvar}$.  Now let $\copysym{\post(\op)}$ be
the following set
\[ \copysym{\post(\op)} = \{ \copyneg \litset_{j} \effimpl (\copyneg \litsetm_j
\cup \neg \copyneg \neg \litsetm_j) \: | \: (\litset_j \effimpl \litsetm_j)
\in \post(\op) \}. \]
Further, let $\cons$ be the set of conditional effects 
\[ \cons = \{ \{\atomvar, \copysym{\atomvar} \} \effimpl \falsity \: |
\: \atomvar \in \atomalph \},\]
let $\newgoal$ be an atom not appearing in $\atomalph$,
let
$\copysym{\op}$ be 
\[ \copysym{\op} = \langle \copyneg \pre(\op), \copysym{\post(\op)} \cup \cons
  \cup \{ \truth \effimpl  \neg \newgoal  \}\rangle, \]
let $\copysym{\opset} = \{ \copysym{\op} \: | \: \op \in \opset \}$,
and let the operator $\opcons$ be 
\[ \opcons = \langle  \truth , \cons \cup \{   \truth  \effimpl 
\newgoal  \} \rangle.\]
Then we can
specify a compilation scheme $\compfun$ from \PLlc{} to \PLac{} as follows:
\begin{eqnarray*}
\compdsfun(\domainstructure) & = & \langle \atomalph \cup
\copysym{\atomalph} \cup \{\newgoal\}, \: \copysym{\opset} \cup \{
\opcons \}\rangle, \\ 
\compifun(\domainstructure) & = & \{ \neg \newgoal \}, \\
\compgfun(\domainstructure) & = & \{ \newgoal \}, \\
\transifun(\atomalph, \initial) & = & \copyneg \initial \cup
\neg \copyneg \neg \initial, \\
\transgfun(\atomalph, \goal) &  = & \copyneg \goal.
\end{eqnarray*}
The scheme $\compfun$ obviously satisfies conditions
(\ref{I:translation}) and (\ref{I:compilation:size}), all the
functions can be  computed in polynomial time, and
$\comp(\planinstance)$ is a \PLac-instance.

Assume $\statespec \subseteq \litalph$. Then it is obvious that 
\[ \transifun(\atomalph,\res(\statespec,\op)) =
\res(\transifun(\atomalph,\statespec),\copysym{\op}), \mbox{\ \ \ provided\ }
\res(\statespec,\op) \not\models \falsity.\] In case $\res(\statespec,\op)
\models \falsity$, either
$\res(\transifun(\atomalph,\statespec),\copysym{\op}) \models \falsity$ or
$\{\atomvar, \copysym{\atomvar}\} \subseteq
\res(\transifun(\atomalph,\statespec),\copysym{\op})$ for some $\atomvar \in
\atomalph$. In the latter case, the application of any operator to
$\res(\transifun(\atomalph,\statespec),\copysym{\op})$ leads to an
inconsistent state because of the conditional effects in $\cons$, which is
part of all postconditions.

Let $\copysym{\plan} = \langle \copysym{\op_1}, \ldots,
\copysym{\op_n}\rangle$ denote a sequence of operators corresponding to a
sequence of operators $\plan = \langle\op_1, \ldots, \op_n \rangle$. Using
induction on the plan length, it can be easily shown that
\begin{center}
  $\plan$ is a plan for $\planinstance$ iff $\copysym{\plan}; \op_{\newgoal}$ is a plan
  for $\comp(\planinstance)$.
\end{center}
Further, since any plan solving the instance $\comp(\planinstance)$ must have
$\op_g$ as the last operator, it follows that
\begin{center}
  there exists a plan for $\planinstance$ iff there exists a plan for
  $\comp(\planinstance)$.
\end{center}
It follows that $\compfun$ is polynomial-time compilation scheme from \PLlc{} to
\PLac{} preserving plan size exactly, which proves the claim.
\end{proof}

This result is, of course, not dependent on the semantics because both
formalisms deal only with complete state specifications, and hence we always
have $\Eff(\statespec,\post(\op)) = \Pot(\statespec,\post(\op))$. 

\begin{theorem}
\label{T:conditional:no:formulae}
  \PLl, \PLlc, \PLa, and \PLac{} are polynomial-time compilable to each other
  preserving plan size exactly.
\end{theorem}

\begin{proof}
  \PLl{} $\compilable^1_p$ \PLac{} follows from Lemma~\ref{L:pl:to:pa},
  Lemma~\ref{L:pa:to:pac} and Proposition~\ref{P:transitivity:reflexivity}.
  Using Propositions~\ref{P:transitivity:reflexivity}
  and~\ref{P:upward:compilability} and the fact that \PLac{} $\spec$ \PLlc{}
  $\spec$ \PLl{} and \PLac{} $\spec$ \PLa $\spec$ \PLl, the claim follows.
\end{proof}

\section{The Limits of Compilation when Preserving Plan Size Linearly}
\label{S:uncompilability}

The interesting question is, of course, whether there are other compilation
schemes preserving plan size exactly than those we have identified so far. As it turns
out, this is not the case. We will prove that for all pairs of formalisms for
which we have not identified a compilation scheme preserving plan size
exactly, such a
compilation scheme is impossible even if we allow for a linear increase of the
plan size. 
For some pairs of formalisms we are even able to prove that a
polynomial increase of the plan size would not help in establishing a
compilation scheme. These results are, however, conditional based on an
assumption that is slightly stronger than the $\Poly \neq \NP$ assumption.
A preview of the results of this section 
is given in Table~\ref{Tab:results}. 
\begin{table}[htb]
\begin{center}
\begin{tabular}{*{7}{c|}}
$\compilable^x$ & \PL{} & \classPLl{} & \PLc{} & \PLu{} & \PLuc{} &
\classPLlu{} \\
\hline
 & & $\not\compilable^p$ & $\not\compilable^p$ & $\not\compilable^c$ &
 $\not\compilable^p$ &  $\not\compilable^p$ \\
\raisehalf{\PL} & \raisehalf{$=$} &  Cor.~\ref{C:ppu:separation} &
Cor.~\ref{C:ppu:separation} & Cor.~\ref{C:p:to:plu} & Cor.~\ref{C:ppu:separation} &  Cor.~\ref{C:ppu:separation} \\
\hline
& & & & $\not\compilable^c$ & $\not\compilable^c$ & $\not\compilable^c$ \\
\raisehalf{\classPLl} & \raisehalf{$\spec$} & \raisehalf{$=$} &
\raisehalf{$\spec$} & {\bf Theo.~\ref{T:p:to:pu}} & Cor.~\ref{C:p:to:plu}  & Cor.~\ref{C:p:to:plu}  \\
\hline
 & & $\not\compilable^c$ & & $\not\compilable^c$ & $\not\compilable^c$ & $\not\compilable^c$ \\
\raisehalf{\PLc} & \raisehalf{$\spec$} & Cor.~\ref{C:pu:to:pl:plu} &
\raisehalf{$=$} & Cor.~\ref{C:p:to:plu}  & Cor.~\ref{C:p:to:plu}  & 
Cor.~\ref{C:pu:to:pl:plu}  \\
\hline
 & & $\not\compilable^p$ & $\not\compilable^p$ & & $\not\compilable^p$ &
 $\not\compilable^p$ \\
\raisehalf{\PLu} & \raisehalf{$\spec$} &  Cor.~\ref{C:ppu:separation} &
{\bf Theo.~\ref{T:p:pu:to:X}} & \raisehalf{$=$} & Cor.~\ref{C:ppu:separation}  &
Cor.~\ref{C:ppu:separation} \\
\hline
 & &  $\not\compilable^c$ & & & & $\not\compilable^c$ \\
\raisehalf{\PLuc} &  \raisehalf{$\spec$} & {\bf Theo.~\ref{T:puc:to:pl}} &
\raisehalf{$\spec$} &  \raisehalf{$\spec$} &  \raisehalf{$=$} &
Cor.~\ref{C:pu:to:pl:plu} \\
\hline
 & & & & & & \\
\raisehalf{\classPLlu} & \raisehalf{$\spec$} &  \raisehalf{$\spec$} &
\raisehalf{$\spec$} &  \raisehalf{$\spec$} &  \raisehalf{$\spec$} &
\raisehalf{$=$} \\
\hline
\end{tabular}
\caption{Separation Results}
\label{Tab:results}
\end{center}
\end{table}
The symbol
$\spec$ means that there exists a compilation scheme because the first
formalism is a specialization of the second one. In all the other cases, we
specify the separation and give the theorem number for this result.


\subsection{Conditional Effects Cannot be Compiled Away} 

First of all, we will prove that conditional effects cannot be compiled away.
The deeper reason for this is that with conditional effects, one can
independently do a number of things in parallel, which is impossible in
formalisms without conditional effects. If we consider, for example, the
operator $\sym{latex}$ from Example~\ref{Ex:1}, it is clear that it
"`propagates"' the truth value of $\sym{bbl}$ and $\sym{ind}$ to
$\sym{dvi\_cite\_ok}$ and $\sym{dvi\_ind\_ok}$, respectively---provided the
state specification satisfies the precondition. It is obviously possible to
come up with a set of exponentially many operators that can do the same thing
in one step.  However, it is unclear how to do that with less than
exponentially many operators. In fact, we will show that this is impossible.

In order to illustrate this point, let us generalize the above example.
We start with a set of $n$ propositional
atoms $\atomalph_n = \{\atomvar_1,\ldots,\atomvar_n\}$ and a disjoint copy of
this set: $\scopy{\atomalph_n} = \{ \scopy{\atomvar_i} \: | \: \atomvar_i \in
\atomalph_n\}$. Further, if $\statespec \subseteq \literals{\atomalph_n}$, then
$\scopy{\statespec}$ shall denote the corresponding set of   literals over
$\literals{\scopy{\atomalph_n}}$, i.e., 
\[ \scopy{\statespec} = \{ \scopy{\atomvar_i} \: | \: \atomvar_i \in \statespec\} \cup \{
\neg \scopy{\atomvar_i} \: | \: \neg \atomvar_i \in \statespec\}.\]
Consider now the following \PLl{} domain structure:
\begin{eqnarray*}
\atomalph_{2n} & = & \atomalph_n \cup \scopy{\atomalph_n}, \\
\opset_{2n} & = & \biggl\{ \langle \truth, \{ \atomvar_i \effimpl  \scopy\atomvar_{i}, 
\neg \atomvar_i \effimpl \neg \scopy{\atomvar_{i}} \:| \: \atomvar_i \in \atomalph_{n}\}
\rangle \biggr\}, \\
 \domainstructure_{2n}  & = & \langle \atomalph_{2n}, \:  \opset_{2n} \rangle.
\end{eqnarray*}
 From the construction it follows that for
all pairs $(\initial,\goal)$ such that $\initial$ is a consistent and complete
set over $\literals{\atomalph_n}$ and $\goal \subseteq  \scopy{\initial}$, the instance
$\planinstance = \langle \domainstructure_{2n}, \initial, \goal\rangle$ has a
one-step plan. Conversely, for all pairs $(\initial, \goal)$ with $\goal \cap
\literals{\scopy{\atomalph}}
\not\subseteq  \scopy{\initial}$, there does not exist a solution.

Trying to define a \PLu{} domain structure polynomially sized in
$\size{\domainstructure_{2n}}$ with the same property seems to be impossible,
even if we allow for $c$-step plans. However, in trying to prove this, it turns
out that an additional condition on the state-translation function is needed. 

We say that the state-translation functions are {\emdef local} iff
for all state specifications $\statespec$ and 
for $\atomalph_1 \cap \atomalph_2 = \emptyset$ we have 
\[ \transifun(\atomalph_1, \statespec \cap \literals{\atomalph_1}) \cap
\transgfun(\atomalph_2, \statespec \cap \literals{\atomalph_2}) = \emptyset.\] 
With locality as an additional condition on
state-translation functions  we could easily prove that conditional effects
cannot be compiled away.  Instead of doing so  we will show, however, that it
is possible to derive a weaker condition from the definition of compilation
schemes that will be enough to prove the impossibility result.  This weaker
condition is {\em quasi-locality} of state-translation functions relative to a
given set of symbols $\atomalph$, which in turn is based on the notion of {\em
  universal literals}. A literal $\litvar$ is called a {\emdef
  universal literal} for  given state-translation functions on
  $\atomalph$ iff one of the following conditions is satisfied:
\begin{enumerate}
\item for all $\atomvar \in \atomalph$: $\litvar \in \transifun(\{\atomvar\},
  \{\atomvar\})$, or
\item for all $\atomvar \in \atomalph$: $\litvar \in \transifun(\{\atomvar\},
  \{\neg \atomvar\})$, or
\item for all $\atomvar \in \atomalph$: $\litvar \in \transifun(\{\atomvar\},
  \emptyset)$, or
\item for all $\atomvar \in \atomalph$: $\litvar \in \transgfun(\{\atomvar\},
  \{\atomvar\})$, or
\item for all $\atomvar \in \atomalph$: $\litvar \in \transgfun(\{\atomvar\},
  \{\neg \atomvar\})$, or
\item for all $\atomvar \in \atomalph$: $\litvar \in \transgfun(\{\atomvar\},
  \emptyset)$.
\end{enumerate}
Let $\univlits$\label{D:univlits} denote the set of universal
literals. Now we define {\emdef quasi-locality} of state-translation functions
relative to a set of propositional atoms $\atomalph$ and the induced set of
universal literals
$\univlits$ as follows. For each
$\statespec \subseteq \litalph$ such that $\statespec \not\models \falsity$ and
for all pairs $\atomalph_1, \atomalph_2 \subseteq
\atomalph$ with $\atomalph_1 \cap \atomalph_2 = \emptyset$, we have
\[ \transifun(\atomalph_1, \statespec \cap \literals{\atomalph_1}) \cap
\transgfun(\atomalph_2, \statespec \cap \literals{\atomalph_2}) \subseteq
\univlits.\]
In words, the only {\em non-local} literals in quasi-local state-translation
functions are the universal literals.  

\begin{lemma}
\label{L:quasi-local}
For a given compilation scheme $\compfun = \compfuntuple$ and natural number
$n$, there exists a set of atoms $\atomalph \subseteq \allatoms$ such
that $\card{\atomalph} \geq n$\label{D:card} and $\transifun$ and $\transgfun$ are
quasi-local on $\atomalph$.
\end{lemma}

\begin{proof}
  Let $\transfun\colon \allatoms \rightarrow \powerset{\allatoms}$ be a
  function that has as the result the union of all results for all possible
  translations of a literal returned by the state-translation functions, i.e.,
\[\transfun(\atomvar) = \!\!\! 
\begin{array}[t]{l} \transifun(\{\atomvar\},\{\atomvar\}) \cup
\transifun(\{\atomvar\},\{\neg \atomvar\}) \cup
\transifun(\{\atomvar\},\emptyset) \cup \\ 
\transgfun(\{\atomvar\},\{\atomvar\}) \cup
\transgfun(\{\atomvar\},\{\neg \atomvar\}) \cup
\transgfun(\{\atomvar\},\emptyset).
\end{array}
\]
Set $\allatomssubset = \allatoms$ and $\univlits = \emptyset$. Now we choose an
infinite subset $\allatomssubset'$ of $\allatomssubset$ such that either
\begin{enumerate}
\item for all $\atomvar \in \allatomssubset'$, there are only finitely many
  other atoms $\atomvarq \in \allatomssubset'$ such that 
  $(\transfun(\atomvar) \cap \transfun(\atomvarq)) - \univlits \neq
  \emptyset$, or if such an infinite subset of $\allatomssubset$ does not exist, 
\item $\allatomssubset'$ has a universal literal $\litvar \not\in \univlits$
  and we set $\univlits' = \univlits \cup \{\litvar\}$. 
  
  Note that such an infinite subset  $\allatomssubset'$ must exist. The reason is that some
  literal $\litvar \not \in \univlits$ must occur for infinitely many atoms in
  $\transfun$ over $\allatomssubset$ because we could not find an infinite
  subset satisfying condition (1). Because for a single atom there are
  only six possible ways to generate $\litvar$, there must exist an infinite
  subset such that this literal occurs in all of either
  $\transxfun(\{\atomvar\}, \{\atomvar\})$, $\transxfun(\{\atomvar\}, \{\neg
  \atomvar\})$, or $\transxfun(\{\atomvar\}, \emptyset)$ (for $x = i,g$) and
  in this subset $\litvar$ is a universal literal.

\end{enumerate}  
If we can pick a subset satisfying the first condition, we can choose from it
a finite subset $\atomalph$ with any desired cardinality such that the
state-translation functions are quasi-local with respect to $\atomalph$ and
$\univlits$.

Otherwise we repeat the selection process with $\allatomssubset'$ and
$\univlits'$ until condition (1) is satisfied. This selection process can only
be repeated finitely often because otherwise there are some atoms $\atomvar$
such that $\transfun(\atomvar)$ has an infinite result, which is impossible
because the state-translation functions are polynomial-time computable and can
therefore have only finite results.

This demonstrates that there always {\em exists} a set of propositional atoms
such that the state-translation functions are quasi-local. However, we might
not be able to effectively determine this set.
\end{proof}

Using this result, we are finally able to prove the non-existence of
compilation schemes for compiling conditional effects away when preserving
plan size linearly.

\begin{theorem}
\label{T:p:to:pu}
\PLl{} cannot be compiled to \PLu{} preserving plan size linearly.
\end{theorem}

\begin{proof}
  Assume for contradiction that there exists a compilation scheme $\compfun$
  from \PLl{} to \PLu{} preserving plan size linearly, which compiles the
  domain structure $\domainstructure_{2n}$ defined above into the \PLu{} domain
  structure 
  \[ \compdsfun(\domainstructure_{2n}) = \domainstructure'_{2n} = \langle 
  \atomalph'_{2n}, \opset'_{2n}\rangle.\]
  Because of Lemma~\ref{L:quasi-local} we can assume that the set of atoms
  $\atomalph_{2n}$ is chosen such that the translation functions are
  quasi-local on this set.
  
  Let us now consider all initial state specifications $\initial$ that are
  consistent and complete over $\atomalph_n$ and do not contain only positive
  or only negative literals:
  \[\initial \in   \powerset{\literals{\atomalph_n}} - \{\atomalph_n, \neg
  \atomalph_n\}.\]
  Obviously, there are $2^n-2$ such state specifications. By assumption,
  each \PLu{} instance of the following form
\[ \langle \domainstructure'_{2n}, \: \transifun(\atomalph_{2n},\initial) 
\cup \compifun(\domainstructure_{2n}), \:
\transgfun(\atomalph_n,\scopy{\initial}) \cup
\compgfun(\domainstructure_{2n})\rangle\] has a $c$-step plan. Since there are
only $O(\card{\opset'_{2n}}^c)$ different $c$-step plans, which is a number
polynomial in the size of $\domainstructure_{2n}$, the same plan $\plan$ is
used for different initial states---provided $n$ is sufficiently large.

Suppose that the plan $\plan$ is used for the pairs
$(\initial'_1,\goal'_1), (\initial'_2,\goal'_2)$, which result from
$\initial_1$ and $\initial_2$:
\begin{eqnarray*}
\initial'_1 & = & \transifun(\atomalph_n,\initial_1) \cup
\compifun(\domainstructure_{2n}) \\
\goal'_1 & = & \transgfun(\atomalph_n,\scopy{\initial_1}) \cup
\compgfun(\domainstructure_{2n}) \\
\initial'_2 & = & \transifun(\atomalph_n,\initial_2) \cup
\compifun(\domainstructure_{2n}) \\
\goal'_2 & = & \transgfun(\atomalph_n,\scopy{\initial_2}) \cup
\compgfun(\domainstructure_{2n}) \\
\end{eqnarray*}
Since $\initial_1 \neq \initial_2$, $\initial_1$ and $\initial_2$ must differ
on at least one atom, say $\atomvar$. Without loss of generality we assume
$\atomvar \in \initial_1$ and $\neg\atomvar \in \initial_2$. Since $\plan$ is
a successful plan from $\initial'_1$ to $\goal'_1$ and because $\transgfun$
is modular, it follows that
\[\Result(\initial'_1,\plan) \supseteq \goal'_1 \supseteq
\transgfun(\{\scopy{\atomvar}\},\{\scopy{\atomvar}\}).\] 

Some of the literals in
$\transgfun(\{\scopy{\atomvar}\},\{\scopy{\atomvar}\})$ may be added by
operators in $\plan$ but none of the literals in
$\transgfun(\{\scopy{\atomvar}\},\{\scopy{\atomvar}\})$ can be deleted by an operator in
$\plan$ without reestablishing this literal by another operator after its
deletion.  Because $\plan$ contains only operators with unconditional effects,
it adds and deletes the same literals regardless of the initial state.  

Let us now assume that there exists a literal $\litvar \in
\transgfun(\{\scopy{\atomvar}\},\{\scopy{\atomvar}\})$ that is not added
by $\plan$. This implies that $\litvar \in \initial'_1$ and we have to
distinguish  three cases:
\begin{enumerate}
\item $\litvar \in \compifun(\domainstructure_{2n})$, from which we conclude that $\litvar \in \initial'_2$.
\item $\litvar \in \transifun(\{\scopy{\atomvar}\},\emptyset)
\subseteq \initial'_1$, which also implies that $\litvar \in \initial'_2$.
\item $\litvar \in \transifun(\{\atomvarq\}, \litset)$ with $\atomvarq \neq
  \scopy{\atomvar}$ and $\litset \in \{\{\atomvarq\},\{\neg \atomvarq\},
  \emptyset\}$.  Because we assumed that the state-translation functions are
  quasi-local on $\atomalph_{2n}$, $\litvar$ must be a universal literal. If
  $\litvar$ is universal for $\transifun$, then we will have $\litvar \in
  \initial'_2$ because the possible initial states contain positive and
  negative literals as well as no literal for some elements from
  $\atomalph_{2n}$. If $\litvar$ is universal for $\transgfun$, it is present
  in $\goal'_1$ and in $\goal'_2$ for the same reason. Further, because
  $\litvar$ is not added by $\plan$ and $\plan$ is a valid plan from
  $\initial'_2$ to $\goal'_2$, it must also be part of of $\initial'_2$.
\end{enumerate}

In other words, all literals  $\litvar \in
\transgfun(\{\scopy{\atomvar}\},\{\scopy{\atomvar}\})$ that are 
not added by $\plan$ are already in $\initial'_1$
and $\initial'_2$. From that we conclude that
\[ \Result(\initial'_2,\plan) \supseteq
\transgfun(\{\scopy{\atomvar}\},\{\scopy{\atomvar}\}). \]

Now let
\begin{eqnarray*}
\goal''_2 & = & \transgfun(\atomalph_{2n} - \{\scopy{\atomvar}\},\scopy{\initial_2} - \{\neg\scopy{\atomvar}\}) \cup
\compgfun(\domainstructure_{2n}), \\
\goal'''_2 & = & \goal''_2 \cup \transgfun(\{\scopy{\atomvar}\}, \{\scopy{\atomvar}\}) \\
 & = & \transgfun(\atomalph_{2n},\scopy{\initial_2} - \{\neg\scopy{\atomvar}\} \cup
\{\scopy{\atomvar}\}) \cup
\compgfun(\domainstructure_{2n}).
\end{eqnarray*}
Because $\transgfun$ is modular, it is clear that $\goal'_2 \supseteq
\goal''_2$ and therefore $\Result(\initial'_2,\plan) \supseteq \goal''_2$.
Because $\plan$ achieves $\goal''_2$ as well as
$\transgfun(\{\scopy{\atomvar}\},\{\scopy{\atomvar}\})$, it follows that (again because
$\transgfun$ is modular), $\plan$ achieves also $\goal'''_2$.

Since $\langle \domainstructure_{2n}, \initial_2, \scopy{\initial_2} - 
\{\neg\scopy{\atomvar}\} \cup \{\scopy{\atomvar}\}\rangle$ does not have any plan, 
there should not be any plan for $\langle \domainstructure'_{2n}, \initial'_2,
\goal'''_2\rangle$. The fact that $\plan$ is a plan for this instance implies
that $\compfun$ cannot be a compilation scheme, which is the desired contradiction. 
\end{proof}

Using Propositions~\ref{P:transitivity:reflexivity}
and~\ref{P:upward:compilability} as well as
Theorem~\ref{T:conditional:no:formulae}, this result can be generalized as
follows (see also Table~\ref{Tab:results}).

\begin{corollary}
\label{C:p:to:plu}
\PL, \PLc, and \classPLl{} cannot be compiled to \PLu{} or any formalism
specializing \PLu{} preserving plan size linearly.
\end{corollary}

This answers the question of whether more space efficient compilation
schemes from \PLlc{} to \PLauc{} than the one proposed by Gazen and
Knoblock \shortcite{gazen:knoblock:ecp-97} are possible. Even assuming
unbounded computational resources for the compilation process, a more
space efficient compilation scheme is impossible---provided that the
compilation should preserve plan size linearly.\footnote{This result
  demonstrates that the choice of the semantics can be very important.
  If we interpret conditional effects sequentially as Brewka and
  Hertzberg \citeyear{brewka:hertzberg:jlc-93} do, then there exists
  an straightforward compilation scheme preserving plan size exactly.}
If we allow polynomially larger plans, then efficient compilation
schemes are possible (see Section~\ref{S:polynomial:compilability}).




\subsection{Non-Uniform Complexity Classes} 
\label{S:non-uniform}

In the next section we make use of so-called {\em non-uniform complexity
  classes}, which are defined using {\em advice-taking machines}, in order to
prove the impossibility of a compilation scheme.
An {\emdef advice-taking Turing machine} is a Turing machine with an {\emdef
  advice oracle}, which is a (not necessarily recursive) function $\advice$
from positive integers to bit strings. On input $\instance$,\label{D:instance} the machine loads
the bit string $\advice(\size{\instance})$\label{D:advice} and then continues as usual. Note
that the oracle derives its bit string only from the length of the input and
not from the contents of the input.  An advice is said to be {\emdef
  polynomial} if the oracle string is polynomially bounded by the instance
size. Further, if $\classX$\label{D:classX} is a complexity class defined in terms of
resource-bounded machines, e.g., \Poly{} or \NP, then ${\classX/\poly}$ (also
called {\emdef non-uniform \classX}) is the class of problems that can be
decided on machines with the same resource bounds and polynomial advice.

Because of the advice oracle, the class \Ppoly{} appears to be much more
powerful than \Poly. However, it seems unlikely that \Ppoly{}\label{D:Ppoly} contains all of
\NP. In fact, one can prove that $\NP \subseteq \Ppoly$ implies certain
relationships between uniform complexity classes that are believed to be very
unlikely. For stating this result, we first have to introduce the 
{\em polynomial hierarchy}. 

Let \classX\ be a class of decision problems. Then $\Poly^{\classX}$ denotes
the class of decision problems $\problem$ that can be decided in polynomial
time by a deterministic Turing machine  that is allowed to use a
procedure---a so-called {\emdef oracle}---for deciding a problem $\problemq
\in \classX$, whereby executing the procedure does only cost constant time.
Similarly, $\NP^{\classX}$ denotes the class of decision problems $\problem$
such that there is a nondeterministic Turing-machine that solves all instances
of $\problem$ in polynomial time using an oracle for $\problemq \in
{\classX}$. Based on these notions, the sets $\Delta^p_k$, $\Sigma^p_k$, and
$\Pi^p_k$ are defined as follows:\footnote{The super-script $p$ is only used to
  distinguish these sets from the analogous sets in the Kleene hierarchy.}
\begin{eqnarray*}
\Delta^p_0 & = & \Sigma^p_0 \: = \: \Pi^p_0 \: = \: \Poly, \\
\Delta^p_{k+1} & = & \Poly^{\Sigma^p_k}, \label{D:Deltapi} \\
\Sigma^p_{k+1} & = & \NP^{\Sigma^p_k}, \label{D:Sigmapi} \\
\Pi^p_{k+1} & = &  \coNP^{\Sigma^p_{k}}.\label{D:Pipi}
\end{eqnarray*}
Thus, $\Sigma^p_1 = \NP$ and $\Pi^p_1 = \coNP$. The set of all classes defined
in this way is called the {\emdef polynomial hierarchy}, denoted by \PH.\label{D:PH}  Note
that \[\PH = \bigcup_{k\geq 0} \Delta^p_k = \bigcup_{k\geq 0} \Sigma^p_k =
\bigcup_{k\geq 0} \Pi^p_k \subseteq \PSPACE.\] Further we have, $\Delta^p_{k}
\subseteq \Sigma^p_{k} \cap \Pi^p_{k}$ and $\Sigma^p_{k}, \Pi^p_{k} \subseteq
\Delta_{k+1}$.  As with other classes, it is unknown whether the inclusions
between the classes are proper. However, it is strongly believed that this is
the case, i.e., that the hierarchy is truly infinite.

Based on the firm belief that the polynomial hierarchy is proper, the above
mentioned question of whether $\NP \subseteq \Ppoly$ can be answered.  It has
been shown that $\NP \subseteq \Ppoly$ would imply that the {\em polynomial
  hierarchy} collapses on the second level \cite{karp:lipton:ens-math-82}, i.e.,
$\Sigma^p_2 = \Pi^p_2$. This, however, is considered to be quite unlikely.
Further, it has been shown that $\NP \subseteq \coNPpoly$\label{D:coNPpoly} or $\coNP \subseteq
\NPpoly$\label{D:NPpoly} implies that the polynomial hierarchy collapses at the third level
\cite{yap:tcs-83}, i.e., $\Sigma^p_3 = \Pi^p_3$, which again is considered to
be very unlikely.  We will use these result for proving that for some pairs of
formalisms it is very unlikely that one formalism can be compiled into the
other one.


\subsection{On the Expressive Power of Partial State Specifications and Boolean
  Formulae} 
\label{S:partial:state:and:formulae}

In all the cases considered so far, operators over partial state
specifications could be compiled to operators over complete state
specifications, i.e., partial state specifications did not add any
expressiveness.  This is no longer true, however, if we also allow for
arbitrary boolean formulae in preconditions and effect conditions. In this case, we can
decide the \coNP-complete problem of whether a formula is a tautology by
deciding whether a one-step plan exists. Asking, for example, if the 
\PLu-instance $\langle \atomalph, \{ \langle \formula, \newgoal \rangle\},
\emptyset, \{\newgoal\}\rangle$ has a plan is equivalent to asking whether
$\formula$ is a tautology.

Let the {\emdef one-step plan existence problem} (1-\planex{}) be the
\planex{} problem restricted to plans of size  one. From the above it is
evident that \PL-1-\planex{} and \PLu-1-\planex{} are \coNP-hard.  Let $p$ be
some fixed polynomial, then the {\emdef polynomial step plan-existence
  problem} ($p$-\planex) is the \planex{} problem restricted to plans that
have length bounded by $p(n)$, if $n$ is the size of the planning instance. As
is easy to see, this problem is in \NP{} for all formalisms except \PL{} and
\PLu{}. The reason is that after guessing a sequence of operators and state
specifications of polynomial size, one can verify for each step in polynomial
time that the precondition is satisfied by the current state specification and
produces the next state specification. Since there are only polynomially many
steps, the overall verification takes only polynomial time.

\begin{proposition}
\label{P:complete:state:in:NP}
$\planfx$-$p$-\planex{} can be solved in polynomial time on a nondeterministic
Turing machine for all formalisms different from \PL{} and \PLu.
\end{proposition}

From the fact that \PLu-1-\planex{} is \coNP-hard and, e.g., \PLc-p-\planex{}
is in \NP{}, it follows almost immediately that there is no {\em
  polynomial-time} compilation scheme from \PLu{} to \PLc{} that preserves
plan length polynomially (if $\NP\neq \coNP$). However, even if we allow for
unbounded computational resources of the compilation process, a proof
technique first used by Kautz and Selman \shortcite{kautz:selman:aaai-92} can
be used to show that such a compilation scheme cannot exist (provided
$\Sigma^p_3 \neq \Pi^p_3$).


\begin{theorem} 
\label{T:p:pu:to:X}
\PLu{} cannot be compiled to \PLc{}  preserving plan size polynomially, unless $\Sigma^p_3 = \Pi^p_3$. 
\end{theorem}

\begin{sloppypar}
\begin{proof}
  Let $\formula$ be a propositional formula of size $n$ in conjunctive
  normal form with three literals per clause. As a first step, we
  construct for each $n$ a \PLu{} domain structure $\domainstructure_n$ with
  size polynomial in $n$ and the following properties.  Unsatisfiability of an
  arbitrary 3CNF formula $\formula$ of size $n$ is equivalent to $1$-step
  plan existence for the \PLu-$1$-\planex{} instance
  $\langle\domainstructure_n,\initial_{\formula},\{\newgoal\}\rangle$, where
  $\initial_{\formula}$ can be computed in polynomial time from
  $\formula$.
  
  Given a set of $n$ atoms, denoted by $\propatomalph_n$, we define the set of
  clauses $\allclauses_n$ to be the set containing all clauses with three
  literals that can be built using these atoms.  The size of $\allclauses_n$
  is $O(n^3)$, i.e., polynomial in $n$. Let $\allclausealph_n$ be a set of new atoms
  $\atomvar_{\{\litvar_1,\litvar_2,\litvar_3\}}$ corresponding one-to-one to
  the clauses in $\allclauses_n$. Further, let
  \[\Formula_n = \bigwedge \biggl\{ \: (\litvar_1 \vee \litvar_2 \vee 
  \litvar_3 \vee
  \atomvar_{\{\litvar_1,\litvar_2,\litvar_3\}}) \: | \:
  \{\litvar_1,\litvar_2,\litvar_3\} \in \allclauses_n \biggr\}.\]
  
  We now construct a \PLu{} domain structure $\domainstructure_n = \langle
  \atomalph_n, \opset_n\rangle$ for all formulae of size $n$ as follows:
  \begin{eqnarray*}
    \atomalph_n & = & \propatomalph_n \cup \allclausealph_n \cup 
    \{\newgoal\}, \\
    \opset_n & = & \{\langle \{ \neg \Formula_n \}, \{ \newgoal \} \rangle \}.
  \end{eqnarray*}
  Let $\clauseset$ be a function that determines for all 3CNF formulae
  $\formula$, which atoms in $\allclausealph_n$ correspond to the clauses in
  the formula , i.e.,
  \[ \clauseset(\formula) = \{ \atomvar_{\{\litvar_1,\litvar_2,\litvar_3\}} \:
  | \: \{\litvar_1,\litvar_2,\litvar_3\} \in \formula\}.\] Now, the initial
  state for any particular formula $\formula$ of size $n$ is computed as
  follows:
  \[ \initial_{\formula} = \neg \clauseset(\formula) \cup (\allclausealph_n -
  \clauseset(\formula)) \cup \{\neg \newgoal\}. \]
  \begin{sloppypar}
    From the construction, it follows that there exists a one-step plan for $\langle \atomalph_n, 
    \opset_n, \initial_{\formula}, \{\newgoal\}\rangle$ 
    iff $\formula$ is unsatisfiable.
  \end{sloppypar}
  
  Let us now assume that there exists a compilation scheme $\compfun$  from \PLu{} to \PLc{} preserving plan size
  polynomially. Further, let us assume that the \PLu{} domain structure
  $\domainstructure_n$ is compiled to the \PLc{} domain structure
  $\domainstructure'_n = \langle \atomalph'_n, \opset'_n\rangle$. Using this
  compiled domain structure, we can construct the
  following advice-taking Turing machine.
  
    On input of a formula $\formula$ of size $n$, we load the advice
    $\langle\domainstructure'_n,\compifun(\atomalph_n,\opset_n),
    \compgfun(\atomalph_n,\opset_n)\rangle$. This advice is polynomial because
    $\domainstructure_n$ is polynomial in the size of $\formula$ and a
    compilation scheme generates only polynomially larger domain structures.  Because
    $\transifun$ is a polynomial-time function and $\initial_{\formula}$ can
    be computed from $\formula$ in polynomial time, we
    can compute 
    \[\initial'= \transifun(\atomalph_n,\initial_{\formula}) \cup 
    \compifun(\atomalph_n,\opset_n)\] in polynomial time. Also the goal
    specification \[\goal' = \transgfun(\atomalph_n,\{\newgoal\}) \cup
    \compgfun(\atomalph_n,\opset_n)\] can be computed in polynomial time.
    Finally, we decide the $p$-\planex{} problem on the resulting \PLc-instance
    $\langle \domainstructure'_n, \initial', \goal'\rangle$.  From
    Proposition~\ref{P:complete:state:in:NP} we know that this can be done in
    polynomial time on a nondeterministic Turing machine.
  
  Because deciding $p$-\planex{} for $\langle \domainstructure'_n, \initial',
  \goal'\rangle$ is equivalent to deciding $1$-\planex{} for $\langle
  \domainstructure_n, \initial_{\formula}, \{\newgoal\}\rangle$, which is in
  turn equivalent to deciding unsatisfiability of $\formula$, it follows that
  we can decide a \coNP-complete problem on a nondeterministic, polynomial
  advice-taking Turing machine in polynomial time. From that it follows that
  $\coNP \subseteq \NP/\poly$. Using Yap's \shortcite{yap:tcs-83} result, the
  claim follows.
\end{proof}
\end{sloppypar}

Using Proposition~\ref{P:transitivity:reflexivity} and
Proposition~\ref{P:upward:compilability}, the above result generalizes as
follows (see also Table~\ref{Tab:results}).

\begin{corollary}
\label{C:ppu:separation}
\PL{} and \PLu{} cannot be compiled to any of the other planning formalisms
preserving plan size polynomially, unless $\Sigma^p_3 = \Pi^p_3$.
\end{corollary}

If we restrict the form of the formulae, however, we may be able to devise
compilation schemes from \PLu{} to, e.g., \PLuc.  Reconsidering the proof of
the last theorem, it turns out that it is essential to use the negation of a
CNF formula as a precondition. If we restrict ourselves to CNF formulae in
preconditions, it seems possible to move from partial to complete state
descriptions using ideas similar to the ones used in the proof of
Lemma~\ref{L:pa:to:pac}.

\begin{sloppypar}
However, no such compilation scheme will work for \PL{}. The reason is the condition
$\Eff(\statespec,\post(\op)) =  \Pot(\statespec,\post(\op))$ in the definition
of the function $\res$. If this condition is not satisfied, the result of the
operator is inconsistent. This condition could be easily employed to reduce
{\em unsatisfiability} of CNF formulae to 1-step plan existence, which 
enables us to use the same technique as in the proof of the above theorem.
\end{sloppypar}

\subsection{Circuit Complexity}
\label{S:circuit:complexity}

For the next impossibility result we need the notions of {\em boolean circuits}
and {\em families of circuits}.  A {\emdef boolean circuit} is a directed,
acyclic graph $\circuit = (\vertices,\edges)$,\label{D:circuit} where the nodes $\vertices$ are
called {\emdef gates}.  Each gate $\node \in \vertices$ has a type $\gtype(\node) \in
\{\neg, \vee, \wedge, 1, 0 \} \cup \{\var_1, \var_2, \ldots\}$. The gates with
$\gtype(\node) \in \{1,0,\var_1,\var_2,\ldots\}$ have in-degree zero, the
gates with $\gtype(\node) \in \{\neg\}$ have in-degree one, and the gates with $\gtype(\node) \in \{\wedge,
\vee\}$ have in-degree two. All gates except one have at least one outgoing
edge. The gate with no outgoing edge is called the {\emdef output gate}. The gates
with no incoming edges are called the {\emdef input gates}.  The {\emdef depth} of
a circuit is the length of the longest path from an input gate to the output
gate. The {\emdef size} of a circuit is the number of gates in the circuit.

Given a {\em value assignment} to the variables $\{\var_1, \var_2, \ldots\}$,
the circuit computes the value of the output gate in the obvious way. For
example, for $\var_1 = 1$ and $\var_2 = 0$ we get the value 1 at the output
gate of the circuit shown in Figure~\ref{F:circuit:example}.

\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{0.00058333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(1298,1994)(0,-10)
\put(370,1764){\ellipse{416}{416}}
\put(370,1719){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\wedge$}}}}}
\put(1045,1104){\ellipse{416}{416}}
\put(1045,1059){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg$}}}}}
\path(377,197)(377,1554)
\blacken\path(407.000,1434.000)(377.000,1554.000)(347.000,1434.000)(407.000,1434.000)
\path(887,1254)(527,1625)
\blacken\path(632.096,1559.772)(527.000,1625.000)(589.037,1517.988)(632.096,1559.772)
\path(1045,189)(1044,898)
\blacken\path(1074.169,778.042)(1044.000,898.000)(1014.169,777.958)(1074.169,778.042)
\put(1037,39){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$x_2$}}}}}
\put(370,39){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$x_1$}}}}}
\end{picture}
}

\caption{Example of a boolean circuit}
\label{F:circuit:example}
\end{center}
\end{figure}

Instead of using circuits for computing boolean functions, we can also use
them for accepting words of length $n$ in $\seq{\{0,1\}}$. A word $\word =
\var_1 \ldots \var_n \in \{0,1\}^n$\label{D:word} is now interpreted as a value assignment
to the $n$ input variables $\var_1,\ldots,\var_n$ of a circuit. The word is {\emdef accepted} iff the
output gate has value 1 for this word. In order to deal with words of
different length, we need one circuit for each possible length.  A {\emdef
  family of circuits} is an infinite sequence $\famcircuits = (\circuit_0,
\circuit_1, \ldots)$,\label{D:famcircuits} where $\circuit_n$ has $n$ input variables. The language
accepted by such a family of circuits is the set of words $\word$ such that
$\circuit_{\size{\word}}$ accepts $\word$.

Usually, one considers so-called {\emdef uniform} families of
circuits, i.e., 
circuits that can be generated on a Turing machine with a $\log n$-space
bound. Sometimes, however, also non-uniform families are interesting. For
example, the class of languages accepted by non-uniform families of
polynomially-sized circuits is just the class \Ppoly{} introduced in
Section~\ref{S:non-uniform}.

Using restrictions on the size and depth of the circuits, we can now define
new complexity classes, which in their uniform variants are all subsets of
\Poly. One class that is important in the following is the class of
languages accepted by uniform families of circuits with polynomial size and logarithmic depth,
named \NCone.\label{D:NCone} Another class which proves to be important for us is defined in
terms of non-standard circuits, namely circuits with gates that have {\em
  unbounded fan-in}. Instead of restricting the in-degree of each gate to be
two at maximum, we now allow an unbounded in-degree. 
The class of languages accepted by families of polynomially sized circuits
with unbounded fan-in and constant depth is called \ACzero.\label{D:ACzero} 

From the definition, it follows almost immediately that \ACzero{} $\subseteq$
\NCone. Moreover, it has been shown that there are some languages in \NCone{}
that are not in the non-uniform variant of \ACzero, which implies that
\ACzero{} $\neq$ \NCone{} \cite{furst:et:al:mst-84}.


\subsection{Boolean Formulae Cannot be Compiled to Conditional Effects}
\label{S:logical:formulae:cannot:compiled}

As we have seen in Section~\ref{S:partial:state:and:formulae}, Boolean
formulae are quite expressive if they are used in combination with 
partial state specifications. However, what if all state specifications are
complete? In this case, it seems to be possible to simulate
the evaluation of CNF formulae by using conditional effects. In fact, it is
possible to compile in polynomial-time, for example, \PLuc{} to \PLlc{}
preserving plan size linearly, provided all formulae are in conjunctive normal
form.  Each operator would have to be split into two operators, one that
evaluates the clauses of all the formulae in the original operator and one that
combines these evaluations and takes the appropriate actions, e.g., asserting
$\falsity$ if the precondition is not satisfied. Sequencing of these pairs of
operators can be achieved by introducing some extra literals.

What can we say about the general case, however? When trying to simulate the
evaluation of an arbitrary logical formula using conditional effects, it seems
to be the case that we need as many operators as the nesting depth of the
formula, which means that we would need plans that cannot be bounded to be
only linearly longer than the original plans.

We will use the results sketched in Section~\ref{S:circuit:complexity} to
separate \PLuc{} and \PLlc{}. In order to do so, let us view domain structures
with fixed size plans as ``machines'' that accept languages.  For all words
$\word$ consisting of $n$ bits, let
\[\domainstructure_n = \langle \atomalph_n \cup
\{\newgoal\}, \opset_n\rangle.\]
Assume that the atoms in $\atomalph_n$ are numbered from 1 to $n$. Then a word
$\word$ consisting of $n$ bits could be encoded by the set of literals
\[ \initial_{\word} = \{ \atomvar_i \: | \: \mbox{\ if the $i$th bit of $\word$ is
  $1$} \} \cup \{ \neg \atomvar_i \: | \: \mbox{\ if the $i$th bit of
  $\word$ is $0$} \}.\] Conversely, for a consistent state specification $\statespec \in
  \literals{\atomalph_n}$, let $\word_{\statespec}$ be a word such
that the $i$th bit is 1 iff $\atomvar_i \in \statespec$.

We now say that the $n$-bit word $\word$ is {\emdef accepted with a one-step
  or $c$-step plan} by $\domainstructure_n$ iff there exists a one-step or
$c$-step plan, respectively, for the instance \[\planinstance_n = \langle
\langle\atomalph_n \cup \{\newgoal\}, \opset_n\rangle, \initial_{\word} \cup \{\neg g\},
\{g\} \rangle.\] Similarly to families of circuits, we also define families of
domain structures, $\famdom = (\domainstructure_0, \domainstructure_1,
\ldots)$.\label{D:famdom}  The language accepted by such a family with a one-step (or
$c$-step) plan is the set of words accepted using the domain structure
$\domainstructure_n$ for words of length $n$.  Borrowing the notion of
  uniformity as well, we say that a family of domain structures is {\emdef
  uniform} if it can be generated by a $\log n$-space Turing machine.

\begin{sloppypar}
Papadimitriou has pointed out that the languages accepted by {\em uniform
  polynomially-sized boolean expressions} is identical to \NCone{}
\cite[p.~386]{papadimitriou:94}. As is easy to see, a family of \PLuc{} domain
structures is nothing more than a family of boolean expressions, provided we
use one-step plans for acceptance.
\end{sloppypar}

\begin{proposition}
\label{P:nc}
The class of languages accepted by uniform families of \PLuc{} domain
structures using one-step plan acceptance is identical to \NCone.
\end{proposition}

If we now have a closer look at what the power of $c$-step plan acceptance for
families of \PLlc{} domain structures is, it turns out that it is less
powerful than \NCone. In order to show that, we will first prove the following
lemma that relates $c$-step \PLlc{} plans to circuits with gates of unbounded fan-in.

\begin{lemma}
\label{L:plan:circuit}
Let $\domainstructure=\domainstructuretuple$ be a \PLlc{} domain structure, let
$\goal \subseteq \litalph$, and let $\plan$ be a $c$-step plan over
$\domainstructure$.  Then there exists a polynomially sized boolean circuit
$\circuit$ with unbounded fan-in and depth $7c+2$ such that $\plan$ is a plan
for $\langle \domainstructure, \initial, \goal\rangle$ iff the circuit
$\circuit$ has value 1 for the input $\word_{\initial}$.
\end{lemma}

\begin{proof}
  The general structure of a circuit for a $c$-step \PLlc{} plan is displayed
  in Figure~\ref{F:circuits:goal}. 
\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{0.00058333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(5053,2654)(0,-10)
\put(272,699){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(272,504){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(272,309){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(969,729){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(969,534){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(969,339){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(2199,744){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(2199,549){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(2199,354){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(2769,744){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(2769,549){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(2769,354){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(1637,2424){\ellipse{416}{416}}
\put(1637,2379){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\wedge$}}}}}
\put(4157,1749){\ellipse{416}{416}}
\put(4157,1704){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\vee$}}}}}
\put(1659,759){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(1659,564){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(1659,369){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}.}}}}}
\put(1367,1749){\ellipse{416}{416}}
\put(1367,1704){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg$}}}}}
\put(2997,2109){\ellipse{416}{416}}
\put(2997,2064){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg$}}}}}
\path(287,1119)(1412,2424)
\blacken\path(1356.370,2313.523)(1412.000,2424.000)(1310.925,2352.699)(1356.370,2313.523)
\path(2762,1074)(1839,2349)
\blacken\path(1933.668,2269.389)(1839.000,2349.000)(1885.067,2234.205)(1933.668,2269.389)
\path(962,1074)(1277,1569)
\blacken\path(1237.885,1451.654)(1277.000,1569.000)(1187.265,1483.867)(1237.885,1451.654)
\path(1487,1919)(1647,2214)
\blacken\path(1616.159,2094.213)(1647.000,2214.000)(1563.417,2122.819)(1616.159,2094.213)
\path(4157,1074)(4157,1534)
\blacken\path(4187.000,1414.000)(4157.000,1534.000)(4127.000,1414.000)(4187.000,1414.000)
\path(4562,1074)(4287,1579)
\blacken\path(4370.736,1487.960)(4287.000,1579.000)(4318.042,1459.265)(4370.736,1487.960)
\path(3752,1074)(4027,1579)
\blacken\path(3995.958,1459.265)(4027.000,1579.000)(3943.264,1487.960)(3995.958,1459.265)
\path(3967,1839)(3201,2068)
\blacken\path(3324.565,2062.371)(3201.000,2068.000)(3307.379,2004.885)(3324.565,2062.371)
\drawline(2797,2184)(2797,2184)
\path(2797,2174)(1850,2458)
\blacken\path(1973.560,2452.265)(1850.000,2458.000)(1956.325,2394.794)(1973.560,2452.265)
\put(2229,999){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}. . . . .}}}}}
\put(2229,99){\makebox(0,0)[b]{\smash{{{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}. . . . .}}}}}
\put(324,54){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^0_1$}}}}}
\put(999,54){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^0_2$}}}}}
\put(1674,54){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^0_3$}}}}}
\put(2762,39){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^0_n$}}}}}
\put(2762,939){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^c_n$}}}}}
\put(1674,954){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^c_3$}}}}}
\put(999,954){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^c_2$}}}}}
\put(324,954){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^c_1$}}}}}
\put(4157,959){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}. . .}}}}}
\put(3757,909){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\falsity_1$}}}}}
\put(4577,909){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\falsity_m$}}}}}
\end{picture}
}

\caption{Circuit structure and goal testing for a $c$-step \PLlc{} plan}
\label{F:circuits:goal}
\end{center}
\end{figure}
For each plan step (or level) $j$ and each atom $\atomvar_i$, there is a
connection $\atomvar^j_i$. The connections on level $0$ are the input gates,
i.e., $\atomvar^0_i = \var_i$.  The goal test is performed by an $\wedge$-gate
that checks that all the goals are true on level $c$, in our case $\goal =
\{\atomvar_1, \neg \atomvar_2, \atomvar_n\}$. Further, using the $\vee$-gate,
it is checked that no inconsistency was generated when executing the plan.

For each plan step $j$, it must be computed whether the precondition is
satisfied and what the result of the conditional effects are.
Figure~\ref{F:circuits:action}~(a) displays the precondition test for the 
precondition $\{\atomvar_1,\atomvar_2,\neg\atomvar_3\}$. If the
conjunction of the precondition literals is not true,  $\falsity_k$
becomes true, which is connected to the $\vee$-gate in Figure~\ref{F:circuits:goal}.
\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{0.00058333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(7246,4320)(0,-10)
\put(3510,2334){\ellipse{416}{416}}
\put(6247,3699){\ellipse{416}{416}}
\put(945,3294){\ellipse{416}{416}}
\put(945,3249){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg$}}}}}
\put(975,2379){\ellipse{416}{416}}
\put(975,2334){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\wedge$}}}}}
\put(1425,1494){\ellipse{416}{416}}
\put(1425,1449){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg$}}}}}
\put(4005,1434){\ellipse{416}{416}}
\put(3510,3234){\ellipse{416}{416}}
\put(5467,1674){\ellipse{416}{416}}
\put(6142,1667){\ellipse{416}{416}}
\put(6547,2342){\ellipse{416}{416}}
\put(6720,3009){\ellipse{416}{416}}
\put(5812,2979){\ellipse{416}{416}}
\path(945,2589)(945,3084)
\blacken\path(975.000,2964.000)(945.000,3084.000)(915.000,2964.000)(975.000,2964.000)
\path(945,3519)(945,3954)
\blacken\path(975.000,3834.000)(945.000,3954.000)(915.000,3834.000)(975.000,3834.000)
\path(990,579)(989,2165)
\blacken\path(1019.076,2045.019)(989.000,2165.000)(959.076,2044.981)(1019.076,2045.019)
\path(300,594)(820,2229)
\blacken\path(812.219,2105.552)(820.000,2229.000)(755.041,2123.737)(812.219,2105.552)
\path(1635,594)(1454,1284)
\blacken\path(1513.466,1175.539)(1454.000,1284.000)(1455.430,1160.315)(1513.466,1175.539)
\path(1320,1654)(1132,2229)
\blacken\path(1197.807,2124.265)(1132.000,2229.000)(1140.778,2105.619)(1197.807,2124.265)
\path(2859,551)(3369,2171)
\blacken\path(3361.581,2047.530)(3369.000,2171.000)(3304.350,2065.547)(3361.581,2047.530)
\path(4225,556)(4030,1231)
\blacken\path(4092.126,1124.040)(4030.000,1231.000)(4034.483,1107.388)(4092.126,1124.040)
\path(3505,2544)(3510,3014)
\blacken\path(3538.722,2893.688)(3510.000,3014.000)(3478.725,2894.326)(3538.722,2893.688)
\path(3510,3439)(3510,3909)
\blacken\path(3540.000,3789.000)(3510.000,3909.000)(3480.000,3789.000)(3540.000,3789.000)
\path(2272,2559)(3300,3189)
\blacken\path(3213.361,3100.718)(3300.000,3189.000)(3182.009,3151.876)(3213.361,3100.718)
\path(5437,579)(5438,1462)
\blacken\path(5467.864,1341.966)(5438.000,1462.000)(5407.864,1342.034)(5467.864,1341.966)
\path(5437,594)(6030,1484)
\blacken\path(5988.428,1367.502)(6030.000,1484.000)(5938.496,1400.771)(5988.428,1367.502)
\path(6135,542)(6135,1454)
\blacken\path(6165.000,1334.000)(6135.000,1454.000)(6105.000,1334.000)(6165.000,1334.000)
\path(6135,542)(5532,1465)
\blacken\path(5622.747,1380.947)(5532.000,1465.000)(5572.516,1348.131)(5622.747,1380.947)
\path(5295,1787)(4860,2004)
\blacken\path(4980.772,1977.278)(4860.000,2004.000)(4953.989,1923.588)(4980.772,1977.278)
\path(6135,1877)(5899,2784)
\blacken\path(5958.251,2675.421)(5899.000,2784.000)(5900.184,2660.313)(5958.251,2675.421)
\path(5850,3204)(6082,3564)
\blacken\path(6042.213,3446.880)(6082.000,3564.000)(5991.779,3479.383)(6042.213,3446.880)
\path(6900,542)(6897,2893)
\blacken\path(6927.153,2773.038)(6897.000,2893.000)(6867.153,2772.962)(6927.153,2773.038)
\path(6322,1794)(6537,2132)
\blacken\path(6497.907,2014.647)(6537.000,2132.000)(6447.281,2046.850)(6497.907,2014.647)
\path(6540,2559)(6540,2893)
\blacken\path(6570.000,2773.000)(6540.000,2893.000)(6510.000,2773.000)(6570.000,2773.000)
\path(6705,3219)(6409,3560)
\blacken\path(6510.318,3489.044)(6409.000,3560.000)(6465.007,3449.713)(6510.318,3489.044)
\path(6255,3917)(6255,4157)
\blacken\path(6285.000,4037.000)(6255.000,4157.000)(6225.000,4037.000)(6285.000,4037.000)
\path(3885,1594)(3669,2192)
\blacken\path(3737.982,2089.329)(3669.000,2192.000)(3681.551,2068.945)(3737.982,2089.329)
\path(2701,2525)(3376,3065)
\blacken\path(3301.037,2966.611)(3376.000,3065.000)(3263.555,3013.463)(3301.037,2966.611)
\path(5440,590)(5441,591)(5442,595)
        (5445,600)(5449,609)(5454,622)
        (5462,640)(5471,661)(5482,687)
        (5495,717)(5510,752)(5526,790)
        (5544,831)(5563,875)(5582,921)
        (5602,968)(5622,1016)(5642,1065)
        (5661,1113)(5680,1161)(5698,1208)
        (5716,1253)(5732,1297)(5747,1340)
        (5761,1381)(5774,1420)(5786,1458)
        (5796,1495)(5805,1530)(5814,1565)
        (5821,1599)(5827,1633)(5832,1667)
        (5837,1702)(5841,1737)(5844,1774)
        (5847,1813)(5849,1853)(5850,1895)
        (5850,1939)(5851,1985)(5850,2032)
        (5849,2082)(5848,2133)(5846,2185)
        (5844,2239)(5842,2292)(5839,2345)
        (5837,2398)(5834,2449)(5831,2497)
        (5829,2543)(5826,2585)(5824,2623)
        (5822,2657)(5820,2686)(5819,2710)
        (5817,2729)(5816,2743)(5815,2765)
\blacken\path(5850.418,2646.486)(5815.000,2765.000)(5790.480,2643.762)(5850.418,2646.486)
\put(300,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^j_1$}}}}}
\put(975,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^j_2$}}}}}
\put(1650,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^j_3$}}}}}
\put(945,3999){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\falsity_k$}}}}}
\put(6217,39){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}(c)}}}}}
\put(2865,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^j_1$}}}}}
\put(3540,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^j_2$}}}}}
\put(4215,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^j_3$}}}}}
\put(3555,39){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}(b)}}}}}
\put(990,39){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}(a)}}}}}
\put(2527,2469){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}. . . }}}}}
\put(4860,2072){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\falsity_r$}}}}}
\put(3555,3999){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg p_i^{e,j}$}}}}}
\put(6255,4149){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p_i^{j+1}$}}}}}
\put(5527,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^{e,j}_i$}}}}}
\put(6202,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg p^{e,j}_i$}}}}}
\put(6877,399){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$p^{j}_i$}}}}}
\put(3510,2289){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\wedge$}}}}}
\put(4005,1389){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg$}}}}}
\put(3510,3189){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\vee$}}}}}
\put(5467,1629){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\wedge$}}}}}
\put(6142,1622){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\vee$}}}}}
\put(6547,2297){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\neg$}}}}}
\put(6720,2964){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\wedge$}}}}}
\put(5812,2934){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\wedge$}}}}}
\put(6247,3654){\makebox(0,0)[b]{\smash{{{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$\vee$}}}}}
\end{picture}
}

\caption{Circuit structure for precondition testing (a), conditional effects
  (b), and the computation of effects (c) for \PLlc{} operators}
\label{F:circuits:action}
\end{center}
\end{figure}

Without loss of generality (using a polynomial transformation), we assume that
all conditional effects have the form $\litset \effimpl \litvar$. Whether the
effect $\litvar$ is activated on level $j$ is computed by a circuit as
displayed in Figure~\ref{F:circuits:action}~(b), which shows the circuit for  
$\{\atomvar_1, \neg \atomvar_3\} \effimpl \neg\atomvar_i$.

Finally, all activated effects are combined by the circuit shown in
Figure~\ref{F:circuits:action}~(c). For all atoms $\atomvar_i$, we check
whether both $\atomvar_i$ and $\neg \atomvar_i$ have been activated, which
would set $\falsity_r$ true. This is again one of the inputs of the $\vee$-gate
in Figure~\ref{F:circuits:goal}. If neither $\atomvar_i$ nor $\neg \atomvar_i$
have been activated, the value of $\atomvar_i$ on level $j+1$ is determined by
the value of $\atomvar_i$ on level $j$. Otherwise the value of $\atomvar_i$ on
level $j+1$ is determined by the value of  $\atomvar_i^{e,j}$, i.e.,
the activation value of the positive effect $\atomvar_i$ on level $j$.

The depths of the circuits in Figure~\ref{F:circuits:action}~(b) and (c) 
  dominate the depth of the circuit necessary to represent one plan step
  leading to the conclusion that a plan step can be represented using a
  circuit of depth 7. Adding the depth of the goal testing circuit, the claim
  follows. 
\end{proof}


The lemma implies that \PLlc{} $c$-step plan acceptance is indeed less
powerful than \PLuc{} 1-step plan acceptance, which means that a compilation
scheme from \PLuc{} to \PLlc{} preserving plan size linearly is impossible.


\begin{theorem}
\label{T:puc:to:pl}
  \PLuc{} $\not\compilable^c$ $\planfx$, for
  all members $\planfx$ of the \PLl-class.
\end{theorem}

\begin{proof}
  We show that \PLuc{} $\not\compilable^c$ \PLlc{}, from which by
  Theorem~\ref{T:conditional:no:formulae} and
  Proposition~\ref{P:transitivity:reflexivity} the claim follows.
  
  Assume for contradiction that \PLuc{} $\compilable^c$ \PLlc{}. Let $\famdom
  = (\domainstructure_0, \domainstructure_1, \ldots)$ be a uniform family of
  \PLuc{} domain structures and $\famdom' = (\domainstructure_0',
  \domainstructure_1', \ldots)$ be the \PLlc{} domain structures generated by
  a compilation scheme $\compfun$ that preserves plan size linearly. By
  Lemma~\ref{L:plan:circuit} we know that for each \PLlc{} domain structure
  $\domainstructure'_n = \langle \atomalph'_n, \opset'_n\rangle$ and given
  goal $\goal'$ we can generate a polynomially sized, unbounded fan-in circuit
  with depth $7c+2$ that tests whether a particular $c$-step plan achieves the
  goal. In order to decide $c$-step plan existence, we must test
  $O(\card{\opset'_n}^c)$ different plans, which is polynomial in the size of
  $\domainstructure_n$ because $\compfun$ is a compilation scheme. For each
  plan, we can generate one test circuit, and by adding another $\vee$-gate we
  can decide $c$-step plan existence using a circuit with depth $7c+3$ and
  size polynomial in the size of $\domainstructure_n$.  Further, since the
  state-translation functions are modular, the results of $\transifun$ for
  fixed $\atomalph$ can be computed using an additional level of gates.  Since
  by Proposition~\ref{P:nc} all languages in \NCone{} are accepted by uniform
  families of \PLuc{} domain structures using one-step plan acceptance, our
  assumption \PLuc{} $\compilable^c$ \PLlc{} implies that we can accept all
  language in \NCone{} by (possibly non-uniform) \ACzero{} circuits, which is
  impossible by the result of Furst and colleagues
  \shortcite{furst:et:al:mst-84}.
\end{proof}


Using the Propositions~\ref{P:transitivity:reflexivity}
and~\ref{P:upward:compilability} again, we can generalize the above theorem as
follows. 

\begin{corollary}
\label{C:pu:to:pl:plu}
\PLc{} and \PLuc{}  cannot be compiled to \classPLl{} or \classPLlu{} preserving plan size
linearly. 
\end{corollary}

\section{Compilability Preserving Plan Size Polynomially}
\label{S:polynomial:compilability}

As has been shown in the previous section, only the compilation schemes
induced by Propositions~\ref{P:transitivity:reflexivity}
and~\ref{P:upward:compilability} and the ones identified in
Section~\ref{S:linear:compilability} allow for compilation schemes preserving
plan size exactly. For all other pairs of formalisms we were able to rule out such
compilation schemes---even if we allow linear growth of the resulting plans.
Nevertheless, there might still be a chance for compilation schemes preserving
plan size polynomially. Having shown that \PL{} and \PLu{} cannot be compiled
to the other formalisms even if the plan can grow polynomially, we may still
be able to find compilation schemes preserving plan size polynomially for the
\PL/\PLu{} pair and for the remaining formalisms.

A preview of the results of this section is given in
Figure~\ref{F:partial:order:polynomial:compilation}. 
\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{0.00083333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(4448,4280)(0,-10)
\texture{0 0 0 888888 88000000 0 0 80808 
        8000000 0 0 888888 88000000 0 0 80808 
        8000000 0 0 888888 88000000 0 0 80808 
        8000000 0 0 888888 88000000 0 0 80808 }
\put(2078,1769){\shade\ellipse{4140}{3524}}
\put(2078,1769){\ellipse{4140}{3524}}
\shade\path(4226,3594)(4243,3580)(4259,3565)
        (4276,3549)(4292,3533)(4308,3515)
        (4323,3497)(4339,3478)(4353,3458)
        (4367,3438)(4380,3418)(4392,3398)
        (4402,3377)(4412,3357)(4419,3338)
        (4426,3319)(4431,3301)(4434,3284)
        (4435,3267)(4436,3252)(4434,3236)
        (4432,3226)(4429,3216)(4425,3206)
        (4420,3196)(4414,3187)(4407,3178)
        (4398,3170)(4388,3162)(4376,3154)
        (4363,3147)(4347,3140)(4331,3135)
        (4312,3130)(4292,3125)(4270,3122)
        (4247,3119)(4222,3118)(4195,3117)
        (4166,3117)(4137,3118)(4105,3121)
        (4073,3124)(4039,3128)(4003,3133)
        (3966,3139)(3928,3147)(3887,3155)
        (3846,3164)(3815,3171)(3783,3179)
        (3751,3187)(3717,3196)(3682,3205)
        (3645,3215)(3608,3226)(3570,3237)
        (3530,3249)(3490,3261)(3448,3274)
        (3406,3288)(3362,3302)(3318,3316)
        (3274,3331)(3228,3347)(3182,3362)
        (3136,3378)(3090,3395)(3044,3411)
        (2998,3428)(2952,3445)(2906,3462)
        (2861,3480)(2816,3497)(2773,3514)
        (2729,3531)(2687,3548)(2646,3565)
        (2606,3582)(2567,3598)(2530,3615)
        (2493,3631)(2458,3647)(2424,3662)
        (2391,3678)(2360,3693)(2330,3708)
        (2301,3722)(2273,3736)(2235,3757)
        (2200,3777)(2166,3796)(2135,3816)
        (2105,3835)(2077,3855)(2051,3874)
        (2026,3893)(2004,3912)(1983,3930)
        (1964,3948)(1947,3966)(1932,3984)
        (1919,4001)(1908,4018)(1899,4034)
        (1891,4049)(1886,4064)(1882,4078)
        (1880,4091)(1879,4104)(1880,4116)
        (1882,4127)(1886,4137)(1890,4147)
        (1896,4156)(1903,4165)(1911,4173)
        (1923,4183)(1937,4193)(1953,4202)
        (1971,4210)(1990,4217)(2012,4224)
        (2035,4230)(2060,4235)(2086,4240)
        (2114,4243)(2142,4247)(2170,4249)
        (2199,4251)(2227,4252)(2255,4253)
        (2283,4253)(2309,4253)(2335,4253)
        (2361,4252)(2386,4251)(2408,4249)
        (2429,4248)(2451,4246)(2473,4244)
        (2496,4242)(2519,4240)(2542,4236)
        (2566,4233)(2591,4229)(2615,4225)
        (2641,4220)(2666,4214)(2692,4209)
        (2719,4202)(2745,4196)(2772,4189)
        (2798,4181)(2825,4174)(2852,4165)
        (2880,4157)(2908,4148)(2937,4138)
        (2960,4130)(2984,4122)(3009,4113)
        (3035,4104)(3061,4094)(3089,4084)
        (3117,4074)(3146,4063)(3176,4052)
        (3207,4040)(3238,4028)(3270,4016)
        (3302,4004)(3334,3991)(3366,3979)
        (3398,3966)(3430,3954)(3461,3942)
        (3492,3930)(3522,3918)(3551,3906)
        (3579,3895)(3607,3884)(3633,3874)
        (3659,3864)(3684,3854)(3708,3844)
        (3731,3835)(3760,3824)(3788,3813)
        (3815,3803)(3842,3792)(3869,3781)
        (3895,3771)(3921,3760)(3946,3750)
        (3971,3739)(3996,3729)(4019,3718)
        (4042,3707)(4065,3696)(4086,3685)
        (4106,3674)(4126,3663)(4144,3652)
        (4162,3641)(4179,3630)(4195,3618)
        (4211,3606)(4226,3594)
\path(4226,3594)(4243,3580)(4259,3565)
        (4276,3549)(4292,3533)(4308,3515)
        (4323,3497)(4339,3478)(4353,3458)
        (4367,3438)(4380,3418)(4392,3398)
        (4402,3377)(4412,3357)(4419,3338)
        (4426,3319)(4431,3301)(4434,3284)
        (4435,3267)(4436,3252)(4434,3236)
        (4432,3226)(4429,3216)(4425,3206)
        (4420,3196)(4414,3187)(4407,3178)
        (4398,3170)(4388,3162)(4376,3154)
        (4363,3147)(4347,3140)(4331,3135)
        (4312,3130)(4292,3125)(4270,3122)
        (4247,3119)(4222,3118)(4195,3117)
        (4166,3117)(4137,3118)(4105,3121)
        (4073,3124)(4039,3128)(4003,3133)
        (3966,3139)(3928,3147)(3887,3155)
        (3846,3164)(3815,3171)(3783,3179)
        (3751,3187)(3717,3196)(3682,3205)
        (3645,3215)(3608,3226)(3570,3237)
        (3530,3249)(3490,3261)(3448,3274)
        (3406,3288)(3362,3302)(3318,3316)
        (3274,3331)(3228,3347)(3182,3362)
        (3136,3378)(3090,3395)(3044,3411)
        (2998,3428)(2952,3445)(2906,3462)
        (2861,3480)(2816,3497)(2773,3514)
        (2729,3531)(2687,3548)(2646,3565)
        (2606,3582)(2567,3598)(2530,3615)
        (2493,3631)(2458,3647)(2424,3662)
        (2391,3678)(2360,3693)(2330,3708)
        (2301,3722)(2273,3736)(2235,3757)
        (2200,3777)(2166,3796)(2135,3816)
        (2105,3835)(2077,3855)(2051,3874)
        (2026,3893)(2004,3912)(1983,3930)
        (1964,3948)(1947,3966)(1932,3984)
        (1919,4001)(1908,4018)(1899,4034)
        (1891,4049)(1886,4064)(1882,4078)
        (1880,4091)(1879,4104)(1880,4116)
        (1882,4127)(1886,4137)(1890,4147)
        (1896,4156)(1903,4165)(1911,4173)
        (1923,4183)(1937,4193)(1953,4202)
        (1971,4210)(1990,4217)(2012,4224)
        (2035,4230)(2060,4235)(2086,4240)
        (2114,4243)(2142,4247)(2170,4249)
        (2199,4251)(2227,4252)(2255,4253)
        (2283,4253)(2309,4253)(2335,4253)
        (2361,4252)(2386,4251)(2408,4249)
        (2429,4248)(2451,4246)(2473,4244)
        (2496,4242)(2519,4240)(2542,4236)
        (2566,4233)(2591,4229)(2615,4225)
        (2641,4220)(2666,4214)(2692,4209)
        (2719,4202)(2745,4196)(2772,4189)
        (2798,4181)(2825,4174)(2852,4165)
        (2880,4157)(2908,4148)(2937,4138)
        (2960,4130)(2984,4122)(3009,4113)
        (3035,4104)(3061,4094)(3089,4084)
        (3117,4074)(3146,4063)(3176,4052)
        (3207,4040)(3238,4028)(3270,4016)
        (3302,4004)(3334,3991)(3366,3979)
        (3398,3966)(3430,3954)(3461,3942)
        (3492,3930)(3522,3918)(3551,3906)
        (3579,3895)(3607,3884)(3633,3874)
        (3659,3864)(3684,3854)(3708,3844)
        (3731,3835)(3760,3824)(3788,3813)
        (3815,3803)(3842,3792)(3869,3781)
        (3895,3771)(3921,3760)(3946,3750)
        (3971,3739)(3996,3729)(4019,3718)
        (4042,3707)(4065,3696)(4086,3685)
        (4106,3674)(4126,3663)(4144,3652)
        (4162,3641)(4179,3630)(4195,3618)
        (4211,3606)(4226,3594)
\path(2753,419)(2003,1169)
\blacken\path(2109.066,1105.360)(2003.000,1169.000)(2066.640,1062.934)(2109.066,1105.360)
\path(2753,419)(3503,1169)
\blacken\path(3439.360,1062.934)(3503.000,1169.000)(3396.934,1105.360)(3439.360,1062.934)
\path(2753,419)(2753,1169)
\blacken\path(2783.000,1049.000)(2753.000,1169.000)(2723.000,1049.000)(2783.000,1049.000)
\path(1853,1394)(653,2294)
\blacken\path(767.000,2246.000)(653.000,2294.000)(731.000,2198.000)(767.000,2246.000)
\path(2753,1394)(803,2369)
\blacken\path(923.748,2342.167)(803.000,2369.000)(896.915,2288.502)(923.748,2342.167)
\path(1853,1394)(1853,2294)
\blacken\path(1883.000,2174.000)(1853.000,2294.000)(1823.000,2174.000)(1883.000,2174.000)
\path(3653,1394)(1853,2294)
\blacken\path(1973.748,2267.167)(1853.000,2294.000)(1946.915,2213.502)(1973.748,2267.167)
\path(3653,1394)(2753,2294)
\blacken\path(2859.066,2230.360)(2753.000,2294.000)(2816.640,2187.934)(2859.066,2230.360)
\path(2753,1394)(2753,2294)
\blacken\path(2783.000,2174.000)(2753.000,2294.000)(2723.000,2174.000)(2783.000,2174.000)
\path(3653,1394)(3653,2294)
\blacken\path(3683.000,2174.000)(3653.000,2294.000)(3623.000,2174.000)(3683.000,2174.000)
\path(653,2594)(1553,3194)
\blacken\path(1469.795,3102.474)(1553.000,3194.000)(1436.513,3152.397)(1469.795,3102.474)
\path(1853,2594)(1853,3194)
\blacken\path(1883.000,3074.000)(1853.000,3194.000)(1823.000,3074.000)(1883.000,3074.000)
\path(1853,2594)(2753,3194)
\blacken\path(2669.795,3102.474)(2753.000,3194.000)(2636.513,3152.397)(2669.795,3102.474)
\path(3653,2594)(2753,3194)
\blacken\path(2869.487,3152.397)(2753.000,3194.000)(2836.205,3102.474)(2869.487,3152.397)
\path(3653,2594)(3653,3194)
\blacken\path(3683.000,3074.000)(3653.000,3194.000)(3623.000,3074.000)(3683.000,3074.000)
\path(2753,2594)(3653,3194)
\blacken\path(3569.795,3102.474)(3653.000,3194.000)(3536.513,3152.397)(3569.795,3102.474)
\path(1853,3494)(2753,3944)
\blacken\path(2659.085,3863.502)(2753.000,3944.000)(2632.252,3917.167)(2659.085,3863.502)
\path(2753,3494)(2753,3944)
\blacken\path(2783.000,3824.000)(2753.000,3944.000)(2723.000,3824.000)(2783.000,3824.000)
\path(3653,3494)(2753,3944)
\blacken\path(2873.748,3917.167)(2753.000,3944.000)(2846.915,3863.502)(2873.748,3917.167)
\path(2753,2594)(1853,3194)
\blacken\path(1969.487,3152.397)(1853.000,3194.000)(1936.205,3102.474)(1969.487,3152.397)
\dashline{60.000}(2753,3869)(3585,3449)
\blacken\path(3464.356,3476.296)(3585.000,3449.000)(3491.395,3529.858)(3464.356,3476.296)
\dashline{60.000}(2744,3103)(3570,2572)
\blacken\path(3452.836,2611.656)(3570.000,2572.000)(3485.281,2662.126)(3452.836,2611.656)
\dashline{60.000}(1950,2159)(3503,1394)
\blacken\path(3382.095,1420.115)(3503.000,1394.000)(3408.609,1473.939)(3382.095,1420.115)
\dashline{60.000}(3728,2294)(3728,1394)
\blacken\path(3698.000,1514.000)(3728.000,1394.000)(3758.000,1514.000)(3698.000,1514.000)
\put(2753,4019){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PL}}}}}
\put(2753,3269){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLc}}}}}
\put(1853,2369){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLlc}}}}}
\put(2753,2369){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLlu}}}}}
\put(3653,2369){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLuc}}}}}
\put(578,2369){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLa}}}}}
\put(1853,1244){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLac}}}}}
\put(2753,1244){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLau}}}}}
\put(3653,1244){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLluc}}}}}
\put(1853,3269){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLl}}}}}
\put(3653,3269){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLu}}}}}
\put(2753,269){\makebox(0,0)[b]{\smash{{{\SetFigFont{10}{12.0}{\familydefault}{\mddefault}{\updefault}\PLauc}}}}}
\end{picture}
}

\caption{Equivalence classes of planning formalisms created by 
polynomial-time compilation schemes preserving plan size polynomially. Compilation
schemes constructed in this section are indicated by dashed lines}
\label{F:partial:order:polynomial:compilation}
\end{center}
\end{figure}
As it can be seen, we are able to establish compilation schemes preserving
plan size polynomially for all pairs of formalisms for which we have not
proved the impossibility of such compilation schemes.

\subsection{Compiling Conditional Effects Away for Partial State
  Specifications} 

The first compilation scheme we will develop is one from \PL{} to \PLu{}.  As
before, we assume that the conditional effects have only singleton effect
sets. Further, since we can use arbitrary boolean formulae in the effect conditions in \PL, we
assume that there is only one rule for each effect literal.  Using a simple
polynomial transformation, arbitrary sets of operators can be brought into
this form.  This simplifies checking the condition
$\Eff(\statespec,\post(\op)) = \Pot(\statespec,\post(\op))$ considerably,
because now only one rule can activate a particular literal.

In order to simulate the parallel behavior of conditional effects, we have to
break them up into individual operators that are executed sequentially.  This
means that for each conditional effect of an operator we introduce two new
operators. One simulates the successful application of the rule, the other one
simulates the ``blocking'' situation of the rule.  At least one of these
operators must be executed for each conditional effect in the original
operator.  This is something we can force by additional literals that are
added to control the execution of operators. All in all this leads to a
sequence of operators that has length bounded by the number of conditional
effects in the original operator.

If we want to simulate the parallel behavior by a sequence of unconditional
operators, the effects of the unconditional operators should not directly
influence the state description, but the effect should be deferred until all
operators corresponding to the set of conditional effects have been executed.
For this reason, we will use a sequence of ``copying operators'' which copy
the activated effects to the state description after all ``conditional
operators'' have been executed.  These ``copying operators'' can also be used
to check that the set of activated effects is consistent.

\begin{theorem}
\label{T:compiling:conditional:effects:away:partial:states}
\PL{} can be compiled to \PLu{} in polynomial time preserving plan size
polynomially. 
\end{theorem}

\begin{proof}
  Assume that $\domainstructure = \domainstructuretuple$ is the \PL{} source
  domain structure and assume further, without loss of generality (using a
  polynomial transformation), that all operators have the form
  \[ \op_i =  \langle \pre(\op_i), \{ \formula_{i,1} \effimpl \litvar_{i,1},
  \ldots, \formula_{i,m_i} \effimpl \litvar_{i,m_i}\}\rangle,\] with
  $\formula_{i,j} \in \loglang$, $\litvar_{i,j} \in \litalph$, and
  $\litvar_{i,j} \neq \litvar_{i,k}$ for $i \neq k$.
  
  Let $\atomalph_+$ and $\atomalph_-$ be disjoint copies of $\atomalph$, which
  are used to record the active effects of conditional effects, and let
  $\atomalph_\#$ be another disjoint copy, which is used to record that an
  active effect has not been copied yet.  Further, let $\atomalph_{\opset} =
  \{ \atomvar_{\op} \: | \: \op \in \opset\}$ be a new set of atoms
  corresponding one-to-one to the operators in $\opset$ and let $\unknownset$
  be a set of symbols corresponding one-to-one to all conditional effects in
  $\opset$, i.e.,
  \[ \unknownset = \{ \atomvarx_{i,j} | (\formula_{i,j} \effimpl
  \litvar_{i,j}) \in \post(\op_i), \op_i \in \opset\}.
  \]
  Finally, let $\copying$ be a fresh atom not appearing in $\atomalph \cup
  \atomalph_+ \cup \atomalph_- \cup \atomalph_\# \cup \atomalph_{\opset}$
  that signals that copying the active effects to the state specification is
  in progress.  The set of symbols $\atomalph'$ for the compiled domain
  structure is then
  \[ \atomalph' = \atomalph \cup \atomalph_+ \cup \atomalph_- \cup \atomalph_\#
  \cup \atomalph_{\opset} \cup \unknownset \cup \{\copying\}.\]
  
  For each operator $\op_i \in \opset$, the compilation scheme introduces a
  number of new operators.  The first operator we introduce is one which
  checks whether the conditional effects of the previous operators have all
  been executed, no copying is in progress and the precondition is satisfied.
  If this is the case, the execution of the conditional effects for this
  operator is started:
  \[ \op_i^{\pre} = \langle \pre(\op_i) \cup \neg \atomalph_{\opset} \cup \{\neg
  \copying\}, \: \{\atomvar_{\op_i}\} \cup \neg \atomalph_+ \cup \neg \atomalph_-
  \cup \neg \unknownset \cup \neg \atomalph_\#\rangle.
  \] 
  This operator enables all the ``conditional effect operators.'' For the
  activated effects, we introduce the following operators:
  \[ \op_i^{\effimpl,i,j} = \langle \{\atomvar_{\op_i} \wedge 
  \formula_{i,j}\},\: \{ \atomvarx_{i,j} \} \cup \{ \atomvar_+, \atomvar_\# \:| \:\atomvar =
  \litvar_{i,j} \} \cup \{ \atomvar_-, \atomvar_\#  \: | \: \neg \atomvar =
  \litvar_{i,j}\} \rangle.\] In words, if the effect condition is entailed,
  then the activated positive or negative effect as well as the fact that the
  rule has been tried is recorded.
  
  Since there is at most one effect literal for each conditional effect, a
  conditional effect is ``blocked'' if the negation of the effect condition is
  entailed by the state specification. For all ``blocked conditional effects''
  we introduce the following operators:
  \[ \op_i^{\neg,i,j} =  \langle \{\atomvar_{\op_i} \wedge 
  \neg\formula_{i,j}\},
  \: \{ \atomvarx_{i,j} \}\rangle.\]

  
  In order to check that all conditional effects have been tried (activating
  the corresponding effect or not activating it because the conditional effect
  is blocked), the following operator is used:
  \[ \op_i^e = \langle \{\atomvar_{\op_i}\} \cup \{\var_{i,j} \in
  \unknownset \:|\: (\formula_{i,j} \effimpl \litvar_{i,j}) \in \post(\op_i)
  \}, \: \{\copying\} \cup \{\neg \atomvar_{\op_i}\} 
  \rangle.
  \] 
  This operator enables copying of the activated effects to the
  state specification, which is achieved with the following set of operators
  for each atom $\atomvar \in \atomalph$:
  \begin{eqnarray*}
    \op^{\atomvar}_+ & = & \langle \{\copying, \atomvar_+,  \neg \atomvar_-, \atomvar_\#\},
    \{\atomvar, \neg \atomvar_\#\} \rangle, \\
    \op^{\atomvar}_- & = & \langle \{\copying, \neg \atomvar_+, \atomvar_-, \atomvar_\#\},
    \{\neg\atomvar, \neg \atomvar_\#\} \rangle, \\
    \op^{\atomvar}_{\falsity} & = & \langle \{\copying, \atomvar_+, \atomvar_-,\atomvar_\#\},
    \falsity \rangle.
  \end{eqnarray*}
  Finally, we need an operator that checks that all possible effects have been
  copied. This operator also starts the ``execution cycle'' again by enabling
  the execution of another ``precondition operator:''
  \[ \op^c = \langle \{\copying\} \cup \neg \atomalph_\#, \: \{\neg \copying\}
  \rangle.
  \]
  Using these definitions, we can now specify the set of compiled operators:
  \[ \opset' =
  \!\!\!\begin{array}[t]{l}
    \{ \op_i^{\pre}, \op_i^e \: | \: \op_i \in \opset \} \: \cup \\
    \{ \op^{\effimpl,i,j} \: | \: \op_i \in \opset, (\formula_{i,j} \effimpl
    \litvar_{i,j}) \in \post(\op_i)\} \: \cup \\
    \{ \op^{\neg,i,j} \: | \: \op_i \in \opset, (\formula_{i,j} \effimpl
    \litvar_{i,j}) \in \post(\op_i) \}
    \: \cup \\
    \{ \op^{\atomvar}_+, \op^{\atomvar}_-, 
    \op^{\atomvar}_{\falsity} \: | \: \atomvar \in \atomalph \} \: \cup \\
    \{ \op^c\}.
  \end{array}
  \]
  Based on that, we specify a compilation scheme $\compfun = \compfuntuple$ as
  follows:
  \begin{eqnarray*}
    \compdsfun(\domainstructure) & = & \langle \atomalph',
    \opset' \rangle \\
    \compifun(\domainstructure) & = & \neg \atomalph_+ \cup \neg
    \atomalph_- \cup \neg \atomalph_\# \cup \neg \atomalph_{\opset} \cup \neg
    \unknownset \cup \{ \neg \copying \}, \\
    \compgfun(\domainstructure) & = & \neg \atomalph_{\opset}
    \cup \{\neg \copying\}, \\
    \transifun(\atomalph,\initial) & = & \initial, \\
    \transgfun(\atomalph,\goal) & = & \goal.
  \end{eqnarray*}
  The scheme $\compfun$ obviously satisfies conditions (\ref{I:translation})
  and (\ref{I:compilation:size}) for compilation schemes and all the
  functions can be computed in polynomial time. Further,
  $\comp(\planinstance)$ is a \PLu-instance if
  $\planinstance$ is a \PL-instance.
  
  Let now $\statespec \in \litalph$ be a legal \PL{} state specification and
  let $\statespec' = \res(\statespec,\op_i)$ for some operator $\op_i \in
  \opset$. From the above discussion, it is clear that if $\statespec'
  \not\models \falsity$, then there exists a sequence $\plan'$ of operators
  from $\opset'$ consisting of $\op_i^{\pre}$, followed by operators of the
  form $\op_i^{\effimpl,i,j}$ and $\op_i^{\neg,i,j}$ followed by the operator
  $\op^e_i$, followed in turn by operators $\op^p_x$, followed finally by the
  operator $\op^c$, such that
  \[ \statespec' = \Result(\statespec \cup \compifun(\domainstructure), \plan') \cap \litalph.\] Conversely, if $\statespec' \models
  \falsity$, then there does not exist any plan that transforms
  \[\res(\statespec \cup \compifun(\domainstructure),
  \op_i^{\pre})\] into a legal state specification that contains $\neg
  \copying$ and $\neg \atomvar_{\op_i}$.
  
  Using induction on the plan length, it follows from the arguments
  above that there exists a plan $\plan$ for $\planinstance$ iff there exists
  a plan $\plan'$ for $\comp(\planinstance)$ and for every such plan we have
  $\size{\plan'} \leq \size{\plan} \times (3+2m)$, with $m$
  being the maximum number of conditional effects in operators of $\opset$.
  Hence $\compfun$ is a polynomial-time compilation scheme preserving plan
  size polynomially.
\end{proof}

An immediate consequence of this theorem is that \PL{} and \PLu{} form an
equivalence class with respect to compilability preserving plan size
polynomially. 

\begin{corollary}
\label{C:poly:comp:p:pu}
\PL{} and \PLu{} are polynomial-time compilable to each other preserving plan
size polynomially.
\end{corollary}

Further, we know from Corollary~\ref{C:ppu:separation} that this class
cannot become larger. 

As in the case of compiling \PLl{} to \PLlc{}, however, the result
depends on the semantics chosen for executing conditional effects over
partial state specifications.  If we use the alternative semantics
where the resulting state specification is legal when the application
of all state-transformation functions leads to a theory that can be
represented as a set of literals, it seems likely that there exists
another scheme that preserves plan size polynomially. However, if we
use the alternative semantics that deletes all the literals in $\neg
(\Pot(\statespec,\post(\op)) - \Eff(\statespec,\post(\op))$ if
$\Pot(\statespec,\post(\op)$ is consistent, then it appears to be very
unlikely that we are able to identify a compilation scheme that
preserves plan size polynomially.

\subsection{Compiling Conditional Effects Away for Complete State
  Specifications}

The next compilation scheme compiles \PLc{} to \PLuc{} and \PLlc{} to \PLluc.
Since we deal with complete state specification, we do not have to take care
of the condition $\Eff(\statespec,\post(\op)) = \Pot(\statespec,\post(\op))$,
which is always true for complete states. This makes the compilation scheme 
somewhat simpler. Since \PLluc{} does not allow for general boolean formulae, the
scheme becomes a little bit more difficult. In general, however,
the compilation scheme we will specify is very similar to the one given in the
proof of Theorem~\ref{T:compiling:conditional:effects:away:partial:states}.

\begin{theorem}
\label{T:compiling:conditional:effects:away:complete:states}
\PLc{} can be compiled to \PLuc{} and \PLlc{} can be compiled to \PLluc{}
in polynomial time preserving plan size
polynomially. 
\end{theorem}

\begin{proof}
  As in the proof of
  Theorem~\ref{T:compiling:conditional:effects:away:partial:states}, we assume
  that $\domainstructure = \domainstructuretuple$ is the (\PLc{} or \PLlc)
  source domain structure. Further, we assume that all operators have the form
  \[ \op_i =  \langle \pre(\op_i), \{ \formulaset_{i,1} \effimpl \litvar_{i,1},
  \ldots, \formulaset_{i,m_i} \effimpl \litvar_{i,m_i}\}\rangle,\] with
  $\litvar_{i,j} \in \litalph$ and $\formulaset_{i,j} \subseteq \loglang$ if
  $\domainstructure$ is a \PLc{} structure or $\formulaset_{i,j} \subseteq
  \litalph$ if $\domainstructure$ is a \PLlc{} structure. This means that we do not
  assume the effects to be unique for each conditional effect.

  In addition, we assume the same
  set symbols for the compiled domain structure as in the proof of
  Theorem~\ref{T:compiling:conditional:effects:away:partial:states}:
  \[ \atomalph' = \atomalph \cup \atomalph_+ \cup \atomalph_- 
  \cup \atomalph_\# \cup \atomalph_{\opset} \cup \unknownset \cup
  \{\copying\}.
  \]
  For each operator $\op_i \in \opset$, we introduce the operators
  $\op_i^{\pre}$, $\op_i^e$, $\op^{\atomvar}_+$, $\op^{\atomvar}_-$,
  $\op^{\atomvar}_{\falsity}$, and $\op^c$ as in the proof of
  Theorem~\ref{T:compiling:conditional:effects:away:partial:states}. In
  addition, the following operators are needed:
  \begin{eqnarray*}
    \op_i^{\effimpl,i,j} & = & \langle \{\atomvar_{\op_i}\} \cup
    \formulaset_{i,j},\: \{ \atomvarx_{i,j} \} \cup \{ \atomvar_+, \atomvar_\# \:| \:
    \atomvar =
    \litvar_{i,j} \} \cup \{ \atomvar_-, \atomvar_\# \: | \: \neg \atomvar =
    \litvar_{i,j}\} \rangle, \\
    \op_i^{\neg,i,j,m} & = &   \langle \{\atomvar_{\op_i}\} \cup \{ 
    \neg\formula_{i,j,m} \: | \: \formula_{i,j,m} \in \formulaset_{i,j}\} ,
    \: \{ \atomvarx_{i,j} \}\rangle.
  \end{eqnarray*}
  The compiled set of operators $\opset'$ contains all of the above operators
  and the compilation scheme is identical to the scheme presented in the proof
  of Theorem~\ref{T:compiling:conditional:effects:away:partial:states}.  This
  means that the only significant difference to the compilation scheme
  presented in the proof of
  Theorem~\ref{T:compiling:conditional:effects:away:partial:states} is the
  operator scheme $\op_i^{\neg,i,j,m}$ which tests for each rule whether it
  contains an effect condition that blocks the rule. Since we have complete
  state specifications, every conditional effect is either activated or
  blocked, and the $\atomvarx_{i,j}$'s are used to record that the execution of
  each conditional effect has been tried.

  Using now similar arguments as in the proof of
  Theorem~\ref{T:compiling:conditional:effects:away:partial:states}, it
  follows that this compilation scheme is indeed a scheme that leads to the
  claim made in the theorem.
\end{proof}

It follows that \PLc{} and \PLuc{} are equivalent with respect to
$\compilable^p_p$ and all formalisms in \classPLl{} and \classPLlu{} are
equivalent with respect to $\compilable^p_p$. These two sets could be merged
into one equivalence class, provided we are able to prove that, e.g., \PLuc{}
can be compiled to \PLluc.

\subsection{Compiling Boolean Formulae Away}

In Section~\ref{S:logical:formulae:cannot:compiled} we showed that it is
impossible to compile boolean formulae to conditional effects if plans are
only allowed to grow linearly. However, we also sketched already the idea of a
compilation scheme that preserves plan size polynomially. Here we will now
show that we can compile boolean formulae to \PLluc{}, which is expressively
equivalent to  basic \strips, i.e., we can
compile boolean formulae away completely.

\begin{theorem}
\PLuc{} is polynomial-time compilable to \PLluc{} preserving plan size
polynomially.
\end{theorem}

\begin{proof}
  Assume that $\domainstructure = \domainstructuretuple$ is a \PLuc{} domain
  structure. Further assume without loss of generality that all operators
  $\op_i \in \opset$ are of the form $\op_i=\langle \formula_i,
  \litset_i\rangle$, with $\litset_i \subseteq
  \litalph$ and $\formula_i \in \loglang$ (i.e., we have just one formula as
  the precondition instead of a set of formulae). 
  
  Let $\atomalph_{\Subformula}$ and
  $\atomalph'_{\Subformula}$ be two new sets of atoms corresponding one-to-one
  to all sub-formulae occurring in  preconditions of operators in
  $\opset$. These new atoms are denoted by $\atomvarq_{\subformula}$ and
  $\atomvarq'_{\subformula}$ for the sub-formula $\subformula$. Atoms of the
  form $\atomvarq'_{\subformula}$ are used to record that the truth-value of
  the sub-formula $\subformula$ has been computed and the atoms of the form
  $\atomvarq_{\subformula}$ are used to store the computed truth-value.
  
  For each operator $\op_i = \langle \formula_i, \litset_i \rangle$, we will
  have in the target operator set the following operator:
  \[ \op'_i = \langle \{ \atomvarq_{\formula_i},  \atomvarq'_{\formula_i} \},
  \litset_i \cup \neg \atomalph'_{\Subformula} \rangle. \] 
  The set of all operators generated in this way is denoted by $\opset'$.
  
  Further, for each atom $\atomvar \in \atomalph$, we introduce the following
  two operators:
  \begin{eqnarray*}
    \op_p^+ & = & \langle \{ \atomvar \},\: \{\atomvarq'_{\atomvar},
    \atomvarq_{\atomvar} \}\rangle, \\
    \op_p^- & = & \langle \{ \neg \atomvar \},\: \{\atomvarq'_{\atomvar},
    \neg \atomvarq_{\atomvar}\} \rangle.
  \end{eqnarray*}
  The set of operators generated in this way is denoted by $\opset_{\atomalph}$.

  For each sub-formula occurring in preconditions of $\opset$ of the form
  $\subformula = \subformula_1 \wedge \subformula_2$ the following operators
  are introduced:
  \begin{eqnarray*}
    \op_{\subformula}^+ & = & \langle \{ \atomvarq'_{\subformula_1},
    \atomvarq'_{\subformula_2}, \atomvarq_{\subformula_1},
    \atomvarq_{\subformula_2} \}, \{ \atomvarq'_{\subformula},
    \atomvarq_{\subformula} \} \rangle, \\
    \op_{\subformula}^{-1} & = & \langle \{ \atomvarq'_{\subformula_1}, \neg
    \atomvarq_{\subformula_1} \}, \{ \atomvarq'_{\subformula}, \neg
    \atomvarq_{\subformula} \} \rangle, \\
    \op_{\subformula}^{-2} & = & \langle \{ \atomvarq'_{\subformula_2}, \neg
    \atomvarq_{\subformula_2} \}, \{ \atomvarq'_{\subformula}, \neg
    \atomvarq_{\subformula} \} \rangle.
  \end{eqnarray*}
  For sub-formulae $\subformula = \subformula_1 \vee \subformula_2$, the
  following operators are introduced:
  \begin{eqnarray*}
    \op_{\subformula}^{+1} & = & \langle \{ \atomvarq'_{\subformula_1},
    \atomvarq_{\subformula_1} \}, \{ \atomvarq'_{\subformula},
    \atomvarq_{\subformula} \} \rangle, \\
    \op_{\subformula}^{+2} & = & \langle \{ \atomvarq'_{\subformula_2},
    \atomvarq_{\subformula_2} \}, \{ \atomvarq'_{\subformula},
    \atomvarq_{\subformula} \} \rangle, \\
    \op_{\subformula}^- & = & \langle \{ \atomvarq'_{\subformula_1},
    \atomvarq'_{\subformula_2}, \neg \atomvarq_{\subformula_1},
    \neg \atomvarq_{\subformula_2} \}, \{ \atomvarq'_{\subformula},
    \neg \atomvarq_{\subformula} \} \rangle.
  \end{eqnarray*}
  Finally, for $\subformula = \neg \subformulaq$, we have the following
  operators:
  \begin{eqnarray*}
    \op_{\subformula}^{+} & = & \langle \{ \atomvarq'_{\subformulaq},
    \neg \atomvarq_{\subformulaq} \}, \{ \atomvarq'_{\subformula},
    \atomvarq_{\subformula} \} \rangle, \\
    \op_{\subformula}^{-} & = & \langle \{ \atomvarq'_{\subformulaq},
    \atomvarq_{\subformulaq} \}, \{ \atomvarq'_{\subformula},
    \neg \atomvarq_{\subformula} \} \rangle.
  \end{eqnarray*}
  The set of operators generated by sub-formulae is denoted by
  $\opset_{\Subformula}$.

Now we can specify the compilation scheme $\compfun$:
\begin{eqnarray*}
\compdsfun(\domainstructure) & = & \langle \atomalph \cup
\atomalph_{\Subformula} \cup \atomalph'_{\Subformula}, \: \opset' \cup
\opset_{\atomalph} \cup \opset_{\Subformula}\rangle, \\
\compifun(\domainstructure) & = & \neg
\atomalph'_{\Subformula}, \\
\compgfun(\domainstructure) & = & \neg
\atomalph'_{\Subformula}, \\
\transifun(\atomalph,\initial) & = & \initial, \\
\transgfun(\atomalph,\goal) & = & \goal.
\end{eqnarray*}

From the construction it is obvious that all the functions are polynomial-time
computable, that the state-translation functions are modular, that the induced
function $\comp$ is a reduction, and that for every plan $\plan$ for a source
planning instance $\planinstance$ there exists a plan $\plan'$ for
$\comp(\planinstance)$ such that $\size{\plan'} \leq \size{\plan} \times
(m+1)$, with $m$ being the maximum number of sub-formulae of
preconditions in $\opset$. From that, the claim follows.
\end{proof}

There might be the question whether compiling boolean formulae away could be done more
efficiently. Using the result that boolean expressions can be evaluated by
circuits with logarithmic depth, this should be indeed possible. However, we
are satisfied here with the result that there is a compilation scheme preserving plan
size polynomially at all. This result together with
Theorem~\ref{T:compiling:conditional:effects:away:complete:states} settles the question for
compilation schemes preserving plan size polynomially for all pairs of
formalisms.

\begin{corollary}
\label{C:poly:comp:pl:pc}
  All formalisms $\planfx$ with $\planfx \spec$ \PLl{} or $\planfx \spec$ \PLc{} are
  polynomial-time compilable to each other preserving plan size polynomially.
\end{corollary}

\subsection{Parallel Execution Models and the Feasibility of Compilation Schemes
  Preserving Plan Size Polynomially}

While compilation schemes that preserve plan size exactly or 
linearly seem to be of immediate use, a polynomial growth of the plan appears
to be of little practical interest. Considering the practical experience that
planning algorithms can roughly be characterized by their property of how many
steps they can plan without getting caught by the combinatorial explosion and
the fact that this number is significantly smaller than 100, polynomial
growth does not seem to make much sense.

If we take \graphplan{} \cite{blum:furst:ai-97} into consideration again---the
planning system that motivated our investigation in the first place---it turns
out that this system allows for the {\em parallel execution} of actions.
Although parallel execution might seem to add to the power of the planning
system considerably, it does not affect our results at all. If a sequential
plan can solve a planning instance with $n$ steps, a parallel plan will also
need at least $n$ actions.  Nevertheless, although the size of a plan
(measured in the number of operations) might be the same, the number of time
steps may be considerably smaller---which might allow for a more efficient
generation of the plan.  Having a look at the compilation scheme
that compiles conditional effects away, it seems to be the case that a large
number of generated actions could be executed in parallel---in particular
those actions that simulate the conditional effects.

However, the semantics of parallel execution in \graphplan{} is quite
restrictive. If one action adds or deletes an atom that a second action
adds or deletes or if one action deletes an atom that a second action
has in its precondition, then these two actions cannot be executed in
parallel in \graphplan. With this restriction, it seems to be impossible to
compile conditional effects away preserving the number of time steps in a
plan. However, a compilation scheme that preserves the number of time steps
linearly seems to be possible.  Instead of such a compilation scheme, the
approaches so far either used an exponential translation
\cite{gazen:knoblock:ecp-97} or modified the \graphplan-algorithm in order to
handle conditional effects
\cite{anderson:et:al:aips-98,koehler:et:al:ecp-97,kambhampati:et:al:ecp-97}.
These modifications involve changes in the semantics of parallel execution as
well as changes in the search procedure. While all these implementations are
compared with the straightforward translation Gazen and Knoblock
\shortcite{gazen:knoblock:ecp-97} used, it would also be interesting to
compare them with a compilation scheme based on the ideas spelled out in
Theorem~\ref{T:compiling:conditional:effects:away:complete:states} as the base
line.



\section{Summary and Discussion}
\label{S:conclusions}

Motivated by the recent approaches to extend the \graphplan{} algorithm
\cite{blum:furst:ai-97} to deal with {\em more expressive planning formalisms}
\cite{anderson:et:al:aips-98,gazen:knoblock:ecp-97,kambhampati:et:al:ecp-97,koehler:et:al:ecp-97},
we asked what the term {\em expressive power} could mean in this context.  One
reasonable intuition seems to be that the term {\em expressive power} refers
to how concisely domain structures and the corresponding plans can be
expressed. Based on this intuition and inspired by recent approaches in the
area of knowledge compilation
\cite{gogic:et:al:ijcai-95,cadoli:et:al:kr-96,cadoli:donini:aicom-97}, we
introduced the notion of {\em compilability} in order to measure the relative
expressiveness of planning formalisms. The basic idea is that a {\em
  compilation scheme} can only transform the domain structure, i.e., the
symbol set and the operators, while the initial state and the goal specification
are not transformed---modulo some small changes necessary for technical
reasons. Further, we distinguish compilation schemes according to whether the
plan in the target formalism has the same size (up to an additive constant), a
size bounded linearly by the size of the plan in the source formalism, or a
size bounded polynomially by the original planning instance and the original
plan.

Although the compilability framework appears to be a straightforward and
intuitive tool for measuring the expressiveness of planning formalisms, it is
possible to come up with alternative measures.  B\"ackstr\"om
\shortcite{backstrom:ai-95}, for instance, proposed to use {\em
  ESP-reductions}, which are polynomial many-one reductions on planning
problems that preserve the plan size exactly. However, requiring that the
transformation should be polynomial-time computable seems to be overly
restrictive.  In particular, if we want to prove that one formalism is {\em
  not} as expressive as another one, we had better proven that there exists no
compilation scheme regardless of how much computational resources the
compilation process may need. Furthermore, there appear to be severe technical
problems to using B\"ackstr\"om's \shortcite{backstrom:ai-95} framework for
proving negative results. On the other hand, all of the positive results
reported by B\"ackstr\"om are achievable in the compilation framework because
the transformations he used are in fact compilation schemes. Taking all this
together, it appears to be the case that the compilation framework is
superior from an intuitive and technical point of view. 

Another approach to judging the expressiveness of planning formalisms has been
proposed by Erol and colleagues
\shortcite{erol:et:al:aaai-94,erol:et:al:amai-96}. They measure the
expressiveness of planning formalisms according to the set of plans a planning
instance can have. While this approach contrasts {\em hierarchical task
  network} planning nicely with \strips-planning, it does not help us in
making distinctions between the formalisms in the \STRIPS-family. 

The compilability framework is mainly a theoretical tool to measure how
concisely domain structures and plans can be expressed. However, it also
appears to be a good measure of how difficult planning becomes when a new
language feature is added.  {\em Polynomial-time} compilation schemes that
preserve the plan size linearly indicate that it is easy to integrate the
feature that is compiled away. One can either use the compilation scheme as is
or mimic the compilation scheme by extending the planning algorithm. If only a
polynomial-time compilation scheme leading to a polynomial growth of the plan
is possible, then this is an indication that adding the new feature requires
most probably a significant extension of the planning algorithm.  If even a
compilation scheme preserving plan size polynomially can be ruled out, then
there is most probably a serious problem integrating the new feature.

Using this framework, we analyzed a large family of planning formalisms
ranging from basic \strips{} to formalisms with conditional effects,
boolean formulae, and incomplete state specifications. The most
surprising result of this analysis is that we are able to come up with a
complete classification. For each pair of formalisms, we were either able to
construct a {\em polynomial-time compilation scheme} with the required size
bound on the resulting plans or we could prove that compilation schemes are
impossible---even if the computational resources for the compilation process
are unbounded. In particular, we showed for the formalisms considered in this
paper:
\begin{itemize}
\item incomplete state specifications and literals in preconditions can be
  compiled to basic \strips{} preserving plan size exactly,
\item incomplete state specifications and literals in preconditions and effect
  conditions can be compiled away preserving plan size exactly, if we have already
  conditional effects,
\item and there are no other compilation schemes preserving plan size linearly
  except those implied by the specialization relationship and those described
  above.
\end{itemize}
If we allow for polynomial growth of the plans in the target formalism, then
all formalisms not containing incomplete state specifications and boolean formulae are
compilable to each other. Incomplete state specifications together with
boolean formulae, however, seem to add significantly to the
expressiveness of a planning formalism, since these cannot be compiled away
even when allowing for polynomial growth of the plan and unbounded resources
in the compilation process.

It should be noted, however, that some of these results hold only if we use the
semantics for conditional effects over partial state specifications as spelled
out in Section~\ref{S:P:formalism}. For other semantics, we may get slightly
different results concerning the compilability of conditional effects over
partial states.

One question one may ask is what happens if we consider formalisms
with boolean formulae that are syntactically restricted.  As
indicated at various places in the paper, restricted formulae, such as
CNF or DNF formulae, can sometimes be easily compiled away. However,
there are also cases when this is impossible. For example, it can be
shown that CNF formulae cannot be compiled to basic \strips{}
preserving plan size linearly \cite{nebel:ecp-99}, which confirms
B\"ackstr\"om's \shortcite{backstrom:ai-95} conjecture that
CNF-formulae in preconditions add to the expressive power of basic \strips.

Another question is how reasonable our restrictions on a compilation scheme
are. In particular, one may want to know whether {\em non-modular}
state-translation functions could lead to more powerful compilation schemes.
First of all, requiring that the state-translation functions are modular seems
to be quite weak considering the fact that a compilation scheme should only be
concerned with the domain structure and that the initial state and goal
specification should not be transformed at all. Secondly, considering the fact
that the state-translation functions do not depend on the operator set, more
complicated functions seem to be useless.  From a more technical point of
view, we need modularity in order to prove that conditional effects and
boolean formulae cannot be compiled away preserving plan size linearly.
For the conditional effects, modularity or a similar condition seems to be
crucial. For the case of boolean formulae, we could weaken the condition
to the point that we require only that state-translation functions are
computable by circuits of constant depth---or something similar.  In any case,
the additional freedom one gets from non-modular state-translation functions
does not seem to be of any help because these functions do not take the
operators into account. Nevertheless, it seems to be an interesting
theoretical problem to prove that more powerful state-translation functions do
not add to the power of compilation schemes.

Although the paper is mainly theoretical, it was inspired by the
recent approaches to extend the \graphplan{} algorithm to handle more
powerful planning formalisms containing conditional effects. So, what
are the answers we can give to open problems in the field of planning
algorithm design?  First of all, Gazen and Knoblock's
\shortcite{gazen:knoblock:ecp-97} approach to compiling conditional
effects away is optimal if we do not want to allow plan growth more
than by a constant factor.  Secondly, all of the other approaches
\cite{anderson:et:al:aips-98,kambhampati:et:al:ecp-97,koehler:et:al:ecp-97}
that modify the \graphplan{} algorithm are using a strategy similar to
a polynomial-time compilation scheme preserving plan size
polynomially. For this reason, these approaches should be compared to a
``pure compilation approach'' using the ideas from the compilation
scheme developed in the proof of
Theorem~\ref{T:compiling:conditional:effects:away:complete:states} as
the base line. Thirdly, allowing for unrestricted boolean formulae adds again
a level of expressivity because they cannot be compiled away with
linear growth of the plan size. In fact, approaches such as the one by
Anderson and colleagues  \shortcite{anderson:et:al:aips-98} simply
expand the formulae to DNF accepting an exponential blow-up. Again, we
cannot do better than that if plan size should be preserved linearly.
Fourthly, if we want to add partial state specifications on top of
general boolean formulae, this would amount to an increase of expressivity
that is much larger than adding conditional effects or general
formulae to basic \strips, because in this case there is no way to
compile this away even if we allow for polynomial plan growth. 

Finally, one may wonder how our results apply to planning approaches that are
based on translating (bounded) planning problems to propositional logic such
as \satplan{} \cite{kautz:selman:aaai-96} or \blackbox{}
\cite{kautz:selman:aips-ws-98}. Since the entire analysis of the relative
expressiveness of planning formalisms uses the assumption that we compile from
one planning formalism to another planning formalism, the results do not tell
us anything about the size of representations if we switch to another
formalism. In particular, it seems possible to find an encoding of (bounded)
planning problems with conditional operators in propositional logic which is
as concise as an encoding of unconditional operators. The only advice our
results give is that such a concise encoding will not be found by first
translating conditional actions to unconditional actions and then using the
``standard'' encoding for unconditional actions \cite{kautz:et:al:kr-96} to
generate boolean formulae. However, addressing the problem of determining the
conciseness of representation in this context appears to be an interesting and
relevant topic for future research.



\section*{Acknowledgments}
The research reported in this paper was started and partly carried out while
the author enjoyed being a visitor at the AI department of the University of
New South Wales. Many thanks go to Norman Foo, Maurice Pagnucco, and Abhaya
Nayak and the rest of the AI department for the discussions and cappuccinos.
I would also like to thank Birgitt Jenner and Jacobo Toran for some
clarifications concerning circuit complexity.

\section*{Appendix A: Symbol Index}
\addcontentsline{toc}{section}{Appendix A: Symbol Index}
\begin{tabbing}
XYZUVW \=
PageX \= \kill
Symbol \> Page \> Explanation \\
$\card{\cdot}$ \> \pageref{D:card} \> cardinality of a set \\
$\size{\cdot}$ \> \pageref{D:size} \> size of an instance \\
$\effimpl$ \> \pageref{D:effimpl} \> symbol  used in conditional
effects \\
$\spec$ \> \pageref{D:spec} \> syntactic specialization relation \\
$\compilable^x_y$ \> \pageref{D:compilable} \> compilability relation
with restriction $x$ and $y$ \\
$\falsity$ \> \pageref{D:falsity} \>
boolean constant denoting falsity, also denoting \\
\> \> the illegal
  state specification \\
$\truth$ \> \pageref{D:truth} \> boolean constant denoting truth \\
$\advice(\cdot)$ \> \pageref{D:advice} \> advice function \\
$\Eff(\cdot,\cdot)$ \> \pageref{D:Eff:state},
\pageref{D:Eff:state:specification} \> active effects of an operator
in a state or 
state specification \\
\ACzero \> \pageref{D:ACzero} \> complexity class \\
$\circuit$ \> \pageref{D:circuit} \> boolean circuit \\
$\famcircuits$ \> \pageref{D:famcircuits} \> family of boolean circuits \\
\coNP \> \pageref{D:coNP} \> complexity class  \\
\coNPpoly \> \pageref{D:coNPpoly} \> non-uniform \coNP \\
$\cwa_{\atomalph}(\cdot)$ \> \pageref{D:cwa} \> closing a set of literals
w.r.t. $\atomalph$ \\
$\plan$ \> \pageref{D:plan} \> plan, i.e., sequence of operators \\
$\Delta^p_i$ \> \pageref{D:Deltapi} \> complexity class in the
polynomial hierarchy \\
$\instance$ \> \pageref{D:instance} \> instance of a problem \\
$\initial$ \> \pageref{D:initial} \> initial state description \\
$\compfun$ \> \pageref{D:compfun} \> compilation scheme ($=\langle \compdsfun, \compifun,
\compgfun, \transifun, \transgfun \rangle$) \\
$\comp(\cdot)$ \> \pageref{D:comp} \> transformation induced by
compilation scheme \\
$\compdsfun, \compifun, \compgfun$ \> \pageref{D:compxfun} \>
components of a compilation scheme \\
$\goal$ \> \pageref{D:goal} \> goal of a planning task \\
$\formulaset$ \> \pageref{D:formulaset} \> set of boolean formulae
\\
$\subformulaq, \formula, \formulaq$ \> \pageref{D:formula} \>
boolean formulae \\
$\litvar$ \> \pageref{D:litvar} \> literal \\
$\litset,\litsetm$ \> \pageref{D:litset} \> sets of literals \\
$\loglang$ \> \pageref{D:loglang} \> all boolean formulae that use
atoms from $\atomalph$ \\
$\mod{\cdot}$ \> \pageref{D:mod} \> set of all models of a theory \\
\NCone \> \pageref{D:NCone} \> complexity class  \\
$\nl{\cdot}$ \> \pageref{D:nl} \> negative literals in a set of
  literals \\
\NP \> \pageref{D:NP} \> complexity class \\ 
\NPpoly \> \pageref{D:NPpoly} \> non-uniform \NP \\
$\op$ \> \pageref{D:op} \> operator ($=\langle\pre,\post\rangle$) \\
$\opset$ \> \pageref{D:opset} \> set of operators \\
$\seq{\opset}$ \> \pageref{D:seq:opset} \> set of finite sequences
of operators \\
$\atomvar,\atomvarq,\atomvaru,\atomvarv,\atomvarx$ \>
\pageref{D:atomvar} \> propositional atoms \\
$\Pot(\cdot,\cdot)$ \> \pageref{D:Pot} \> potentially active effects
of an operator \\ 
\> \> for a given state specification \\
\Poly \> \pageref{D:Poly} \> complexity class \\
\Ppoly \> \pageref{D:Ppoly} \> non-uniform \Poly \\
\PH \> \pageref{D:PH} \> the polynomial hierarchy \\
$\pl{\cdot}$ \> \pageref{D:pl} \> positive literals in a set of
  literals \\
\planex \> \pageref{D:planex} \> plan existence problem \\
$\post$ \> \pageref{D:post} \> postconditions of an operator \\
$\pre$ \> \pageref{D:pre} \> preconditions of an operator \\
\PSPACE \> \pageref{D:PSPACE} \> complexity class \\
$\planinstance$ \> \pageref{D:planinstance} \> planning instance
($=\planinstancetuple$) \\
$\Pi^p_i$ \> \pageref{D:Pipi} \> complexity class in the polynomial
hierarchy \\
$\res(\cdot,\cdot)$ \> \pageref{D:res} \> maps a state
specification and an operator to a new state \\
$\Result(\cdot,\cdot)$ \> \pageref{D:Result} \> extension of
$\res(\cdot,\cdot)$ to plans \\
$\state$ \> \pageref{D:state} \> state (or truth assignment) \\
$\statespec$ \> \pageref{D:statespec} \> state specification \\
\STRIPS \> \pageref{D:STRIPS} \> the \strips{} planning formalism \\
\PLluc \> \pageref{D:STRIPSx} \> \strips{} with literals in
preconditions \\
\PLuc \> \pageref{D:STRIPSx} \> \strips{} with boolean formulae in
preconditions \\
\PLau \> \pageref{D:STRIPSx} \> \strips{} with incomplete state
descriptions \\
\PLac \> \pageref{D:STRIPSx} \> \strips{} with conditional effects
\\
\STRIPS$_{\ldots}$ \> \pageref{D:STRIPSx} \> \strips{} with combinations
of the above extensions \\
\classPLl \>  \pageref{D:classPLl} \> equivalence
classes induced by $\compilable^1_p$ \\
\classPLlu \> \pageref{D:classPLl} \> equivalence
classes induced by $\compilable^1_p$ \\
$\alphabet(\cdot)$ \> \pageref{D:alphabet} \> all propositional
atoms used in a set of literals \\
${\allatoms}$ \> \pageref{D:allatoms} \> countably infinite set of
propositional atoms \\
$\atomalph$ \> \pageref{D:atomalph} \> finite subset of $\allatoms$ \\
$\litalph$ \> \pageref{D:litalph} \> set of literals overs
$\atomalph$ \\
$\Sigma^p_i$ \> \pageref{D:Sigmapi} \> complexity class in the
polynomial hierarchy \\
$\transifun, \transgfun$ \> \pageref{D:transxfun} \> state-translation functions in a
compilation scheme \\
$\univlits$ \> \pageref{D:univlits} \> universal literals \\
$\word$ \> \pageref{D:word} \> a word over $\{0,1\}^\star$ \\
\classX \> \pageref{D:classX} \> some complexity class \\
$\planfx$, $\planfy$ \> \pageref{D:planfx} \> some planning formalisms \\
$\domainstructure$ \> \pageref{D:domainstructure} \> domain
structure ($=\domainstructuretuple$) \\
$\famdom$ \> \pageref{D:famdom} \> family of domain structures 
\end{tabbing}


%\bibliography{abbreviations,biblio,crossref} 
%\bibliographystyle{theapa}

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Anderson, Smith, \BBA\ Weld}{Anderson
  et~al.}{1998}]{anderson:et:al:aips-98}
Anderson, C.~R., Smith, D.~E., \BBA\ Weld, D.~S. \BBOP1998\BBCP.
\newblock \BBOQ Conditional effects in {G}raphplan\BBCQ\
\newblock In {\Bem Proceedings of the 4th International Conference on
  Artificial Intelligence Planning Systems (AIPS-98)}, \BPGS\ 44--53. {AAAI}
  Press, Menlo Park.

\bibitem[\protect\BCAY{Baader}{Baader}{1990}]{baader:ecai-90}
Baader, F. \BBOP1990\BBCP.
\newblock \BBOQ A formal definition for expressive power of knowledge
  representation languages\BBCQ\
\newblock In {\Bem Proceedings of the 9th European Conference on Artificial
  Intelligence (ECAI-90)}\ Stockholm, Sweden. Pitman.

\bibitem[\protect\BCAY{B{\"a}ckstr{\"o}m}{B{\"a}ckstr{\"o}m}{1995}]{backstrom:%
ai-95}
B{\"a}ckstr{\"o}m, C. \BBOP1995\BBCP.
\newblock \BBOQ Expressive equivalence of planning formalisms\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 76\/}(1--2), 17--34.

\bibitem[\protect\BCAY{B{\"a}ckstr{\"o}m \BBA\ Nebel}{B{\"a}ckstr{\"o}m \BBA\
  Nebel}{1995}]{backstrom:nebel:ci-95}
B{\"a}ckstr{\"o}m, C.\BBACOMMA\  \BBA\ Nebel, B. \BBOP1995\BBCP.
\newblock \BBOQ Complexity results for {SAS$^{+}$} planning\BBCQ\
\newblock {\Bem Computational Intelligence}, {\Bem 11\/}(4), 625--655.

\bibitem[\protect\BCAY{Blum \BBA\ Furst}{Blum \BBA\
  Furst}{1997}]{blum:furst:ai-97}
Blum, A.~L.\BBACOMMA\  \BBA\ Furst, M.~L. \BBOP1997\BBCP.
\newblock \BBOQ Fast planning through planning graph analysis\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 90\/}(1-2), 279--298.

\bibitem[\protect\BCAY{Brewka \BBA\ Hertzberg}{Brewka \BBA\
  Hertzberg}{1993}]{brewka:hertzberg:jlc-93}
Brewka, G.\BBACOMMA\  \BBA\ Hertzberg, J. \BBOP1993\BBCP.
\newblock \BBOQ How to do things with worlds: On formalizing actions and
  plans.\BBCQ\
\newblock {\Bem Journal Logic and Computation}, {\Bem 3\/}(5), 517--532.

\bibitem[\protect\BCAY{Bylander}{Bylander}{1994}]{bylander:ai-94}
Bylander, T. \BBOP1994\BBCP.
\newblock \BBOQ The computational complexity of propositional {STRIPS}
  planning\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 69\/}(1--2), 165--204.

\bibitem[\protect\BCAY{Cadoli \BBA\ Donini}{Cadoli \BBA\
  Donini}{1997}]{cadoli:donini:aicom-97}
Cadoli, M.\BBACOMMA\  \BBA\ Donini, F.~M. \BBOP1997\BBCP.
\newblock \BBOQ A survey on knowledge compilation\BBCQ\
\newblock {\Bem AI Communications}, {\Bem 10\/}(3,4), 137--150.

\bibitem[\protect\BCAY{Cadoli, Donini, Liberatore, \BBA\ Schaerf}{Cadoli
  et~al.}{1996}]{cadoli:et:al:kr-96}
Cadoli, M., Donini, F.~M., Liberatore, P., \BBA\ Schaerf, M. \BBOP1996\BBCP.
\newblock \BBOQ Comparing space efficiency of propositional knowledge
  representation formalism\BBCQ\
\newblock In Aiello, L.~C., Doyle, J., \BBA\ Shapiro, S.\BEDS, {\Bem Principles
  of Knowledge Representation and Reasoning: Proceedings of the 5th
  International Conference (KR-96)}, \BPGS\ 364--373\ Cambridge, MA. Morgan
  Kaufmann.

\bibitem[\protect\BCAY{Erol, Hendler, \BBA\ Nau}{Erol
  et~al.}{1994}]{erol:et:al:aaai-94}
Erol, K., Hendler, J.~A., \BBA\ Nau, D.~S. \BBOP1994\BBCP.
\newblock \BBOQ {HTN} planning: Complexity and expressivity\BBCQ\
\newblock In {\Bem Proceedings of the 12th National Conference of the American
  Association for Artificial Intelligence (AAAI-94)}, \BPGS\ 1123--1129\
  Seattle, WA. MIT Press.

\bibitem[\protect\BCAY{Erol, Hendler, \BBA\ Nau}{Erol
  et~al.}{1996}]{erol:et:al:amai-96}
Erol, K., Hendler, J.~A., \BBA\ Nau, D.~S. \BBOP1996\BBCP.
\newblock \BBOQ Complexity results for hierarchical task-network planning\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem 18},
  69--93.

\bibitem[\protect\BCAY{Fikes \BBA\ Nilsson}{Fikes \BBA\
  Nilsson}{1971}]{fikes:nilsson:ai-71}
Fikes, R.~E.\BBACOMMA\  \BBA\ Nilsson, N. \BBOP1971\BBCP.
\newblock \BBOQ {STRIPS}: A new approach to the application of theorem proving
  to problem solving\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 2}, 189--208.

\bibitem[\protect\BCAY{Furst, Saxe, \BBA\ Sipser}{Furst
  et~al.}{1984}]{furst:et:al:mst-84}
Furst, M., Saxe, J.~B., \BBA\ Sipser, M. \BBOP1984\BBCP.
\newblock \BBOQ Parity, circuits, and the polynomial-time hierarchy\BBCQ\
\newblock {\Bem Mathematical Systems Theory}, {\Bem 17\/}(1), 13--27.

\bibitem[\protect\BCAY{Garey \BBA\ Johnson}{Garey \BBA\
  Johnson}{1979}]{garey:johnson:79}
Garey, M.~R.\BBACOMMA\  \BBA\ Johnson, D.~S. \BBOP1979\BBCP.
\newblock {\Bem Computers and In\-trac\-ta\-bi\-li\-ty---A Guide to the Theory
  of NP-Completeness}.
\newblock Freeman, San Francisco, CA.

\bibitem[\protect\BCAY{Gazen \BBA\ Knoblock}{Gazen \BBA\
  Knoblock}{1997}]{gazen:knoblock:ecp-97}
Gazen, B.~C.\BBACOMMA\  \BBA\ Knoblock, C. \BBOP1997\BBCP.
\newblock \BBOQ Combining the expressiveness of {UCPOP} with the efficiency of
  {Graphplan}\BBCQ\
\newblock In Steel, S.\BBACOMMA\  \BBA\ Alami, R.\BEDS, {\Bem Recent Advances
  in AI Planning. 4th European Conference on Planning (ECP'97)},
  \lowercase{\BVOL}\ 1348 of {\Bem {L}ecture {N}otes in {A}rtificial
  {I}ntelligence}, \BPGS\ 221--233\ Toulouse, France. Springer-Verlag.

\bibitem[\protect\BCAY{Gogic, Kautz, Papadimitriou, \BBA\ Selman}{Gogic
  et~al.}{1995}]{gogic:et:al:ijcai-95}
Gogic, G., Kautz, H.~A., Papadimitriou, C.~H., \BBA\ Selman, B. \BBOP1995\BBCP.
\newblock \BBOQ The comparative linguistics of knowledge representation\BBCQ\
\newblock In {\Bem Proceedings of the 14th International Joint Conference on
  Artificial Intelligence (IJCAI-95)}, \BPGS\ 862--869\ Montreal, Canada.
  Morgan Kaufmann.

\bibitem[\protect\BCAY{Kambhampati, Parker, \BBA\ Lambrecht}{Kambhampati
  et~al.}{1997}]{kambhampati:et:al:ecp-97}
Kambhampati, S., Parker, E., \BBA\ Lambrecht, E. \BBOP1997\BBCP.
\newblock \BBOQ Understanding and extending {G}raphplan\BBCQ\
\newblock In Steel, S.\BBACOMMA\  \BBA\ Alami, R.\BEDS, {\Bem Recent Advances
  in AI Planning. 4th European Conference on Planning (ECP'97)},
  \lowercase{\BVOL}\ 1348 of {\Bem {L}ecture {N}otes in {A}rtificial
  {I}ntelligence}, \BPGS\ 260--272\ Toulouse, France. Springer-Verlag.

\bibitem[\protect\BCAY{Karp \BBA\ Lipton}{Karp \BBA\
  Lipton}{1982}]{karp:lipton:ens-math-82}
Karp, R.~M.\BBACOMMA\  \BBA\ Lipton, R.~J. \BBOP1982\BBCP.
\newblock \BBOQ Turing machines that take advice\BBCQ\
\newblock {\Bem L' Ensignement Math{\'e}matique}, {\Bem 28}, 191--210.

\bibitem[\protect\BCAY{Kautz, McAllester, \BBA\ Selman}{Kautz
  et~al.}{1996}]{kautz:et:al:kr-96}
Kautz, H.~A., McAllester, D.~A., \BBA\ Selman, B. \BBOP1996\BBCP.
\newblock \BBOQ Encoding plans in propositional logic\BBCQ\
\newblock In Aiello, L.~C., Doyle, J., \BBA\ Shapiro, S.\BEDS, {\Bem Principles
  of Knowledge Representation and Reasoning: Proceedings of the 5th
  International Conference (KR-96)}, \BPGS\ 374--385\ Cambridge, MA. Morgan
  Kaufmann.

\bibitem[\protect\BCAY{Kautz \BBA\ Selman}{Kautz \BBA\
  Selman}{1992}]{kautz:selman:aaai-92}
Kautz, H.~A.\BBACOMMA\  \BBA\ Selman, B. \BBOP1992\BBCP.
\newblock \BBOQ Forming concepts for fast inference.\BBCQ\
\newblock In {\Bem Proceedings of the 10th National Conference of the American
  Association for Artificial Intelligence (AAAI-92)}, \BPGS\ 786--793\ San
  Jose, CA. MIT Press.

\bibitem[\protect\BCAY{Kautz \BBA\ Selman}{Kautz \BBA\
  Selman}{1996}]{kautz:selman:aaai-96}
Kautz, H.~A.\BBACOMMA\  \BBA\ Selman, B. \BBOP1996\BBCP.
\newblock \BBOQ Pushing the envelope: Planning, propositional logic, and
  stochastic search\BBCQ\
\newblock In {\Bem Proceedings of the 13th National Conference of the American
  Association for Artificial Intelligence (AAAI-96)}, \BPGS\ 1194--1201. MIT
  Press.

\bibitem[\protect\BCAY{Kautz \BBA\ Selman}{Kautz \BBA\
  Selman}{1998}]{kautz:selman:aips-ws-98}
Kautz, H.~A.\BBACOMMA\  \BBA\ Selman, B. \BBOP1998\BBCP.
\newblock \BBOQ {BLACKBOX}: {A} new approach to the application of theorem
  proving to problem solving\BBCQ\
\newblock In {\Bem Working notes of the AIPS'98 Workshop on Planning as
  Combinatorial Search}\ Pittsburgh, PA.

\bibitem[\protect\BCAY{Koehler, Nebel, Hoffmann, \BBA\ Dimopoulos}{Koehler
  et~al.}{1997}]{koehler:et:al:ecp-97}
Koehler, J., Nebel, B., Hoffmann, J., \BBA\ Dimopoulos, Y. \BBOP1997\BBCP.
\newblock \BBOQ Extending planning graphs to an {ADL} subset\BBCQ\
\newblock In Steel, S.\BBACOMMA\  \BBA\ Alami, R.\BEDS, {\Bem Recent Advances
  in AI Planning. 4th European Conference on Planning (ECP'97)},
  \lowercase{\BVOL}\ 1348 of {\Bem {L}ecture {N}otes in {A}rtificial
  {I}ntelligence}, \BPGS\ 273--285\ Toulouse, France. Springer-Verlag.

\bibitem[\protect\BCAY{Lifschitz}{Lifschitz}{1986}]{lifschitz:raap-86}
Lifschitz, V. \BBOP1986\BBCP.
\newblock \BBOQ On the semantics of {STRIPS}\BBCQ\
\newblock In Georgeff, M.~P.\BBACOMMA\  \BBA\ Lansky, A.\BEDS, {\Bem Reasoning
  about Actions and Plans: Proceedings of the 1986 Workshop}, \BPGS\ 1--9\
  Timberline, OR. Morgan Kaufmann.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1999}]{nebel:ecp-99}
Nebel, B. \BBOP1999\BBCP.
\newblock \BBOQ What is the expressive power of disjunctive
  preconditions?\BBCQ\
\newblock In Biundo, S.\BBACOMMA\  \BBA\ Fox, M.\BEDS, {\Bem Recent Advances in
  AI Planning. 5th European Conference on Planning (ECP'99)}\ Durham, UK.
  Springer-Verlag.
\newblock To appear.

\bibitem[\protect\BCAY{Papadimitriou}{Papadimitriou}{1994}]{papadimitriou:94}
Papadimitriou, C.~H. \BBOP1994\BBCP.
\newblock {\Bem Computational Complexity}.
\newblock Addison-Wesley, Reading, MA.

\bibitem[\protect\BCAY{Pednault}{Pednault}{1989}]{pednault:kr-89}
Pednault, E.~P. \BBOP1989\BBCP.
\newblock \BBOQ {ADL}: Exploring the middle ground between {STRIPS} and the
  situation calculus\BBCQ\
\newblock In Brachman, R., Levesque, H.~J., \BBA\ Reiter, R.\BEDS, {\Bem
  Principles of Knowledge Representation and Reasoning: Proceedings of the 1st
  International Conference (KR-89)}, \BPGS\ 324--331\ Toronto, ON. Morgan
  Kaufmann.

\bibitem[\protect\BCAY{Yap}{Yap}{1983}]{yap:tcs-83}
Yap, C.~K. \BBOP1983\BBCP.
\newblock \BBOQ Some consequences of non-uniform conditions on uniform
  classes\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 26}, 287--300.

\end{thebibliography}

\end{document}
 





