\documentstyle[amssymbols,theapa,jair,fleqn,eepic]{article}

\newcounter{A}
\newcounter{prgline}



\jairheading{6}{1997}{211-221}{12/96}{6/97}
\ShortHeadings{A Complete Classification of Tractability in RCC-5}
{Jonsson \& Drakengren}
\setcounter{page}{211}

% LaTeX macros for typesetting algorithms

\newlength{\prgindent}
\newenvironment{program}{
  \begin{list}%
   {\arabic{prgline}}%
   {%\normalsize % To get the em measure right
   \usecounter{prgline}
   \setlength{\prgindent}{0em}
   \setlength{\parsep}{0em}
   \setlength{\itemsep}{0em}
   \setlength{\labelwidth}{1em}
   \setlength{\labelsep}{1em}
   \setlength{\leftmargin}{\labelwidth}
   \addtolength{\leftmargin}{\labelsep}
   \setlength{\topsep}{0em}
   \setlength{\parskip}{0em} } }%
 {\end{list}}

\newif\ifprgendtext
\prgendtexttrue


\newenvironment{prgblock}{\addtolength{\prgindent}{\labelsep}}%
{\addtolength{\prgindent}{-\labelsep}}
\newcommand{\prgbeginblock}{\addtolength{\prgindent}{\labelsep}}
\newcommand{\prgendblock}{\addtolength{\prgindent}{-\labelsep}}
\newcommand{\prgcndendblock}[1]{\addtolength{\prgindent}{-\labelsep}
 \ifprgendtext \prglin\prgres{#1}\fi}


\newcommand{\prglin}{\rm \item\hspace{\prgindent}}
\newcommand{\prgcontlin}{\\  \hspace{\prgindent}}

\newcommand{\prgres}[1]{{\bf #1}}
\newcommand{\prgassn}{\leftarrow}
\newcommand{\prgname}[1]{{\it #1}}

\newcommand{\prgbegin}{\prglin\prgres{begin}\prgbeginblock}
\newcommand{\prgend}{\prgendblock\prglin\prgres{end\ }}
\newcommand{\prgnoend}{\prgendblock}

\newcommand{\prgif}{\prglin\prgres{if\ }}
\newcommand{\prgthen}{\prgres{\ then\ }\prgbeginblock}
\newcommand{\prgelse}{\prgendblock\prglin\prgres{else}\prgbeginblock}
\newcommand{\prgelsif}{\prgendblock\prglin\prgres{elsif\ }}
\newcommand{\prgendif}{\prgcndendblock{end if}}

\newcommand{\prgwhile}{\prglin\prgres{while\ }}
\newcommand{\prgfor}{\prglin\prgres{for\ }}
\newcommand{\prgdo}{\prgres{\ do}\prgbeginblock}
\newcommand{\prgrepeat}{\prgres{\ repeat}\prgbeginblock}
\newcommand{\prgloop}{\prglin\prgres{loop}\prgbeginblock}
\newcommand{\prgendloop}{\prgendblock\prglin\prgres{end loop}}
\newcommand{\prgendwhile}{\prgcndendblock{end while}}
\newcommand{\prgendfor}{\prgcndendblock{end for}}
\newcommand{\prguntil}{\prgendblock\prglin\prgres{until\ }}

\newcommand{\prgcomment}{\prglin\prgres{comment\ }\it }
\newcommand{\prgprocedure}{\prglin\prgres{procedure\ }}
\newcommand{\prgnil}{\prgres{\ nil}}
\newcommand{\prgtrue}{\prgres{\ true}}
\newcommand{\prgfalse}{\prgres{\ false}}
\newcommand{\prgnot}{\prgres{\ not\ }}
\newcommand{\prgand}{\prgres{\ and\ }}
\newcommand{\prgor}{\prgres{\ or \ }}
\newcommand{\prgfail}{\prgres{fail}}
\newcommand{\prgreturn}{\prgres{return\ }}
\newcommand{\prgaccept}{\prgres{accept}}
\newcommand{\prgreject}{\prgres{reject}}



\newcommand{\unprint}[1]{}

\newcommand{\texttt}[1]
  {{\tt #1}}
\newcommand{\ensuremath}[1]
  {\mbox{$#1$}}



\newcommand{\emdef}{\em}
\newcommand{\blankline}{$\:$}

\newcommand{\cA}{{\cal A}}
\newcommand{\cM}{{\cal V}}
\newcommand{\md}{{\rm MD}}

\newcommand{\ISAT}{\ensuremath{{\cal A}}{\rm -SAT}}
\newcommand{\Cl}[1]{\overline{#1}}


\newcommand{\inv}[1]{\ensuremath{{#1}^\smile}}





\newcommand{\spc}{\ }
\newcommand{\spii}{\ \ }
\newcommand{\spiii}{\ \ \ }
\newcommand{\spiv}{\ \ \ \ }
\newcommand{\spv}{\ \ \ \ \ }
\newcommand{\spvi}{\ \ \ \ \ \ }

\newcommand{\rdr}{{\tt DR}}
\newcommand{\rpo}{{\tt PO}}
\newcommand{\rpp}{{\tt PP}}
\newcommand{\rpq}{{\tt PPI}}
\newcommand{\req}{{\tt EQ}}



\newcommand{\rpib}{$\{${\tt b}$\}$}
\newcommand{\rpis}{$\{${\tt s}$\}$}
\newcommand{\rpid}{$\{${\tt d}$\}$}
\newcommand{\rpif}{$\{${\tt f}$\}$}
\newcommand{\rpia}{$\{${\tt a}$\}$}
\newcommand{\rpifull}{$\{${\tt b,s,d,f,a}$\}$}
\newcommand{\rpidfa}{$\{${\tt d,f,a}$\}$}
\newcommand{\rpibsd}{$\{${\tt b,s,d}$\}$}


\newcommand{\rdrx}{\rdr \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ }
\newcommand{\rpox}{\rpo \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ }
\newcommand{\rppx}{\rpp \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ }
\newcommand{\rpqx}{\rpq \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ }
\newcommand{\reqx}{\req \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ }


%%%%

% File: mathmacros.tex

% Last edited: Fri Jun 16 12:28:08 1995 by petej@brut2 (Peter Jonsson)

% Some useful LaTeX macros, mainly math, to be input in head of LaTeX files

%%%%%%%%% Old macros

% Shortcuts for writing the name of an author and do or several shortcites
\newcommand{\namecite}[1]{\citeauthor{#1}~\citeyear{#1}}
%\newcommand{\nameciteii}[2]{\citeauthor{#1}~\citeyear{#1,#2}}
%\newcommand{\nameciteiii}[3]{\citeauthor{#1}~\citeyear{#1,#2,#3}}

% Command for advanced citations
% \citelist simply puts it argument inside citation ['s and ]'s
% \scite, \mciteii, \mciteiii ... should be used in the argument of \citelist
% \scite makes an ordinary reference, but without the ['s and ]'s
% \mciteii takes two citekeys which should refer to the same author(s)
%   and writes the name(s) once followed by the years of both references
% \mciteiii works as \mciteii but for three references of the same author(s)
\newcommand{\citelist}[1]{\raisebox{.2ex}{[}#1\raisebox{.2ex}{]}}
\newcommand{\scite}[1]{\citeauthor{#1}, \citeyear{#1}}
\newcommand{\mciteii}[2]{\citeauthor{#1}, \citeyear{#1}, %
\citeyear{#2}}
\newcommand{\mciteiii}[3]{\citeauthor{#1}, \citeyear{#1}, %
\citeyear{#2}, \citeyear{#3}}

% Shortcut for making a compact reference to several works by the same author(s)
\newcommand{\multiciteii}[2]{\citelist{\scite{#1}, \citeyear{#2}}}
\newcommand{\multiciteiii}[3]%
  {\citelist{\scite{#1}, \citeyear{#2}, \citeyear{#3}}}



%%%%%%%%%%%%%%%%%%%%%%%
%% Fix greek letters %%
%%%%%%%%%%%%%%%%%%%%%%%

\renewcommand{\phi}{\varphi}
\renewcommand{\epsilon}{\varepsilon}


\newcommand{\draft}{\begin{center}\huge Draft!!! \end{center}}
\newcommand{\void}{\makebox[0mm]{}}	% Often needed to fool LaTeX

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Commands to write text in math mode %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\text}[1]{\mbox{\rm \,#1\,}}	% To write text in mathmode

% Abbrev's for frequently used words
\newcommand{\tand}{\text{\ and\ }}
\newcommand{\tor}{\text{\ or\ }}
\newcommand{\tif}{\text{\ if\ }}
\newcommand{\tiff}{\text{\ iff\ }}
\newcommand{\tfor}{\text{\ for\ }}
\newcommand{\tforall}{\text{\ for all\ }}
\newcommand{\totherwise}{\text{\ otherwise}}


%%%%%%%%%%%%%%%%%%%
%% Miscellaneous %%
%%%%%%%%%%%%%%%%%%%

\newcommand{\fnl}{\void \\}		% Force newline

\newcommand{\pushlist}[1]{\setcounter{#1}{\value{enumi}} \end{enumerate}}
\newcommand{\poplist}[1]{\begin{enumerate} \setcounter{enumi}{\value{#1}}}
 % These commands makes it possible to break a first level enumerate list
 % and resume it later on. There must be a \newcounter{foo} command at
 % the beginning of the top level file, though.


%%%%%%%%%%
%% Math %%
%%%%%%%%%%

%% Sets
\renewcommand{\emptyset}{\varnothing}  % The usual empty set,  not LaTeX std.
				   % Requires the ``amssymbols'' option
\newcommand{\union}{\cup} 		% Union
\newcommand{\intersect}{\cap}		% intersection
\newcommand{\setdiff}{-}		% Set difference
\newcommand{\compl}[1]{\overline{#1}}	% Set complement
\newcommand{\card}[1]{{|#1|}}		% Cardinality     
\newcommand{\set}[1]{\{{#1}\}} % Set 
\newcommand{\st}{\ |\ }		     	% `such that' symbol in sets
\newcommand{\suchthat}{\st}		% Old, do not use
\newcommand{\cprod}{\times}		% Cartesian product
\newcommand{\powerset}[1]{{\bf 2}^{#1}}	% Powerset

%% Other math
\newcommand{\tuple}[1]{\langle{#1}\rangle}  % Tuple
\newcommand{\seq}[1]{\langle #1 \rangle}
\newcommand{\emptyseq}{\seq{}}
\newcommand{\floor}[1]{\left\lfloor{#1}\right\rfloor}
\newcommand{\ceiling}[1]{\left\lceil{#1}\right\rceil}

%% Functions
\newcommand{\map}{\rightarrow}
\newcommand{\fncomp}{\!\circ\!}		% Function composition


%% Relations
\newcommand{\transclos}[1]{#1^+}
\newcommand{\reduction}[1]{#1^-}	% Warning! non-standard notation


%% Lattices
\newcommand{\latlt}{\sqsubset}		% Lattice `less than'
\newcommand{\latleq}{\sqsubseteq}	% Lattice `less or equal'
\newcommand{\join}{\sqcup}		% Join
\newcommand{\meet}{\sqcap}		% Meet
\newcommand{\latbot}{\bot}		% Bottom eltTop elt
\newcommand{\lattop}{\top}		% Top elt

%% Logic
\newcommand{\limp}{\rightarrow} 
\newcommand{\leqv}{\leftrightarrow}
\newcommand{\falsum}{\bot}
 
\newcommand{\turnst}{\vdash}		% Turnstile
\newcommand{\nturnst}{\nvdash}		% Negated turnstile
\newcommand{\modls}{\vDash}		% Double turnstile
\newcommand{\nmodls}{\nvDash}		% negated double turnstile

%% Environments %%
%%%%%%%%%%%%%%%%%%

\newif\ifnoemthenvs
\noemthenvsfalse

% These are used indirectly by the following group of new environments
\newtheorem{defnx}{Definition}[section]
\newtheorem{axiomx}[defnx]{Axiom}
\newtheorem{theoremx}[defnx]{Theorem}
\newtheorem{propositionx}[defnx]{Proposition}
\newtheorem{lemmax}[defnx]{Lemma}
\newtheorem{factx}[defnx]{Fact}
\newtheorem{corollx}[defnx]{Corollary}
\newtheorem{algx}{Algorithm}[section]
\newtheorem{exx}[defnx]{Example}
\newtheorem{restrx}{Restriction}[section]

% New environments that don't print in italics
\newcommand{\QED}{\nopagebreak[4]{\makebox[1mm]{}\hfill$\Box$}}
\newenvironment{definition}{\begin{defnx}\em}{\end{defnx}}
\newenvironment{axiom}{\begin{axiomx}\em}{\end{axiomx}}
\newenvironment{theorem}{\begin{theoremx}\em}{\end{theoremx}}
\newenvironment{proposition}{\begin{propositionx}\em}{\end{propositionx}}
\newenvironment{lemma}{\begin{lemmax}\em}{\end{lemmax}}
\newenvironment{fact}{\begin{factx}\em}{\end{factx}}
\newenvironment{corollary}{\begin{corollx}\em}{\end{corollx}}
\newenvironment{algorithm}{\begin{algx}\em}{\end{algx}}
\newenvironment{example}{\begin{exx}\em}{\end{exx}}
\newenvironment{restr}{\begin{restrx}\em}{\end{restrx}}
\newenvironment{proof}{\noindent {\bf \noindent Proof: }}{\QED}
\newenvironment{proofsk}{\noindent {\bf \noindent Proof sketch: }}{\QED}
\newenvironment{emptyproof}{\noindent {\bf \noindent Proof: }}{}


%%%%

\newlength{\oldtopmargin}
\setlength{\oldtopmargin}{\topmargin}

\prgendtextfalse


\title{A Complete Classification of Tractability in RCC-5}
\author{\name Peter Jonsson
        \email petej@ida.liu.se \\
        \name Thomas Drakengren
        \email thodr@ida.liu.se \\
        \addr Department of Computer and Information Science, Linköping University\\
              S-581 83 Linköping, Sweden}


%\author{Peter Jonsson and Thomas Drakengren\\
%Department of Computer and Information Science\\
%Linköping University, S-581 83 Linköping, Sweden\\
%email: {\tt $\{$petej,thodr$\}$@ida.liu.se}}
%\date{}


\begin{document}

\researchnote

\maketitle

\begin{abstract}
We investigate the computational properties of the
spatial algebra RCC-5 which is a restricted version of the
RCC framework for spatial reasoning. 
The satisfiability problem for RCC-5 is known
to be NP-complete but not much is known about its approximately
four billion subclasses. We provide a complete classification
of satisfiability for all these subclasses into polynomial and
NP-complete respectively. In the process, we identify all
maximal tractable subalgebras which are four in total.
\end{abstract}



\section{Introduction}

Qualitative spatial reasoning has received a constantly increasing
amount of interest in the literature. The main reason for this is, probably,
that spatial reasoning has proved to be applicable to
real-world problems in, for example, geographical database
systems \cite{Egenhofer:ssd91,Grigni:etal:ijcai95} and
molecular biology \cite{Cui:ismb94}. In both these applications,
the size of the problem instances can be huge, so
the complexity of
problems and algorithms is a highly relevant area to study.
However, questions of
computational complexity have not received so much 
attention in the literature;
two notable exceptions are the results reported by \namecite{Nebel:ki95}
and \namecite{Renz:Nebel:ijcai97}. 
In this article we take a small step
towards a better understanding of complexity issues in qualitative
spatial reasoning.

A well-known framework for qualitative spatial reasoning
is the so-called RCC approach
\cite{Randell:Cohn:kr89,Randell:etal:kr92}.
This approach is based on modelling qualitative spatial
relations between regions using first-order logic.
Of special interest, from a complexity-theoretic standpoint, are the two subclasses 
RCC-5 and RCC-8.
It is well-known that both RCC-5 and RCC-8 have quite weak expressive power.
Although they can be used to describe spatial situations, they
are very general and should perhaps better be described as topological
algebras. However, we will denote these algebras as spatial
algebras in order to avoid terminological confusion; the term
topological algebra has a well-established but completely different meaning
in mathematics \cite{Mallios:TA}.

\namecite{Bennett:kr94} has shown the sufficiency of
using propositional logics for reasoning about RCC-5 and RCC-8. 
Hence, the reasoning becomes more efficient when
compared to reasoning in a full first-order logic.
Bennett's approach uses classical propositional logic for
RCC-5 and intuitionistic propositional logic for RCC-8.
Unfortunately, these logics are known to be computationally
hard. The satisfiability problem for classical propositional logic
and intuitionistic propositional logic is NP-complete \cite{Cook:stoc71}
 and
{\sc Pspace}-complete \cite{Statman:tcs79} respectively.
However, the complexity of the underlying logic does not carry over
in both cases; \namecite{Renz:Nebel:ijcai97} have shown that the satisfiability
problem for both RCC-5 and RCC-8 is NP-complete. The full proofs
can be found in \cite{Renz:xjobb}.

These findings motivate the search for tractable subclasses of
RCC-5 and RCC-8. \namecite{Nebel:ki95} showed that reasoning
with the basic relations in RCC-8 is a polynomial-time problem.
\namecite{Renz:Nebel:ijcai97} improved this result substantially by
showing the following results:

\begin{itemize}
\item
There exists a large, maximal 
subclass of RCC-8, denoted $\widehat{{\cal H}}_8$,
which contains all basic relations and is polynomial. 
$\widehat{{\cal H}}_8$ contains 148 elements out of 256 (58\%).

\item
There exists a large, maximal 
subclass of RCC-5, denoted $\widehat{{\cal H}}_5$,
which contains all basic relations and is polynomial. 
$\widehat{{\cal H}}_5$ contains 28 elements out of 32 (87\%).
Furthermore, this is the unique, maximal subclass of
RCC-5 containing all basic relations.
\end{itemize}

\noindent
We will concentrate on RCC-5 in this article. The main result 
is a complete classification of
all subclasses of RCC-5 with respect to tractability.
The classification makes it possible to determine
whether a given subclass is tractable or not by a simple test
that can be carried out by hand or automatically.
We have thus gained a clear picture of the tractability borderline
in RCC-5. As is more or less necessary when showing results
of this kind, the main proof relies on a case analysis
performed by a computer. The number of cases considered
was roughly $4 \times 10^4$. 
The analysis cannot, of course, be reproduced in a research paper
or be verified manually. Hence, we include a description
of the programs used. The programs are also available as an on-line
appendix to this article.

The structure of the article is as follows: Section~2 defines RCC-5
and some auxiliary concepts. Section~3 contains the tractability
proofs for three subclasses of RCC-5. In Section~4 we show
that these subclasses together with $\widehat{{\cal H}}_5$ 
are the only maximal tractable subclasses of RCC-5.
The article concludes with a brief discussion of the results.

\section{The RCC-5 Algebra}

We follow \namecite{Bennett:kr94} in our definition of RCC-5.
RCC-5 is based on the
notions of {\emdef regions} and
{\emdef binary relations} on them.
A region $p$ is a variable interpreted over the non-empty subsets
of some fixed set. It should be noted that we do not require the sets
to be open sets in some topological space. This is no limitation
since it is impossible to distinguish interior points from
boundary points in RCC-5.
Thus we can
take any set ${\cal X}$ and use the discrete topology
${\cal T} = \langle {\cal X}, 2^{\cal X} \rangle$, where every subset
of ${\cal X}$ is an open set in ${\cal T}$.






We assume that we have a fixed universe of variable
names for regions.
Then, an $R$-{\emdef interpretation} is a function 
that maps region variables to the non-empty subsets of some
set.

Given two interpreted regions, their
relation can be described by exactly one of the elements of
the set ${\bf B}$ of five {\emdef basic RCC-5 relations}.
The definition of these relations can be found in
Table~\ref{basicrels}. Figure~\ref{basicrels:pict} shows
2-dimensional examples of the relations in RCC-5. 
A formula of the form $X B Y$ where $X$ and $Y$ are regions
and $B \in {\bf B}$, is said to be
satisfied by an $R$-interpretation iff the interpretation of the
regions satisfies the relations specified
in Table~\ref{basicrels}.

To express indefinite information, unions of the basic relations
are used, written as sets of basic relations, leading
to $2^5$ binary RCC-5 relations. 
Naturally, a set of basic relations is to be interpreted as a
disjunction of the basic relations.
The set
of all RCC-5 relations $2^{{\bf B}}$ is denoted by
$R_5$. Relations of special interest are the {\emdef null} relation
$\emptyset$ (also denoted by $\bot$) and the
{\emdef universal} relation ${\bf B}$ (also denoted $\top$).
%With the notation
%$\neg x$ we mean the relation ${\bf B}-\{x\}$,
%{\em e.g.} $\neg \pia = \{\pib,\pis,\pid,\pif\}$.

A formula of the form $X \{B_1,\ldots,B_n\} Y$ is called an
RCC-5 formula. Such a formula is satisfied by
an $R$-interpretation $\Im$ iff
$X B_i Y$ is satisfied by $\Im$ for some $i$, $1 \leq i \leq n$.
A finite set $\Theta$ of RCC-5 formulae is said to be
$R$-{\em satisfiable} iff there exists an $R$-interpretation
$\Im$ that satisfies every formula of $\Theta$.
Such a satisfying $R$-interpretation is called an
{\emdef $R$-model} of $\Theta$. 
Given an $R$-interpretation $\Im$ and a variable $v$, we write
$\Im(v)$ to denote the value of $v$ under the interpretation $\Im$.

The reasoning problem
we will study is the following:

\blankline

\noindent
{\sc Instance}: A finite set $\Theta$ of RCC-5 formulae.\\
{\sc Question}: Does there exist an $R$-model of 
$\Theta$?

\blankline

\noindent
We denote this problem by RSAT. In the following, we often
consider restricted versions of RSAT where the relations
used in formulae in $\Theta$ are only from a subset
$S$ of $R_5$. In this case we say that
$\Theta$ is a set of formulae over $S$ and we use a 
parameter in the problem description to denote the subclass
under consideration, {\em e.g.}, RSAT($S$).
Note that
an RSAT problem instance can be represented by a labelled
directed graph, where the nodes are region variables
and the arcs are labelled by relations between variables.
Given an instance $\Theta$ of RSAT, we say that such a graph is a
{\em graph representation} of $\Theta$.

We continue by defining an algebra over the RCC-5 relations.


\begin{definition}
Let ${\bf B} = \{\rdr,\rpo,\rpp,\rpq,\req\}$.
The RCC-5 algebra consists of the set
$R_5 = 2^{{\bf B}}$ and the operations
unary {\emdef converse} (denoted by $^\smile$),
binary {\emdef intersection} (denoted by $\cap$) and
binary {\emdef composition} (denoted by $\circ$).
They are defined as follows:

\blankline

\begin{tabular}{lrcl}
$\forall X,Y$: & $X R^\smile Y$ & iff & $Y R X$\\

$\forall X,Y$: & $X (R \cap S) Y$ & iff & $X R Y  \wedge 
                                               X  S  Y$\\

$\forall X,Y$: & $X (R \circ S) Y$ & iff & $\exists Z:(XRZ \wedge ZSY)$
\end{tabular}
\end{definition}


\begin{table}
\centering
\begin{tabular}{lll}

$X \{\rdr\} Y$ & iff & $X \cap Y = \emptyset$\\

$X \{\rpo\} Y$ & iff & $\exists a,b,c: a \in X, a \not\in Y,
                                  b \in X, b \in Y,
                                  c \not\in X, c \in Y$\\

$X \{\rpp\} Y$ & iff & $X \subset Y$\\

$X \{\rpq\} Y$ & iff & $X \supset Y$\\

$X \{\req\} Y$ & iff & $X = Y$\\
\end{tabular}


\caption{The five basic relations of RCC-5.}
\label{basicrels}
\end{table}

\begin{figure}
\centering
\vspace*{0.5cm}
\setlength{\unitlength}{0.00083333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined
% extract first six characters in \fmtname
\def\x#1#2#3#4#5#6#7\relax{\def\x{#1#2#3#4#5#6}}%
\expandafter\x\fmtname xxxxxx\relax \def\y{splain}%
\ifx\x\y   % LaTeX or SliTeX?
\gdef\SetFigFont#1#2#3{%
  \ifnum #1<17\tiny\else \ifnum #1<20\small\else
  \ifnum #1<24\normalsize\else \ifnum #1<29\large\else
  \ifnum #1<34\Large\else \ifnum #1<41\LARGE\else
     \huge\fi\fi\fi\fi\fi\fi
  \csname #3\endcsname}%
\else
\gdef\SetFigFont#1#2#3{\begingroup
  \count@#1\relax \ifnum 25<\count@\count@25\fi
  \def\x{\endgroup\@setsize\SetFigFont{#2pt}}%
  \expandafter\x
    \csname \romannumeral\the\count@ pt\expandafter\endcsname
    \csname @\romannumeral\the\count@ pt\endcsname
  \csname #3\endcsname}%
\fi
\fi\endgroup
\begin{picture}(4311,1484)(0,-10)
\thicklines
\put(2075,987){\ellipse{372}{372}}
\put(2183,990){\ellipse{600}{450}}
\put(2333,936){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$Y$}}}}}
\put(2030,930){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$X$}}}}}
\put(2075,987){\ellipse{372}{372}}
\put(2183,990){\ellipse{600}{450}}
\put(2333,936){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$Y$}}}}}
\put(2030,930){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$X$}}}}}
\put(308,1236){\ellipse{600}{450}}
\put(308,636){\ellipse{600}{450}}
\put(1283,1086){\ellipse{600}{450}}
\put(1283,861){\ellipse{600}{450}}
\put(3983,1011){\ellipse{600}{450}}
\put(2975,987){\ellipse{372}{372}}
\put(3083,990){\ellipse{600}{450}}
\put(257,1185){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$X$}}}}}
\put(254,573){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$Y$}}}}}
\put(1238,1137){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$X$}}}}}
\put(1238,675){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$Y$}}}}}
\put(2930,930){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$Y$}}}}}
\put(3233,936){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$X$}}}}}
\put(3809,954){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$X$}}}}}
\put(4079,954){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$Y$}}}}}
\put(22,27){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$\rdr(X,Y)$}}}}}
\put(983,36){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$\rpo(X,Y)$}}}}}
\put(1918,36){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$\rpp(X,Y)$}}}}}
\put(2760,36){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$\rpq(X,Y)$}}}}}
\put(3758,36){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{12.0}{rm}$\req(X,Y)$}}}}}
\end{picture}

\caption{Pictorial example of the relations in RCC-5.}
\label{basicrels:pict}
\end{figure}

\noindent
If ${\cal S}$ is a subset of $R_5$,
${\cal S}$ is said to be a {\em subalgebra} of
RCC-5 iff ${\cal S}$ is closed under converse, intersection and
composition. 
It can easily be verified that $R \circ S =
\bigcup \{B \circ B' | B \in R,B' \in S\}$,
{\em i.e.}, composition is the union of the component-wise
composition of basic relations. 

Next, we introduce a {\em closure} operation.
The closure operation transforms a given subclass of $R_5$
to one that is polynomially equivalent to the original subclass with
respect to satisfiability.
The operation is similar to the closure operation
for RCC-5 introduced by \namecite{Renz:xjobb} but it does not
pose the same restrictions on the given subclass. (Renz's operation
requires $\{\req\}$ to be a member of the subclass to be closed.)


\begin{definition} \label{mclosuredef} 
    Let ${\cal S}\subseteq R_5$.
    Then we denote by $\Cl{{\cal S}}$ the {\em closure} of 
    ${\cal S}$,
    defined as the least subalgebra containing ${\cal S}$ closed
    under converse, intersection and composition.
\end{definition}

\noindent
Observe that a subset ${\cal S}$ of $R_5$ is a subalgebra
iff ${\cal S}=\Cl{{\cal S}}$.
 
The next lemma is given without proof. A proof of the analogous
result for Allen's algebra can be found in
\namecite{Nebel:Burckert:jacm95}.

\begin{lemma} \label{mclosuretransform}
Let ${\cal S} \subseteq R_5$. Then
RSAT($\Cl{{\cal S}}$) can be polynomially transformed
to RSAT(${\cal S}$) and vice versa.
\end{lemma}

\begin{corollary} \label{closureprop1}
Let ${\cal S} \subseteq R_5$.
RSAT(${\cal S}$) is polynomial iff
RSAT($\Cl{{\cal S}}$) is polynomial.
RSAT(${\cal S}$) is NP-complete iff
RSAT($\Cl{{\cal S}}$) is NP-complete.
\end{corollary}




\section{Tractable Subclasses of RCC-5}

We begin this section by defining four tractable
subalgebras of RCC-5, which can be found in
Table~\ref{algebrarels}. Later on, we
show that these algebras are the only maximal tractable subalgebras
of RCC-5. 
The tractability of the first algebra, $R^{28}_5$, has been established by
\namecite{Renz:Nebel:ijcai97}. The name $R^{28}_5$ reflects the fact that
the algebra contains 28 elements.



\begin{theorem}
RSAT($R^{28}_5$) is polynomial.
\end{theorem}

\noindent
The tractability of our second algebra, $R^{20}_5$, 
can be settled quite easily. The algorithm can be found
in Figure~\ref{fig:r20alg}.

\begin{lemma}
Let $\Theta$ be an instance of RSAT$(R^{20}_5)$.
The algorithm $A^{20}$ accepts on input $\Theta$ iff $\Theta$ has an
$R$-model.
\end{lemma}
\begin{proof}
{\em if:} We show the contrapositive, {\em i.e.}, if
$A^{20}$ rejects then $\Theta$ has
no $R$-model. 
Clearly, the satisfiability of $\Theta$ is preserved
under the transformations made in lines 7-10.
Note that if $X R X \in \Theta$ then $\req \in R$
if $\Theta$ is satisfiable. Thus $\Theta$ is not satisfiable
if the algorithm rejects in line 5. Similarly,
$\Theta$ is not satisfiable if the algorithm rejects in line 6.

\blankline

\noindent
{\em only-if:} Consider the set $\Theta$ after the completion
of line 11. We denote this set by $\Theta'$. 
Obviously, $\Theta'$ is satisfiable if
the initial $\Theta$ was satisfiable.
Also observe that line 7 ensures that
$\Theta'$ does not relate any variables with $\req$.
Furthermore, line 8 guarantees that there is at most
one relation that relates two variables.

Now, we construct an $R$-model $M$ for $\Theta'$ as follows:
Let $V$ be the set of variables in $\Theta'$.
Let $M$ assign 
non-empty sets that are pairwise disjoint to the members of $V$.
Let ${\cal U}=\bigcup_{X \in V} M(X)$.
Introduce a set of values $U' = \{\alpha_{X,Y} \; | \; X,Y \in V\}$
satisfying the following:

\begin{enumerate}
\item
$\alpha_{X,Y} = \alpha_{Z,W}$ iff $X=Z$ and $Y=W$; and

\item
for arbitrary $X,Y \in V$, $\alpha_{X,Y} \not\in {\cal U}$.
\end{enumerate}

\noindent
For each relation of the type $X \{\rpo\} Y$ or $X \{\rpo,\req\} Y$,
extend the sets $M(X)$ and $M(Y)$ with the
element $\alpha_{X,Y}$.

Clearly, two sets $X,Y$ are disjoint (and are thus related
by $\rdr$) under $M$ unless $X \{\rpo\} Y$ or
$X \{\rpo,\req\} Y$ is in $\Theta$. But in these cases,
$X$ and $Y$ must not be disjoint. In fact, by introducing
$\alpha_{X,Y}$, we have forced $X \{\rpo\} Y$ to hold under $M$ which
satisfies formulae of the type $X \{\rpo\} Y$ as well
as formulae of the type $X \{\rpo,\req\} Y$. Hence, $M$ is
an $R$-model of $\Theta'$ which implies the $R$-satisfiability of
$\Theta$.
\end{proof}


\newcommand{\bt}{$\bullet$}
\begin{table*}[tb] 


\blankline

\centering
\begin{tabular}{|l|c|c|c|c|} \hline 
&
$R^{28}_5$ &
$R^{20}_5$ &
$R^{17}_5$ &
$R^{14}_5$ \\ \hline \hline

$\bot$                         & \bt & \bt & \bt & \bt \\ \hline
$\{\rdr\}$                     & \bt & \bt &     &     \\ \hline
$\{\rpo\}$                     & \bt & \bt &     &     \\ \hline
$\{\rdr,\rpo\}$                & \bt & \bt &     &     \\ \hline
$\{\rpp\}$                     & \bt &     &     & \bt \\ \hline
$\{\rdr,\rpp\}$                & \bt & \bt &     &     \\ \hline
$\{\rpo,\rpp\}$                & \bt &     &     &     \\ \hline
$\{\rdr,\rpo,\rpp\}$           & \bt & \bt &     &     \\ \hline
$\{\rpq\}$                     & \bt &     &     & \bt \\ \hline
$\{\rdr,\rpq\}$                & \bt & \bt &     &     \\ \hline
$\{\rpo,\rpq\}$                & \bt &     &     &     \\ \hline
$\{\rdr,\rpo,\rpq\}$           & \bt & \bt &     &     \\ \hline
$\{\rpp,\rpq\}$                &     &     &     & \bt \\ \hline
$\{\rdr,\rpp,\rpq\}$           &     & \bt &     & \bt \\ \hline
$\{\rpo,\rpp,\rpq\}$           & \bt &     &     & \bt \\ \hline
$\{\rdr,\rpo,\rpp,\rpq\}$      & \bt & \bt &     & \bt \\ \hline

$\{\req\}$                     & \bt & \bt & \bt & \bt \\ \hline
$\{\rdr,\req\}$                & \bt & \bt & \bt &    \\ \hline
$\{\rpo,\req\}$                & \bt & \bt & \bt &     \\ \hline
$\{\rdr,\rpo,\req\}$           & \bt & \bt & \bt &     \\ \hline
$\{\rpp,\req\}$                & \bt &     & \bt & \bt \\ \hline
$\{\rdr,\rpp,\req\}$           & \bt & \bt & \bt &     \\ \hline
$\{\rpo,\rpp,\req\}$           & \bt &     & \bt &     \\ \hline
$\{\rdr,\rpo,\rpp,\req\}$      & \bt & \bt & \bt &     \\ \hline
$\{\rpq,\req\}$                & \bt &     & \bt & \bt \\ \hline
$\{\rdr,\rpq,\req\}$           & \bt & \bt & \bt &     \\ \hline
$\{\rpo,\rpq,\req\}$           & \bt &     & \bt &     \\ \hline
$\{\rdr,\rpo,\rpq,\req\}$      & \bt & \bt & \bt &     \\ \hline
$\{\rpp,\rpq,\req\}$           &     &     & \bt & \bt \\ \hline
$\{\rdr,\rpp,\rpq,\req\}$      &     & \bt & \bt & \bt \\ \hline
$\{\rpo,\rpp,\rpq,\req\}$      & \bt &     & \bt & \bt \\ \hline
$\top$                         & \bt & \bt & \bt & \bt \\ \hline
\end{tabular}
\caption{The maximal tractable subalgebras of RCC-5.}
\label{algebrarels}
\end{table*}

\begin{theorem}
RSAT($R^{20}_5$) is polynomial.
\end{theorem}
\begin{proof}
Algorithm $A^{20}$ correctly solves the
RSAT($R^{20}_5$) problem by the previous lemma.
Furthermore, the number of iterations is bounded from above by the number
of variables and the number of formulae in the given instance
and the tests can easily be performed in polynomial time.
\end{proof}

\begin{figure}[tb]
\begin{program}
\prglin {\bf algorithm} $A^{20}$
\prglin Input: An instance $\Theta$ of RSAT($R^{20}_5$).
\prglin \prgrepeat
\prglin $\Theta' \prgassn \Theta$

\prgif $\exists X,R: \: XRX \in \Theta$ and $\req \not\in R$
\prgthen \prgreject \prgendif

\prgif $\exists X,Y: \: X \bot Y \in \Theta$ 
\prgthen \prgreject \prgendif

\prgif $\exists X,Y: \: X \neq Y$ and $X \{\req\}Y \in \Theta$ 
\prgthen substitute $Y$ for $X$ in $\Theta$ \prgendif

\prgif $\exists X,Y,R,S: \: XRY \in \Theta$ and 
$XSY \in \Theta$
\prgthen \prglin $\Theta \prgassn (\Theta-\{XRY,XSY\}) \cup \{X(R \cap S)Y\}$
\prgendif

\prgif $\exists X,R: \: XRX \in \Theta$ and $\req \in R$
\prgthen $\Theta \prgassn \Theta-\{XRX\}$ \prgendif

\prguntil $\Theta=\Theta'$
\prglin \prgaccept
\end{program}

\vspace*{0.6cm}

\begin{program}
\prglin {\bf algorithm} $A^{17}$
\prglin Input: An instance $\Theta$ of RSAT($R^{17}_5$).
\prgif $\exists X,Y$ such that $X \bot Y \in \Theta$ \prgthen
\prgreject
\prgelse $\:$ \prgaccept
\prgendif
\end{program}

\vspace*{0.6cm}

\begin{program}
\prglin {\bf algorithm} $A^9$
\prglin Input: An instance $\Theta$ of RSAT($R^{9}_5$) with graph
representation $G$.
\prglin Let $G'$ be the graph obtained from $G$ by removing
arcs which are not labelled $\{\rpp,\req\}$.
\prglin Find all strongly connected components $C$ in $G'$
\prgfor every arc $e$ in $G$ whose relation does not
contain $\req$ \prgdo
\prgif $e$ connects two nodes in some $C$ \prgthen \prgreject
\prgendif
\prgendfor
\prglin \prgaccept
\end{program}
\caption{Algorithms for RSAT($R^{20}_5$), RSAT($R^{17}_5$) and RSAT($R^{9}_5$).}
\label{fig:r14alg} \label{fig:r17alg} \label{fig:r20alg}
\end{figure}

\blankline

\noindent
Next we show the tractability of RSAT($R^{17}_5$).

\begin{theorem}
RSAT($R^{17}_5$) is polynomial.
\end{theorem}
\begin{proof}
Consider the algorithm $A^{17}$ in Figure~\ref{fig:r17alg}. If there
exist $X,Y$ such that $X \bot Y \in \Theta$ then
$\Theta$ is not satisfiable. Otherwise, we can let all
variables have the same value. Since $\req$ is a member
of every relation that occurs in $\Theta$, this interpretation
is an $R$-model of $\Theta$.
\end{proof}


\blankline

\noindent
We continue by proving that RSAT($R^{14}_5$) is a tractable problem.
Let \[R^9_5 =
\{\{\rpp,\req\}\} \cup 
\{R \cup \{\rpp,\rpq\} \: | \: R \in R_5\}.\]
Using a machine-assisted proof, it can be shown that
$R_5^{14} = \Cl{R_5^9}$ so it is sufficient to prove the tractability of
RSAT$(R_5^9)$ by
Corollary~\ref{closureprop1}.
The program that we used for showing this is available as
an on-line appendix to this article.

From now on, let $\Theta$ be an arbitrary instance
of RSAT($R^{9}_5$) and $G=\langle V,E \rangle$ be its
graph representation.
The following proofs are similar in spirit to some of the proofs
appearing in \namecite{Drakengren:Jonsson:aaai96}. The algorithm itself
is reminiscent of an algorithm by \namecite{vanBeek:ai92} 
for deciding satisfiability in the point algebra.

\begin{definition}
A RCC-5 relation $R$ is said to be an {\em acyclic} relation iff
any cycle in any $G$ with $R$ on every arc is never satisfiable. 
\end{definition}

\noindent
The relation $\rpp$ is an example of an acyclic relation while
$\{\rpp,\req\}$ is not acyclic. We continue by showing a few properties
of acyclic relations.

\begin{proposition} \label{firstcorollary}
Let $R$ be an acyclic relation. Then every relation $R' \subseteq R$
is acyclic.
\end{proposition}
\begin{proof}
Since taking subsets of $R$ constrains satisfiability further, the result
follows.
\end{proof}

\begin{proposition} \label{secondcorollary}
Let $R$ be an acyclic relation, and choose $A$ such that
$A \subseteq \{R' \: | \: R' \subseteq R\}$.
Then, any cycle in $G$ where every arc is labelled by some relation
in $A$ is unsatisfiable. 
\end{proposition}
\begin{proof}
Same argument as in the previous proposition.
\end{proof}

\blankline

\noindent
The following definition is needed in the following proofs.

\begin{definition}
Let ${\cal I}$ be an instance of the $R$-satisfiability problem,
$M$ a model for ${\cal I}$, and $r \in R_5$ a relation
between two region variables $X$ and $Y$ in ${\cal I}$.
Then $r$ is said to be {\em satisfied as} $r'$ in $M$ for
any relation $r' \subseteq r$, such that $X r' Y$ is satisfied in
$M$.
\end{definition}

\noindent
The definition may seem a bit cumbersome but the essence should
be clear. 
As an example, let $X$ and $Y$ be region variables related by
$X \{\rpo,\rpp\} Y$, and $M$ a model
where $X$ is interpreted as $\{1,2\}$ and $Y$ as
$\{1,2,3\}$. Then in $M$, $\{\rpo,\rpp\}$ is
satisfied as $\{\rpp\}$, but also as $\{\rpo,\rpp\}$.

\begin{lemma} \label{basiccycle}
Let $R$ be an acyclic relation, and $A,A'$ sets such that
$A \subseteq \{R' \: | \: R' \subseteq R\}$ and
$A' \subseteq \{a \cup \{\req\} \: | \: a \in A\}$.
Then, every cycle $C$ labelled by relations in
$A \cup A'$ is satisfiable iff it contains only relations from
$A'$. Furthermore, all relations in the cycle have to be satisfied
as $\req$.
\end{lemma}
\begin{proof}
{\em only-if:} Suppose that a cycle $C$ is satisfiable and that it contains
some relation from $A$. Apply induction on the number $n$ of arcs
in the cycle. For $n=1$, we get a contradiction by Proposition~\ref{secondcorollary}.
So, suppose for the induction that $C$ contains $n+1$ arcs.
Let $M$ be an $R$-model for the relations in $C$.
It cannot be the case that every relation in $C$ is satisfied in $M$
as some relation in $A$, by Proposition~\ref{secondcorollary}.
Thus, some relation $R'$ in $C$ has to be satisfied as $\req$.
But then we can collapse the two variables connected by $R'$
to one variable, and we have a cycle with $n$ nodes containing
a relation from $A$. This contradicts the induction hypothesis.

\blankline

\noindent
{\em if:} Suppose that a cycle $C$ contains only relations in $A'$.
Then $C$ can be satisfied by choosing $\req$ on every arc. Notice that 
the only-if part implies that $C$ {\em must} be satisfied by choosing
$\req$ on every arc. Hence, the variables are forced to be equal.
\end{proof}

\blankline

\noindent
After having studied acyclic relations, we will now turn our attention
to {\em DAG-satisfying} relations. The formal definition is as follows.

\begin{definition}
A basic relation $B$ is said to be {\emdef DAG-satisfying}
iff any DAG (directed acyclic graph) labelled only by
relations containing $B$ is satisfiable, {\em i.e.}, if the
corresponding RSAT problem has a model.
\end{definition}

\noindent
A typical example of a DAG-satisfying relation is $\req$. Given
a DAG labelled only by relations containing $\req$, we can always
satisfy these relations by assigning some non-empty set $S$ to all variables.

We can now show that $\rpp$ is a DAG-satisfying relation.

\begin{definition}
Let $G$ be an arbitrary DAG. A node $v$ in $G$ is said to be a {\em terminal} 
node iff there are no arcs which start in $v$.
\end{definition}

\begin{lemma} \label{ppdagsatlemma}
The basic relation $\rpp$ is DAG-satisfying.
\end{lemma}
\begin{proof}
Let $G$ be a DAG labelled only by relations containing $\rpp$.
We show that $G$ is satisfied by some $R$-model $M$. 
Induction on $n$ which is the number of nodes in $G$. The case when
$n=1$ is trivial. Suppose that $G$ has $n+1$ nodes and remove a
terminal node $g$. By induction, the remaining graph 
$G'=\langle V',E' \rangle$ is
satisfiable by a model $M'$. We shall now construct a model
$M$ of $G$, which agrees with $M'$ on every
variable in $G'$. Let $S=\bigcup \{M'(v) \: | \: v \in V'\}$ and 
let $\alpha$
be an element not in $S$.
Let $M(g)=S \cup \{\alpha\}$. Obviously, $M$ is
a model of $G$.
\end{proof}

\blankline

\noindent
We now state a simple result from \namecite{Drakengren:Jonsson:aaai96}.

\begin{lemma}
Let $G$ be irreflexive\footnote{A graph is irreflexive iff it has no
arcs from a node $v$ to the node $v$.}
and have an acyclic subgraph $D$.  
Then those arcs of $G$ which are not in $D$ can be reoriented
so that the resulting graph is acyclic.
\end{lemma}

\noindent
By specializing this result, we get the next lemma.

\begin{lemma} \label{satlemma}
Let $G$ be irreflexive with an acyclic subgraph $D$ and let the arcs
of $D$ be labelled by relations containing $\rpp$, and the arcs not
in $D$ being labelled by relations containing $\rpp$ and $\rpq$. Then
$G$ is $R$-satisfiable.
\end{lemma}
\begin{proof}
Reorient the arcs of $G$
such that the resulting graph is acyclic. This is always possible by the previous lemma.
Furthermore, whenever an arc is reoriented, also
invert the relation on that arc, so that $G'$ is satisfiable iff
$G$ is. By this construction, only arcs
containing both $\rpp$ and $\rpq$ have been reoriented, so every arc
in the DAG $G'$ contains $\rpp$ and, thus, since $\rpp$ is 
DAG-satisfying by Lemma~\ref{ppdagsatlemma}, 
$G'$ is satisfiable. Consequently, $G$
is also satisfiable.
\end{proof}

\blankline



\begin{lemma}
Algorithm $A^9$ correctly solves
RSAT($R_5^{9}$).
\end{lemma}
\begin{proof}
Assume that the algorithm finds a strongly connected component of
$G'$ (which then contains only the relation $\{\rpp,\req\}$),
containing two nodes that in $G$ are connected by an arc $e$ that is
labelled by a relation $R'$ which does not contain $\req$.
Then there exists a cycle $C$ in which the relation of every
arc contains $\req$, such that $e$ connects two nodes in that
$C$ but $e$ is not part of that cycle.
By Lemma~\ref{basiccycle}, $C$ can be satisfied only by
choosing the relation $\req$ on every arc in $C$, and since
$R'$ does not admit $\req$, $C$ is unsatisfiable.

Otherwise, every such strongly connected component can be collapsed to
a single node, removing all arcs which start and end in
the collapsed node. This transformation retains
satisfiability using the same argument as above.
After collapsing, the subgraph obtained by considering only
arcs labelled $\{\rpp,\req\}$ will be acyclic.
Since the remaining arcs are labelled by relations containing
both $\rpp$ and $\rpq$, the graph is $R$-satisfiable by
Lemma~\ref{satlemma}.
(Note that the graph will be irreflexive since every node is contained
in some strongly connected component.)
\end{proof}

\begin{lemma}
Given a graph $G=\langle V, E \rangle$,
algorithm $A^9$ runs in $O(|V|+|E|)$ time.
\end{lemma}
\begin{proof}
Strongly connected components can be found in $O(|V|+|E|)$ time
\cite{Baase:CA} and the remaining test can also
be made in $O(|V|+|E|)$ time.
\end{proof}

\begin{theorem}
RSAT($R_5^{14}$) can be solved in polynomial time.
\end{theorem}
\begin{proof}
RSAT($R_5^9$) is polynomial by the
previous two lemmata.
Since $R_5^{14} = \Cl{R_5^9}$,
RSAT$(R_5^{14})$ can be solved in polynomial time by
Corollary~\ref{closureprop1}.
\end{proof}






\section{Classification of RCC-5}

Before we can give the classification of RCC-5 we need two
NP-completeness results.

\begin{theorem}
RSAT(${\cal S}$) is NP-complete if

\begin{enumerate}
\item
\cite{Renz:Nebel:ijcai97}
${\cal C}_1 = \{ \{\rpo\},\{\rpp,\rpq\} \} \subseteq {\cal S}$, or

\item
${\cal C}_2 = \{ \{\rdr,\rpo\},\{\rpp,\rpq\} \} \subseteq {\cal S}$.
\end{enumerate}
\end{theorem}
\begin{proof}
The proof for ${\cal C}_2$ is by polynomial-time reduction from
RSAT(${\cal C}_1$). Let $\Theta$ be an arbitrary instance
of RSAT(${\cal C}_1$). Construct the following set:

\[\Theta'=\{X \{\rpp,\rpq\} Y \: | \: X \{\rpp,\rpq\} Y \in \Theta\}
\cup \{X \{\rdr,\rpo\} Y \: | \: X \{\rpo\} Y \in \Theta\}.\]

\noindent
Clearly, $\Theta'$ can be obtained from $\Theta$ in polynomial time
and $\Theta'$ is an instance of RSAT(${\cal C}_2$).
We show that $\Theta$ is satisfiable iff
$\Theta'$ is satisfiable.

\blankline

\noindent
{\em only-if:} Assume that there exists an $R$-model $I$ of
$\Theta$. It is not hard to see that $I$ is also an
$R$-model of $I'$ since if
$X \{\rpo\} Y$ under $I$ then
$X \{\rdr, \rpo\} Y$ under $I$. Thus 
$\Theta'$ is $R$-satisfiable if $\Theta$ is
$R$-satisfiable.

\blankline

\noindent
{\em if:} Assume the existence of an $R$-model $I'$ that assigns
subsets of some set ${\cal U}$ to the region variables of
$\Theta'$.
Let $\alpha$ be an element such that $\alpha \not\in {\cal U}$.
We construct a new interpretation
$I$ as follows: $I(x) = I'(x) \cup \{\alpha\}$ for every variable $x$ in
$\Theta'$. It can easily be seen that the following holds for
$I$:

\begin{enumerate}
\item
If $x \{\rdr\} y$ under $I'$ then $x \{\rpo\} y$ under $I$.

\item
If $x \{\rpo\} y$ under $I'$ then $x \{\rpo\} y$ under $I$.

\item
If $x \{\rpp\} y$ under $I'$ then $x \{\rpp\} y$ under $I$.

\item
If $x \{\rpq\} y$ under $I'$ then $x \{\rpq\} y$ under $I$.

\end{enumerate}

\noindent
It is easy to see that if $x \{\rpp,\rpq\} y$ under $I'$ then
$x \{\rpp,\rpq\} y$ under $I$. Similarly, if
$x \{\rdr, \rpo\} y$ under $I'$ then
$x \{\rpo\} y$ under $I$. It follows that $I$ is a model of
$\Theta$ so $\Theta$ is $R$-satisfiable if $\Theta'$ is
$R$-satisfiable.
\end{proof}

\blankline

\noindent
The main theorem can now be stated and proved.

\begin{theorem} \label{maintheorem}
For ${\cal S} \subseteq R_5$,
RSAT(${\cal S}$) is polynomial iff
${\cal S}$ is a subset of some member of 
$R_P=\{R^{28}_5,R^{20}_5,R^{17}_5,R^{14}_5\}$, and
NP-complete otherwise.
\end{theorem}
\begin{proof}
{\em if:}
For each $R \in R_P$,
RSAT($R$) is polynomial as was shown in the previous section.

\noindent
{\em only-if:}
Choose ${\cal S} \subseteq R_5$
such that ${\cal S}$
is not a subset of any algebra in $R_P$.
For each subalgebra $R \in R_P$, choose
a relation $x$ such that $x \in {\cal S}$ and $x \not\in R$.
This can always be done since ${\cal S} \not\subseteq R$.
Let $X$ be the set of these relations and note that
$X$ is not a subset of any algebra in $R_P$.
The set $R_P$ contains four algebras so by the construction
of $X$, $|X| \leq 4$. Observe that RSAT$({\cal S})$ is 
NP-complete if RSAT($X$) is NP-complete.

To show that RSAT$({\cal S})$ has to be NP-complete,
a machine-assisted case analysis of the
following form was performed:

\begin{enumerate}
\item
Generate all subsets of $R_5$ of size $\leq 4$. There are
$\displaystyle{\sum_{i=0}^4 
\left( \begin{array}{c} 32 \\ i \end{array} \right)}
= 41449$ such subsets.

\item
Let ${\cal T}$ be such a set. Test: ${\cal T}$ is a subset of
some subalgebra in $R_P$ or
${\cal C}_i \subseteq \Cl{{\cal T}}$ for some $i \in \{1,2\}$.
\end{enumerate}

\noindent
The test succeeds for all ${\cal T}$.
Hence, RSAT(${\cal S}$) is
NP-complete by Corollary~\ref{closureprop1}.
\end{proof} 

\blankline

\noindent
The program used for showing the previous theorem appears
in the on-line appendix of this article.

\section{Discussion}

The main problem of reporting tractability results for
restricted classes of problems is the difficulty of isolating interesting
and relevant subclasses.
The systematic approach of building complete classifications
is a way of partially overcoming this problem.
If the problem class under consideration is regarded relevant, then
its tractable subclasses should be regarded relevant if the computational
problem is of interest. 
This is especially true in spatial reasoning where the size of
the problem instances can be extremely large; one good example
is spatial reasoning in connection with the
Human Genome project \cite{Cui:ismb94}.

Another advantage with complete classifications is that they
are more satisfactory from a scientific
point of view; to gain a clear picture of the borderline between
tractability and intractability has an intrinsic scientific value.
A common critique is that complete classifications tend to
generate certain classes which are totally useless. For instance,
the subalgebra $R^{17}_5$ is certainly of no use. It must be made
clear that such critique is unjustified since the researcher
who makes a complete classification does not deliberately invent
useless classes. Instead, if useless classes appear in a complete
classification, they are unavoidable parts of the classification.

The work reported in this article 
can be extended in many different ways. One obvious
extension is to study other computational problems than the
RSAT problem. \namecite{Renz:xjobb} has studied
two problems, RMIN and RENT, on certain subclasses of
RCC-5 and RCC-8. The RMIN problem is to decide if a
set of spatial formulae $\Theta$ is minimal, {\em i.e.}, whether all
basic relations in every formula of $\Theta$ can be satisfied or not.
The RENT problem is to decide whether a formula $X R Y$
is entailed by a set of spatial formulae. 
\namecite{Grigni:etal:ijcai95} study a stronger form of
satisfiability which they refer to as {\em realizability}:
A finite set $\Theta$ of RCC-5 formulae is said to be realizable iff there
exist regions on the plane bounded by Jordan curves
which satisfy the relations in $\Theta$. 
\namecite{Grigni:etal:ijcai95} have shown that the realizability problem
is much harder than the satisfiability problem. For instance,
deciding realizability of formulae constructed from the two
relations $\rdr$ and $\rpo$ is NP-complete while the satisfiability
problem is polynomial.
Certainly, further studies of the realizability problem 
would be worthwhile.

Another obvious research direction is to completely classify other
spatial algebras, such as RCC-8. RCC-8 contains 
$2^{256} \approx 10^{77}$ relations so the question whether this is feasible or
not remains to be answered. 


\section{Conclusions}

We have studied computational properties of RCC-5.
All of the $2^{32}$ possible subclasses are classified
with respect to whether their corresponding satisfiability problem
is tractable or not. The classification reveals that there are four
maximal tractable subclasses of the algebra. 

%\newpage

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Baase}{Baase}{1988}]{Baase:CA}
Baase, S. \BBOP1988\BBCP.
\newblock {\Bem Computer Algorithms: Introduction and Analysis\/} (2nd \BEd).
\newblock Addison Wesley, Reading, MA.

\bibitem[\protect\BCAY{Bennett}{Bennett}{1994}]{Bennett:kr94}
Bennett, B. \BBOP1994\BBCP.
\newblock \BBOQ Spatial reasoning with propositional logics\BBCQ\
\newblock In Doyle, J., Sandewall, E., \BBA\ Torasso, P.\BEDS, {\Bem
  Proceedings of the 4th International Conference on Principles on Knowledge
  Representation and Reasoning (KR-94)}, \BPGS\ 165--176\ Bonn, Germany. Morgan
  Kaufmann.

\bibitem[\protect\BCAY{Cook}{Cook}{1971}]{Cook:stoc71}
Cook, S.~A. \BBOP1971\BBCP.
\newblock \BBOQ The complexity of theorem-proving procedures\BBCQ\
\newblock In {\Bem Proceedings of the 3rd ACM Symposium on Theory of
  Computing}, \BPGS\ 151--158.

\bibitem[\protect\BCAY{Cui}{Cui}{1994}]{Cui:ismb94}
Cui, Z. \BBOP1994\BBCP.
\newblock \BBOQ Using interval logic for order assembly\BBCQ\
\newblock In {\Bem Proceedings of the Second International Conference on
  Intelligent Systems for Molecular Biology}, \BPGS\ 103--111. AAAI Press.

\bibitem[\protect\BCAY{Drakengren \BBA\ Jonsson}{Drakengren \BBA\
  Jonsson}{1996}]{Drakengren:Jonsson:aaai96}
Drakengren, T.\BBACOMMA\  \BBA\ Jonsson, P. \BBOP1996\BBCP.
\newblock \BBOQ Maximal tractable subclasses of {A}llen's interval algebra:
  Preliminary report\BBCQ\
\newblock In {\Bem Proceedings of the 13th (US) National Conference on
  Artificial Intelligence (AAAI-96)}, \BPGS\ 389--394\ Portland, OR, USA.
  American Association for Artificial Intelligence.

\bibitem[\protect\BCAY{Egenhofer}{Egenhofer}{1991}]{Egenhofer:ssd91}
Egenhofer, M.~J. \BBOP1991\BBCP.
\newblock \BBOQ Reasoning about binary topological relations\BBCQ\
\newblock In Gunther, O.\BBACOMMA\  \BBA\ Schek, H.~J.\BEDS, {\Bem Advances in
  Spatial Databases}, \BPGS\ 143--160. Springer-Verlag.

\bibitem[\protect\BCAY{Grigni, Papadias, \BBA\ Papadimitriou}{Grigni
  et~al.}{1995}]{Grigni:etal:ijcai95}
Grigni, M., Papadias, D., \BBA\ Papadimitriou, C. \BBOP1995\BBCP.
\newblock \BBOQ Topological inference\BBCQ\
\newblock In Mellish, C.\BED, {\Bem Proceedings of the 14th International Joint
  Conference on Artificial Intelligence (IJCAI-95)}, \BPGS\ 901--906\
  Montr{\'e}al, PQ, Canada. Morgan Kaufmann.

\bibitem[\protect\BCAY{Mallios}{Mallios}{1986}]{Mallios:TA}
Mallios, A. \BBOP1986\BBCP.
\newblock {\Bem Topological Algebras. Selected Topics}.
\newblock North-Holland, Amsterdam.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1995}]{Nebel:ki95}
Nebel, B. \BBOP1995\BBCP.
\newblock \BBOQ Computational properties of qualitative spatial reasoning:
  {F}irst results\BBCQ\
\newblock In Wachsmuth, I., Rollinger, C.-R., \BBA\ Brauer, W.\BEDS, {\Bem
  {KI}-95: {A}dvances in {A}rtificial {I}ntelligence}, \BPGS\ 233--244\ Bielefeld,
  Germany. Springer-Verlag.

\bibitem[\protect\BCAY{Nebel \BBA\ B{\"u}rckert}{Nebel \BBA\
  B{\"u}rckert}{1995}]{Nebel:Burckert:jacm95}
Nebel, B.\BBACOMMA\  \BBA\ B{\"u}rckert, H.-J. \BBOP1995\BBCP.
\newblock \BBOQ Reasoning about temporal relations: {A} maximal tractable
  subclass of {A}llen's interval algebra\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 42\/}(1), 43--66.

\bibitem[\protect\BCAY{Randell \BBA\ Cohn}{Randell \BBA\
  Cohn}{1989}]{Randell:Cohn:kr89}
Randell, D.~A.\BBACOMMA\  \BBA\ Cohn, A.~G. \BBOP1989\BBCP.
\newblock \BBOQ Modelling topological and metrical properties of physical
  processes\BBCQ\
\newblock In Brachman, R.~J., Levesque, H.~J., \BBA\ Reiter, R.\BEDS, {\Bem
  Proceedings of the 1st International Conference on Principles on Knowledge
  Representation and Reasoning (KR-89)}, \BPGS\ 55--66\ Toronto, ON, Canada.
  Morgan Kaufmann.

\bibitem[\protect\BCAY{Randell, Cui, \BBA\ Cohn}{Randell
  et~al.}{1992}]{Randell:etal:kr92}
Randell, D.~A., Cui, Z., \BBA\ Cohn, A.~G. \BBOP1992\BBCP.
\newblock \BBOQ A spatial logic based on regions and connection\BBCQ\
\newblock In Swartout, B.\BBACOMMA\  \BBA\ Nebel, B.\BEDS, {\Bem Proceedings of
  the 3rd International Conference on Principles on Knowledge Representation
  and Reasoning (KR-92)}, \BPGS\ 165--176\ Cambridge, MA, USA. Morgan Kaufmann.

\bibitem[\protect\BCAY{Renz}{Renz}{1996}]{Renz:xjobb}
Renz, J. \BBOP1996\BBCP.
\newblock \BBOQ Qualitatives räumliches {S}chlie{\ss}en:
  {B}erechnungseigenschaften und effiziente {A}lgorithmen\BBCQ\
\newblock Master thesis report, Fakultät f\"ur Informatik, Universität Ulm.
\newblock Available from {\tt
  http://www.informatik.uni-freiburg.de/$\sim$sppraum}.

\bibitem[\protect\BCAY{Renz \BBA\ Nebel}{Renz \BBA\
  Nebel}{1997}]{Renz:Nebel:ijcai97}
Renz, J.\BBACOMMA\  \BBA\ Nebel, B. \BBOP1997\BBCP.
\newblock \BBOQ On the complexity of qualitative spatial reasoning: A maximal
  tractable fragment of the region connected calculus\BBCQ\
\newblock In {\Bem Proceedings of the 15th International Joint Conference on
  Artificial Intelligence (IJCAI-97)}\ Nagoya, Japan. Morgan Kaufmann.
\newblock To appear.

\bibitem[\protect\BCAY{Statman}{Statman}{1979}]{Statman:tcs79}
Statman, R. \BBOP1979\BBCP.
\newblock \BBOQ Intuitionistic logic is polynomial-space complete\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 9\/}(1), 67--72.

\bibitem[\protect\BCAY{van Beek}{van Beek}{1992}]{vanBeek:ai92}
van Beek, P. \BBOP1992\BBCP.
\newblock \BBOQ Reasoning about qualitative temporal information\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 58}, 297--326.

\end{thebibliography}

%\bibliographystyle{theapa}
%\bibliography{/home/chrba/bib/strings,/home/chrba/bib/abstracts,/home/chrba/bib/papers,/home/petej/bib/extrapapers,/home/chrba/bib/books,/home/chrba/bib/xref}

\end{document}




