\documentstyle[jair,amssymbols,twoside,11pt,apa,eepic]{article}

\input{defs}
\defnltrue
\input{envs}
\input{allendefs}
\input{misc}
\newcommand{\st}{\ |\ } % ``such that''

\jairheading{7}{1997}{25-45}{7/96}{7/97}
\ShortHeadings{Eight Maximal Tractable Subclasses of Allen's Algebra with Metric Time}
{Drakengren \& Jonsson}
\firstpageno{25}

\title{Eight Maximal Tractable Subclasses of\\
       Allen's Algebra with Metric Time}

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

\begin{document}

\maketitle

\begin{abstract}
  This paper
  combines two important directions of research in temporal resoning:
  that of finding maximal tractable subclasses of Allen's interval algebra,
  and that
  of reasoning with metric temporal information.
  Eight new maximal tractable subclasses of Allen's interval algebra
  are presented,
  some of them subsuming previously reported tractable algebras.
  The algebras allow for metric temporal constraints on interval
  starting or ending points, using the recent framework of {\em Horn DLRs}.
  Two of the algebras can express the notion of {\em sequentiality}
  between intervals, being the first such algebras
  admitting both qualitative and metric time.
\end{abstract}

\section{Introduction}

Reasoning about temporal knowledge abounds in artificial
intelligence applications and other areas, such as
planning \cite{Allen:TRandPlanning},
natural language understanding \cite{Song:Cohen:aaai88} and
molecular biology \cite{Benzer:pnas59,Golumbic:Shamir:jacm93}.
However, since even the restricted problem of reasoning
with pure qualitative time in Allen's interval algebra
\cite{Allen:cacm83} is NP-complete \cite{Vilain:etal:constrprop},
research has focused on identifying classes of problems
where reasoning is tractable
\cite{Drakengren:Jonsson:aaai96,Golumbic:Shamir:jacm93,Kautz:Ladkin:aaai91,Nebel:Burckert:jacm95,vanBeek:Cohen:ci90,vanBeek:ijcai89,vanBeek:aij92}.

Until recently, approaches have mostly been either
metric or qualitative, with a few exceptions
\cite{Kautz:Ladkin:aaai91,Meiri:aaai91,Gerevini:etal:sigart93}.
However, the approach of Jons\-son and Bäck\-ström
\shortcite{Jonsson:Backstrom:aaai96tcr}
(also developed independently by
Koubarakis, \citeyear{Koubarakis:cp96})
manages to unify almost every approach to tractable reasoning about metric
time, qualitative time and the integrated approaches in one framework,
that of {\em Horn disjunctive linear relations} (Horn-DLRs),
in which the reasoning problem can be solved in polynomial time.
Since its expressiveness in terms of qualitative information
subsumes that of the maximal tractable\footnote{
  That is, it is tractable, and no other tractable algebra strictly contains it.
}
ORD-Horn algebra \cite{Nebel:Burckert:jacm95},
it can be viewed as a maximal tractable subalgebra of Allen's
interval algebra, provided with metric temporal information.

First, this paper continues the work on finding maximal
tractable subalgebras of Allen's algebra started by Nebel and B\"{u}rckert
\shortcite{Nebel:Burckert:jacm95} and continued by Drakengren and Jonsson \shortcite{Drakengren:Jonsson:aaai96},
by identifying eight more maximal tractable subclasses
of Allen's algebra.
Second, we combine this with the work of Jonsson and B\"{a}ckstr\"{o}m \shortcite{Jonsson:Backstrom:aaai96tcr},
by providing the maximal algebras with metric temporal information in the form
of Horn DLRs, whose expressiveness subsumes that of the ORD-Horn algebra.
Further, the maximality result of these algebras settles the
question of maximality of some algebras in Drakengren and Jonsson \shortcite{Drakengren:Jonsson:aaai96},
since these are included in the new algebras presented here.
Two of the maximal algebras can express the notion
of {\em sequentiality} between intervals\footnote{
That is, they contain the relations $(\rllt)$, $(\rlgt)$,
$(\rllt\ \rlgt)$, $(\rlequ\ \rllt)$, $(\rlequ\ \rlgt)$,
$(\rlequ\ \rllt\ \rlgt)$, and the ``unrelated'' relation,
and can thus express that ``two intervals occur in sequence''.
}, important
for example in reasoning about action \cite{Sandewall:FF},
where actions are typically assumed to occur in sequence.
To our knowledge, these are the first
such algebras in the literature that are also provided with
metric temporal information.
By the fact that we can also relate starting or ending points by Horn DLRs,
we have a combination (with restrictions, of course)
of the expressiveness of the ORD-Horn algebra, and that of sequentiality.

The structure of the paper is as follows.
\refsec{allen} introduces Allen's interval algebra,
\refsec{dlrs} defines the concepts needed to integrate
qualitative and metric reasoning,
together with the satisfiability algorithm,
and \refsec{algebras} presents the new maximal tractable algebras, and
how to provide these with metric temporal information.
In \refsec{correctness} and \refsec{maximality},
we prove that the algorithm is correct
and that the algebras are maximal.
Finally,
\refsec{discussion} and \refsec{conclusions} discuss and conclude the paper.

\section{Allen's Interval Algebra}\labsec{allen}

\tab{1}
  {
    The thirteen basic relations.
    The endpoint relations $\xm<\xp$ and $\ym<\yp$ that are valid
    for all relations have been omitted.
  }
  {
    \begin{center}
    \begin{tabular}{|ll|c|l|}\hline
      \small Basic relation        &          & Example & Endpoints\\ 
\hline\hline
      \small $x$ before        $y$ & $\rllt$  & \stexttt{xxx\spv}    & $\xp<\ym$ 
\\ \cline{1-2}
      \small $y$ after         $x$ & $\rlgt$  & \stexttt{\spv yyy}   & \\ 
\hline
      \small $x$ meets         $y$ & $\rlm$   & \stexttt{xxxx\spiv}  & $\xp=\ym$ 
\\ \cline{1-2}
      \small $y$ met-by        $x$ & $\rlmi$  & \stexttt{\spiv yyyy} & \\ 
\hline
      \small $x$ overlaps      $y$ & $\rlo$   & \stexttt{xxxx\spii}  & $\xm<\ym<\xp$, \\ \cline{1-2}
      \small $y$ overl.-by $x$ & $\rloi$  & \stexttt{\spii yyyy} & $\xp<\yp$  
\\ \hline
      \small $x$ during        $y$ & $\rld$   & \stexttt{\spii xxx\spii} & $\xm>\ym$, \\ \cline{1-2}
      \small $y$ includes      $x$ & $\rldi$  & \stexttt{yyyyyyy}   & $\xp<\yp$ \\ 
\hline
      \small $x$ starts        $y$ & $\rls$   & \stexttt{xxx\spiv}  & $\xm=\ym$, 
\\ \cline{1-2}
      \small $y$ started by    $x$ & $\rlsi$  & \stexttt{yyyyyyy}   & $\xp<\yp$ \\ 
\hline
      \small $x$ finishes      $y$ & $\rlf$   & \stexttt{\spiv xxx} & $\xp=\yp$, 
\\ \cline{1-2}
      \small $y$ finished by   $x$ & $\rlfi$  & \stexttt{yyyyyyy}   & $\xm>\ym$ \\ 
\hline
      \small $x$ equals        $y$ & $\rlequ$ & \stexttt{xxxx}      & $\xm=\ym$, \\ 
                                   &          & \stexttt{yyyy}      & $\xp=\yp$ \\ 
\hline
    \end{tabular}
    \end{center}
  }

\noindent Allen's interval algebra \cite{Allen:cacm83}
is based on the notion of {\em relations between pairs of intervals}.
An interval $x$ is represented as a tuple $\tuple{\xm, \xp}$
of real numbers with $\xm<\xp$, denoting the left and right
endpoints of the interval, respectively,
and relations between intervals are composed as disjunctions
of {\em basic interval relations}, which are those in \reftb{1}.
Such disjunctions are represented as {\em sets} of basic relations,
but using a notation such that,
for example, the disjunction of the basic intervals $\rllt$, $\rlm$ and $\rlfi$
is written $(\rllt\ \rlm\ \rlfi)$.
Thus, we have that $(\rllt\ \rlfi)\subseteq(\rllt\ \rlm\ \rlfi)$.
Sometimes the disjunction of {\em all} basic relations
is written $\top$ and the empty relation is written $\bot$
(this is also used for relations between interval endpoints,
denoting ``always satisfiable'' and ``unsatisfiable'', respectively).
The algebra is provided with the operations of
{\em converse, intersection and composition} on intervals,
but we shall need only the converse operation explicitly.
The converse operation takes an interval relation $i$ to its converse $\inv{i}$,
obtained by inverting each basic relation in $i$,
i.e., exchanging $x$ and $y$ in the endpoint relations shown in \reftb{1}.

By the fact that there are thirteen basic relations,
we get $2^{13}=8192$
possible relations between intervals in the
full algebra. We denote the set of all interval relations by $\cA$.
Subclasses of the full algebra are obtained by considering subsets of $\cA$.
There are $2^{8192}\approx 10^{2466}$ such subclasses.
Classes that are closed under the operations of intersection,
converse and composition are said to be {\em algebras}.

Although there are several computational problems associated with
Allen's interval algebra, this paper focuses on the problem
of {\em satisfiability} ($\ISAT$) of a set of interval variables with relations
between them, i.e., deciding whether there exists an assignment
of intervals on the real line for the interval variables, such that all of 
the relations between the intervals are satisfied.
We define this as follows.

\definition{0.01}{$\ISAT(\cI)$}
  {
    Let $\cI$ be a set of interval relations.
    An instance of $\ISAT(\cI)$ is a labelled directed graph
    $S=\tuple{V,E}$, where the nodes in $V$ are interval variables
    and $E$ is a subset of $V\times\cI\times V$.
    A labelled edge $\tuple{u,r,v}\in E$ means that $u$
    and $v$ are related by $r$.
\condnl
    A function $M$ taking an interval variable $v$ to
    its interval rep\-re\-sen\-ta\-tion
    $M(v)=\tuple{x^-,x^+}$ with $x^-,x^+\in\tR$ and $x^-<x^+$,
    is said to be an {\em in\-ter\-pre\-ta\-tion} of $S$.
\condnl
    An instance $S=\tuple{V,E}$ is said to be {\em satisfiable}
    iff there exists an interpretation $M$
    such that for each $\tuple{u,r,v}\in E$,
    $M(u)r M(v)$ holds, i.e., the endpoint relations
    required by $r$ (see \reftb{1}) are satisfied by the assignments
    of $u$ and $v$.
    Then $M$ is said to be a {\em model} of $S$.
\condnl
    We refer to the {\em size} of an instance $S$
    as $|V|+|E|$.
  }

\noindent For $\cA$, we have the following result.

\proposition{1.01}
  {
    $\ISAT(\cA)$ is NP-complete.
  }
  {
    See Vilain et al.\ \shortcite{Vilain:etal:constrprop}.
  }

\section{Qualitative and Metric Time}\labsec{dlrs}

We first briefly recapitulate the Horn-DLR
formalism of Jonsson and Bäckström \shortcite{Jonsson:Backstrom:aaai96tcr}.

\definition{1a.0}{Linear relation, Disjunctive linear relation}
  {
    Let $X=\set{x_1,\ldots,x_n}$ be a set of real-valued variables, and
    $\alpha,\beta$ linear polynomials (polynomials of degree one) over $X$
    with rational coefficients.
    A {\em linear relation} over $X$ is a mathematical expression of the form
    $\alpha r \beta$, where $r\in\set{<,\leq,=,\not=,\geq,>}$.
    A {\em disjunctive linear relation} (DLR) over $X$ is
    a disjunction of one or more linear relations.
    A DLR is said to be {\em Horn} iff at most one of its disjuncts
    is not of the form $\alpha\not=\beta$.
\condnl
    The satisfiability problem for
    finite sets $H$ of Horn DLRs is denoted {\sc hornDLRsat}$(H)$,
    checking whether there exists an assignment $M$
    of variables in $X$ to real numbers such that all
    DLRs in $H$ are satisfied in $M$.
    Such an $M$ is said to be a {\em model} of $H$.
  }

\example{1a.01}
  {
    \[x+2y\leq 3z+42.3\]
    is a linear relation,
    \[(x+2y\leq 3z+42.3)\vee (x>\frac{3}{12})\]
    is a disjunctive linear relation, and
    \[(x+2y\leq 3z+42.3)\vee (x\not=\frac{3}{12})\]
    is a Horn disjunctive linear relation.
  }

\proposition{1a.1}
  {
    There is a polynomial-time algorithm for {\sc hornDLRsat}$(H)$.
  }
  {
    See Jonsson and Bäckström \shortcite{Jonsson:Backstrom:aaai96tcr}
    or Koubarakis \shortcite{Koubarakis:cp96}.
  }

\noindent In principle, the framework of DLRs makes it unnecessary
to distinguish between qualitative and metric information.
Nevertheless, when it comes to identifying tractable subclasses,
the distinction is still convenient.

The Horn-DLR approach subsumes almost all previously
known approaches to tractable metric and qualitative temporal reasoning,
e.g.\ \cite{Nebel:Burckert:jacm95,mk:densetime,dmp:tcn,Meiri:aaai91,Gerevini:etal:sigart93}.
It is worth mentioning that the maximal tractable algebras
found by Drakengren and Jonsson \shortcite{Drakengren:Jonsson:aaai96} cannot be expressed as Horn DLRs.

Although polynomial, the algorithm presented in Jonsson and Bäckström \shortcite{Jonsson:Backstrom:aaai96tcr}
is quite expensive (it relies on a linear-programming algorithm)
so when we have no need of specifying metric information,
the following well-known subclass of the set of Horn DLRs
will result in a lower-complexity algorithm.

\definition{1a.2a}{The point algebra}
  {
    The {\em point algebra} \cite{Vilain:aaai82}
    is the subclass of Horn DLRs consisting of the set of
    expressions $x R y$, where $x$ and $y$ are variables,
    and $R$ is one of the relations $<$, $\leq$, $=$, $\not=$, $\geq$ and $>$.
  }

\noindent
The satisfiability problem for this subclass is denoted {\sc PAsat}$(H)$,
for a set $H$ of point algebra formulae.

\proposition{1a.2}
  {
    {\sc PAsat}$(H)$ is solvable in linear time in the size of $H$.
  }
  {
    See Gerevini et al.\ \shortcite{Gerevini:etal:sigart93}
    (for practical purposes the algorithm of
    Delgrande and Gupta,~\citeyear{Delgrande:Gupta:aaai96},
    could be preferred).
  }

\noindent Next, we define the problem of interest in this paper ---
the interval satisfiability problem with metric temporal information.

\definition{1.8}{$\QISAT(\cI)$}
  {
    Let $\tuple{V,E}$ be an instance of $\ISAT(\cI)$
    and $H$ a finite set of DLRs over the set
    $\set{v^+,v^-\st v\in V}$ of variables,
    $v^-$ representing starting points and
    $v^+$ ending points of intervals $v$.
\condnl
    An instance of the problem of {\em interval satisfiability with
    metric information} for a set $\cI$ of interval relations,
    denoted $\QISAT(\cI)$, is a tuple $Q=\tuple{V,E,H}$.
\condnl
    An {\em in\-ter\-pre\-ta\-tion} $M$ for $Q$ is an interpretation for $\tuple{V,E}$.
    Since we now need to refer to starting and ending points
    of intervals, we extend the notation such that $M(v^-)$ obtains
    the starting point of the interval $M(v)$, and similarly for $M(v^+)$.
\condnl
    An instance $Q$ is said to be {\em satisfiable} iff
    there exists a model $M$ of $\tuple{V,E}$ such that 
    the DLRs in $H$ are satisfied, with values for all $v^-$ and $v^+$
    by $M(v^-)$ and $M(v^+)$, respectively.
  }

\noindent Since every Allen interval relation can be expressed as a DLR
(but not necessarily as a Horn DLR), we could instead have formulated
the problem as a pure satisfiability problem of a set of DLRs,
but since we are interested in the particular structure imposed on the
problem by interval relations specifically we prefer this formulation.

Several concepts are needed in order to present the
{\em starting and ending point algebras}, for which we shall provide
polynomial-time algorithms.
The curious reader might temporarily jump to \refsec{algebras} for the explicit
presentation of the algebras which will be proved to be
starting or ending points algebras.

The following definitions are needed to transfer
information from interval relations to point relations.

\definition{1.603}{$\sprel(r)$, $\eprel(r)$, $\sprel^+(r)$, $\eprel^-(r)$}
  {
    Take the relation $r\in\cA$, let $u$ and $v$ be interval
    variables, and consider the instance $S$ of $\ISAT(\set{r})$
    which relates $u$ and $v$ with the relation $r$ only.
    Define the relation $\sprel(r)$ on real numbers to be
    the symbol for the implied relation between the
    starting points of $u$ and $v$.
    That is, for basic relations define

    \[
    \begin{array}{rcl}
      \sprel(\rlequ) & = & \mbox{``$=$''}\\
      \sprel(\rllt)  & = & \mbox{``$<$''}\\  
      \sprel(\rld)   & = & \mbox{``$>$''}\\
      \sprel(\rlo)   & = & \mbox{``$<$''}\\
      \sprel(\rlm)   & = & \mbox{``$<$''}\\
      \sprel(\rls)   & = & \mbox{``$=$''}\\
      \sprel(\rlf)   & = & \mbox{``$>$''}\\
      \sprel(\inv{r})& = & (\sprel(r))^{-1},
    \end{array}
    \]
    and for disjunctions $\sprel(r)$ is the relation symbol
    corresponding to $\bigvee_{b\in r}\sprel(b)$.
    For example, $\sprel((\rllt\ \rlgt))=\mbox{``$\not=$''}$.
    Symmetrically, we define $\bx{\eprel(r)}$ to be the implied relation between
    ending points given $r$.
    Note that $\sprel(r)$ and $\eprel(r)$ have to be either of
    $<$, $\leq$, $=$, $\geq$, $>$, $\not=$, $\top$ or $\bot$.
\condnl
    Further, we define specialisations of these, by
    $\bx{\sprel^+(r)}=\bx{\sprel(r\cap\rleqffi)}$
    and
    $\bx{\eprel^-(r)}=\bx{\eprel(r\cap\rleqssi)}$,
    i.e., the implied relations on starting (ending) points by $r$, given
    that the ending (starting) points are known to be equal.
}

\definition{1.602}{Explicit starting (ending) point relations}
  {
    Let $\cI\subseteq\cA$, $Q=\tuple{V,E,H}$
    an instance of $\QISAT(\cI)$, and construct the instance
    $Q'=\tuple{V,E,H'}$ of $\QISAT(\cI)$
    by setting
    \[H'=H\cup\set{u^-\sprel(r)v^-\st \tuple{u,r,v}\in E}.\]
    Then $Q'$ is said to be obtained from $Q$
    by {\em making starting point relations explicit}.
    We denote this $Q'$ by $\expl^-(Q)$.
\condnl
    Symmetrically, using $\eprel$ and ending points
    instead of $\sprel$ and starting points,
    $Q'$ is said to be obtained from $Q$ by
    {\em making ending points explicit},
    denoted $\expl^+(Q)$.
  }

\noindent It is easy to see that only point algebra formulae are added to $H$.

Transferring information from interval relations to point relations
does not change satisfiability, as expected:

\proposition{1.604}
  {    
    Let $\cI\subseteq\cA$ and $Q$ an instance of $\QISAT(\cI)$.
    Then $Q$ is satisfiable iff $\expl^-(Q)$
    is satisfiable iff $\expl^+(Q)$ is satisfiable.
  }
  {
    By the fact that the added starting and ending point
    relations are already guaranteed to hold in any model of $Q$.
  }

\noindent We jump ahead by presenting a satisfiability
algorithm (\refalg{2}) and
briefly discuss the intuition behind it
in order to indicate what kind of algebras it works for.
This will hopefully make it easier to appreciate \refdf{1.6}.

\algorithm{2}{$\QSISAT(\cI)$}
  {
       & \INPUT Instance $Q=\tuple{V,E,H}$\\
    \\
    1  & $Q'=\tuple{V,E,H'}\leftarrow\expl^-(Q)$\\
    2  & \IF not {\sc hornDLRsat}$(H')$ \THEN\\
    3  & \algind \reject\\
    4  & $K\leftarrow\emptyset$\\
    5  & \FOR each $\tuple{u,r,v}\in E$\\
    6  & \algind\IF not {\sc hornDLRsat}$(H'\cup\set{u^-\not=v^-})$ \THEN\\
    7  & \algind\algind $K\leftarrow K\cup\set{u^-=v^-}$\\
    8  & \algind\ELSE\\
    9  & \algind\algind $K\leftarrow K\cup\set{u^-\not=v^-}$\\
    10 & \algind\ENDIF\\
    11 & \ENDFOR\\
    12 & $P\leftarrow\set{u^+\eprel^-(r) v^+\st\tuple{u,r,v}\in E\wedge u^-=v^-\in H'\cup K}$\\
    13 & \IF not {\sc PAsat}($P$) \THEN\\
    14 & \algind\reject\\
    15 & \accept
  }
First assume that $H$ only contains Horn DLRs, which only relate starting points
of intervals.
Line $1$ makes the interval relations explicit as starting point relations
and line $2$ checks satisfiability of the resulting set of starting point
relations.
Lines $4$ to $11$ collect in $K$ the relations $u^-=v^-$, such that
in any model these starting points have to be equal.
In addition, $K$ forces all starting points to be distinct,
that are not forced to be equal.
It is clear that the equality formulae in $K$ do not affect satisfiability.
However, it is less clear that the disequality formulae in $K$ cannot
make the instance $Q''=\tuple{V,E,H'\cup K}$ unsatisfiable.
This fact indeed follows from a property of Horn DLRs, which is proved in 
\refth{1.2}.
At line $12$, we know that there are no two models for $Q''$,
where for some $u,v\in V$, $u^-=v^-$ in one model, and $u^-\not=v^-$
in the other model. This is the intuition behind \refdf{1.601}.
Now, line $13$ checks for satisfiability of the ending points
of those intervals whose starting points have to be equal in any model.
If the algorithm rejects at line $14$, then the instance is obviously not satisfiable.
Otherwise we need a condition on the algebra $\cI$, corresponding to
\refdf{1.6}, in order to guarantee satisfiability.

The formal machinery follows.

\definition{1.601}{Starting (ending) point definite}
  {
    Let $\cI\subseteq\cA$, and
    $Q=\tuple{V,E,H}$ an instance of $\QISAT(\cI)$.
    The instance $Q'=\tuple{V,E,H\cup H'}$ of $\QISAT(\cI)$ is said to be
    {\em starting point definite wrt.\ $Q$} iff
    there exists a function $f:E\rightarrow\set{=,\not=}$
    such that
    $H'=\set{u^-f(e)v^-\st\tuple{u,r,v}\in E}$.
    We denote this relation by $\sep^-(Q,Q')$.
    This means that for each relation, either the starting points
    of related intervals are forced to be equal in all models,
    or they are forced to be distinct in all models.
    If for some $Q$ we have $\sep^-(Q,Q')$, then
    $Q'$ is said to be {\em starting point definite}.
\condnl
    Similarly, by exchanging starting and ending points,
    we get that $Q'$ is {\em ending point definite wrt.\ $Q$},
    denoted $\sep^+(Q,Q')$.
  }

\noindent Line $13$ of \refalg{2} checks the following, as we shall see.

\definition{1.61}{Locally satisfiable for starting (ending) points}
  {
    Let 
    $Q=\tuple{V,E,H}$ be a starting point definite
    instance of $\QISAT(\cI)$ for some $\cI\subseteq\cA$,
    and construct $Q'=\tuple{V,E',H}$ such that
    $E'=\set{\tuple{u,r,v}\in E\st u^-=v^-\in H}$,
    i.e.\ by considering only relations which
    force the starting points to be equal.
    Now $Q$ is said to be {\em locally satisfiable for starting points}
    iff $Q'$ is satisfiable. A model satisfying $Q'$ is
    said to {\em locally satisfy $Q$ for starting points}.
\condnl
    Similarly, exchanging starting and ending points,
    $Q$ is said to be {\em locally satisfiable
    for ending points} iff $Q'$ is satisfiable, and a model satisfying $Q'$
    is said to {\em locally satisfy $Q$ for ending points}.   
}

\noindent We now define the algebra for which \refalg{2} solves satisfiability.

\definition{1.6}{Starting (ending) point algebra}    
  {
    A subalgebra $\cI\subseteq\cA$ is said to be a {\em starting point algebra}
    iff for any instance $Q=\tuple{V,E,H}$ of $\QISAT(\cI)$, the
    following holds:
    for any $T=\tuple{V,E,H'}$ such that $\sep^-(\expl^-(Q),T)$,
    if $T$ is locally satisfiable for starting points,
    then $T$ is satisfiable.
\condnl
    Symmetrically, exchanging ending points and starting points,
    we obtain an {\em ending point algebra}.
  }

\noindent The satisfiability problems for these algebras are defined as follows.

\definition{1.81}{$\QSISAT(\cI)$, $\QEISAT(\cI)$}
  {
    Let $\cI$ be a starting point algebra.
    The {\em satisfiability problem for starting point algebras with
    metric information}
    is the set of instances $\tuple{V,E,H}$ of $\QISAT(\cI)$
    where the DLRs of $H$ are restricted in two ways:
    first, $H$ may only contain Horn DLRs and second,
    $H$ may not contain any variables $v^+$, where $v\in V$,
    i.e., it may only relate starting points of intervals.
\condnl
    Symmetrically, by exchanging starting and ending points,
    we get the {\em satisfiability problem for ending point algebras with
    metric information}.
  }

\section{Tractable Algebras}\labsec{algebras}

We now present the algebras which are starting (ending)
point algebras.

\definition{1.65}{The subclasses $S(b)$ and $E(b)$}
  {
    Set
    $r_s=(\rlgt\ \rld\ \rloi\ \rlmi\ \rlf)$,
    and
    $r_e=(\rllt\ \rld\ \rlo\ \rlm\ \rls)$.
    Note that $r_s$ contains all basic relations $b$ such that
    whenever $I b J$ for interval variables $I$, $J$,
    $I^->J^-$ has to hold in any model
    and sym\-me\-tri\-cal\-ly, 
    $r_e$ is equivalent to $I^+<J^+$ holding in any model.
\condnl
    First, for $b\in\set{\rlgt, \rld, \rloi}$,
    define $S(b)$ to be the set of relations $r$,
    such that either of the following holds:
    \eqsp{rcccl}
      {
        ( b\ \inv{b} ) & \subseteq & r\\
        ( b )          & \subseteq & r & \subseteq & r_s\cup\rleqssi\\
        ( \inv{b} )    & \subseteq & r & \subseteq & \inv{r_s}\cup\rleqssi\\
                       &           & r & \subseteq & \rleqssi.
      }
    Then, by switching starting and ending points of intervals,
    for $b\in\set{\rllt, \rld, \rlo}$, $E(b)$ is defined
    to be the set of relations $r$, such that
    either of the following holds:
    \eqsp{rcccl}
      {
        ( b\ \inv{b} ) & \subseteq & r\\
        ( b )          & \subseteq & r & \subseteq & r_e\cup\rleqffi\\
        ( \inv{b} )    & \subseteq & r & \subseteq & \inv{r_e}\cup\rleqffi\\
                       &           & r & \subseteq & \rleqffi.
      }
  \noindent
  }

\definition{1.64}{The subclasses $S^*$ and $E^*$}
  {
    Let $r_s$ and $r_e$ be as in \refdf{1.65},
    and define
    $S^*$ to be the set of relations $r$,
    such that either of the following holds:
    \eqsp{rcccl}
      {
        \rleqffi        & \subseteq & r\\
        (\rlf\ \rlfi)   & \subseteq & r & \subseteq & r_s\cup\inv{r_s}\\
        (\rlequ\ \rlf)  & \subseteq & r & \subseteq & r_s\cup\rleqssi\\
        (\rlequ\ \rlfi) & \subseteq & r & \subseteq & \inv{r_s}\cup\rleqssi\\
        (\rlf)          & \subseteq & r & \subseteq & r_s\\
        (\rlfi)         & \subseteq & r & \subseteq & \inv{r_s}\\
        (\rlequ)        & \subseteq & r & \subseteq & \rleqssi\\
                        &           & r & =         & \bot
      }
   Symmetrically, replacing $\rlf$ by $\rls$ (and their inverses),
   $\rleqssi$ by $\rleqffi$, 
   and $r_s$ by $r_e$, we get the subclass $E^*$.
}

\noindent Files containing the algebras are supplied as an on-line appendix
to this article.

It is easy to see that the algebras are all considerably larger
than, for example, the ORD-Horn algebra, which contains $868$ elements.

\condproposition{1.910}
  {
    The six algebras $S(b)$ and $E(b)$ contain $2312$ elements
    each and $S^*$ and $E^*$ contain $1445$ elements each.
  }
  {
    A straightforward combinatorial exercise according to the definitions.
  }

\noindent We also see that the $S(b)$ and $E(b)$ algebras each 
contain five basic relations, and that $S^*$ and $E^*$ contain
three basic relations each.
A subsumption result and a nonsubsumption result follow.

\condproposition{1.9101}
  {
    The twelve algebras presented by Drakengren and Jonsson \shortcite{Drakengren:Jonsson:aaai96}, which were
    not classified as maximal tractable, are each included
    in one of the algebras $S(b)$ and $E(b)$.
  }
  {
    By simply checking inclusion from the definitions.
  }

\proposition{1.9102}
  {
    In all of the algebras $S(b)$, $E(b)$, $S^*$ and $E^*$,
    there are relations which are not expressible by Horn DLRs alone.
  }
  {
    It is easily verified that the point relations induced by the
    Allen relations $(\rllt\ \rlgt)$, $(\rld\ \rldi)$, $(\rlo\ \rloi)$,
    $(\rlgt \rlfi)$ and $(\rllt\ \rls)$ are not Horn DLRs.
  }

\noindent
It was observed by Drakengren and Jonsson \shortcite{Drakengren:Jonsson:aaai96}
that the ORD-Horn algebra cannot express the notion
of {\em sequentiality}, and thus since it is maximal tractable,
we cannot add the relation $( \rllt\ \rlgt )$ to it without losing tractability.
However, we can obtain a weaker yet useful result by the following observation:
We know from the results of Jonsson and Bäckström
\shortcite{Jonsson:Backstrom:aaai96tcr} that the expressivity
of Horn DLRs subsumes that of the ORD-Horn algebra,
by expressing the ORD-Horn relations
as disjunctions of point relations in the starting and ending points
of the intervals.
Thus, since the satisfiability problem for starting point
algebras (and ending point algebras, which follows by symmetry)
allow arbitrary Horn DLRs relating starting points, we can convert
any network expressed in the ORD-Horn algebra
into an equivalent instance of $\QSISAT(\cI)$ for some
of the tractable subclasses above, where only starting
points of intervals are related.
The additional expressivity of the starting point algebras
can then be used to express e.g.\ sequentiality
(using one of the algebras $S(\rlgt)$ or $E(\rllt)$) or
other relations between intervals.

Now it is time to verify that the presented algebras
are indeed starting and ending point algebras, respectively.
A few auxiliary definitions and results are needed.

\definition{1.70a}{Sign function}
  {
    For $x\in\tR$, let $\sgn(x)\in\set{-1,0,1}$ be the {\em sign} of $x$,
    that is, if $x<0$, then $\sgn(x)=-1$, if $x=0$ then $\sgn(x)=0$,
    and if $x>0$, then $\sgn(x)=1$.
  }

\lemma{1.70}
  {
    Let $Q=\tuple{V,E,H}$ be a starting point definite instance
    of $\QSISAT(\cI)$,
    which is locally satisfiable for starting points by some model $M$,
    and let $M'$ be an interpretation for $Q$ such that
    \begin{itemize}
      \item $\forall v\in V.M(v^-)=M'(v^-)$
      \item $\forall u,v\in V.M(u^-)=M(v^-)\rightarrow$\\
            $\ind\ind \sgn(M(u^+)-M(v^+))=\sgn(M'(u^+)-M'(v^+))$,
    \end{itemize}
    which means that $M'$ may not differ from $M$
    in the interpretation of starting points,
    and for ending points, any change is allowed, as long
    as their relative order for relations
    which have the same interpretations of starting points
    is the same.
    Then $M'$ also locally satisfies $Q$ for starting points.
  }
  {
    Apart from checking the DLRs in $H$,
    local satisfiability for starting points checks only
    relations where the intervals they relate are forced to
    have the same starting point.
    Since $H$ does not relate ending points of intervals,
    the only thing that affects satisfiability of these relations
    is the relative order of ending points, given a fixed starting point.
    Since this order is the same, and $M$ and $M'$ coincide
    on starting points, the result follows.
  }

\lemma{1.71}
  {
    Let $Q=\tuple{V,E,H}$ be a starting point definite instance of $\QSISAT(\cI)$,
    where for no $\tuple{u,r,v}\in E$,
    $r\cap\rleqssi\not=\emptyset$ and $r-\rleqssi\not=\emptyset$.
    Then $Q$ is satisfied by the model $M$ iff
    $M$ locally satisfies $Q$ for starting points and
    $M$ satisfies $\tuple{V,E'}$, for
    $E'=\set{\tuple{u,r,v}\in E\st r\cap\rleqssi=\emptyset}$.
  }
  {
    \Rcase Assuming that $M$ satisfies $Q$, the latter condition
    is a direct consequence of the definitions.

    \Lcase By the restriction on $Q$, satisfiability of every relation $r$
    is checked by the two conditions together,
    and the satisfiability of $H$ is included in
    the local satisfiability condition.
    Thus $Q$ is satisfiable.
  }

\lemma{1.6010}
  {
    Let $Q=\tuple{V,E,H}$ be an instance of $\QISAT(\cI)$,
    and let $T=\tuple{V,E,H'}$ be such that $\sep^-(Q,T)$.
    Construct $T'=\tuple{V,E',H'}$ by setting
    \[\begin{array}{rcl}
        E' & = & \set{\tuple{u,r\cap\rleqssi,v}\st v_1^-=v_2^-\in H}\cup\\
           &   & \set{\tuple{u,r-\rleqssi,v}\st v_1^-\not=v_2^-\in H}
      \end{array}\]
    Now $T'$ is satisfiable iff $T$ is.
    The analogous result holds for ending points,
    when references to starting points are changed to ending points,
    and $\rleqssi$ is changed to $\rleqffi$.
  }
  {
    Directly from the definitions.
    The restrictions imposed on the qualitative relations are already
    guaranteed to hold in any model, by the restrictions on $H'$.
    Note that $E'$ is well-defined since $\sep$ adds to $H$ either
    equality or inequality for all interval starting points.

    The property of ending points follows by symmetry.
  }

\definition{1.69a}{Absolute value}
  {
    For $x\in\tR$, denote by $\abs(x)$ the
    absolute value of $x$, i.e.\ $x\cdot\sgn(x)$.
  }

\noindent The main results follow.

\theorem{1.69}
  {
    The algebras $S(b)$ are starting point algebras,
    and the algebras $E(b)$ are ending point algebras.
  }
  {
    Let $Q=\tuple{V,E,H}$ be an instance of $\QSISAT(S(b))$,
    and let $T=\tuple{V,E,H'}$ with $\sep^-(\expl^-(Q),T)$.
    By \reflm{1.6010}, we can assume that for every
    $\tuple{u,r,v}\in E$, either $r\subseteq\rleqssi$ or $r\cap\rleqssi=\emptyset$,
    since $T$ is starting point definite.
    Thus, the only relations $r$ which are left are those satisfying
    \eqsp{rcccl}
      {
        ( b\ \inv{b} ) & \subseteq & r & \subseteq & r_s\cup\inv{r_s}\\
        ( b )          & \subseteq & r & \subseteq & r_s\\
        ( \inv{b} )    & \subseteq & r & \subseteq & \inv{r_s}\\
                       &           & r & \subseteq & \rleqssi.
      }
    So, suppose that $T$ is locally satisfied for starting points by a model $M$.
    Since $T$ has explicit starting points,
    all relations from line $4$ are satisfied in $M$.
    Also, since $M$ imposes a certain order on starting points of intervals,
    we know that without loss of generality,
    relations $r$ on line $1$ can be replaced by
    either $r\cap r_s$ or $r\cap\inv{r_s}$, since
    $r_s$ and $\inv{r_s}$ impose disjoint orderings on starting points.
    Thus, without loss of generality,
    we take $T$ only to contain relations from
    lines $2$ and $4$, inverting relations
    containing line $3$ relations while changing their direction.
    If we could modify $M$ into an interpretation $M'$
    such that the conditions of \reflm{1.70}
    are satisfied, and the relations of line $2$
    and their inverses are satisfied, then by \reflm{1.71},
    since these relations do not overlap
    with $\rleqssi$, $M'$ would be a model of $T$, and the result would follow.
    Indeed, we shall satisfy line $2$ relations with
    the basic relation $b$ on every arc.

    A few auxiliary definitions are needed for the construction.
    Define $\mt{MD}(M)$ to be the least nonzero member of the set
    $\set{\abs(M(u^-)-M(v^-))\st u,v\in V}$, i.e., the least nonzero
    distance between starting points in $M$.
    Given a $w\in V$, let $EP(w)$ be the set
    \[\set{v\in V\st M(v^-)=M(w^-)},\]
    i.e., the set of intervals whose order of ending points has to be
    fixed, to maintain local satisfiability, by \reflm{1.70}.
    Note that $EP(w)$ is uniquely determined by $M(w^-)$.
    Also, for a given $w$, let $n_w=|\set{M(v^+)\st v\in EP(w)}|$
    (the number of distinct ending points in $M$ within
    $w$'s ``group''), and
    $f_w : EP(w)\rightarrow\set{k\in\tN\st k<n_w}$ the function uniquely
    determined by the ordering on ending points of $EP(w)$ in $M$, such that
    for every $u,v\in EP(w)$,
    \[\sgn(M(u^+)-M(v^+))=\sgn(f_w(u)-f_w(v)).\]
    Note that for every $u,v\in EP(w)$, $f_u=f_v$.

    Let $s=|\set{M(v^-)\st v\in V}|$,
    i.e., the number of distinct starting points in $M$.
    Corresponding to $f_w$, define $i:V\rightarrow\set{k\in\tN\st k<s}$ to be
    the uniquely determined function such that for every $u,v\in V$,
    \[\sgn(M(u^-)-M(v^-))=\sgn(i(u)-i(w)).\]
    We construct the interpretation $M'$ as follows, depending on $b$,
    and afterwards prove that it is a model of $T$.
    First, set $\epsilon=\mt{MD}(M)$,
    and for all $v\in V$, set $M'(v^-)=M(v^-)$.

\begin{figure}[t]
\begin{center}
\input{construction.tex}
\caption{
  An example of the construction for the case when 
  $b$ is $\rlgt$ in the proof of 
  \protect\refth{1.69}.
}
\end{center}
\end{figure}

    \begin{itemize}
      \item Suppose that $b$ is $\rlgt$.
            For every $v\in V$, set
            \[M'(v^+)=M(v^-)+\frac{\epsilon}{4}(1+\frac{f_v(v)}{n_v}).\]

      \item Suppose that $b$ is $\rld$.
            For every $v\in V$, set
            \[M'(v^+)=M(v^-)+1+2\epsilon(s-i(v)-1)+\frac{\epsilon}{2}(\frac{f_v(v)}{n_v}-1).\]

      \item Suppose that $b$ is $\rloi$.
            First let $w\in V$ be such that $i(w)=s-1$, i.e., having the largest ending point,
            set $M'(w^+)=M(w^-)+1$.
            For every $v\in V$, set 
            \[M'(v^+)=M(w^-)+\frac{i(v)+1}{s}+\frac{1}{s}(\frac{f_v(v)}{n_v}-\frac{1}{2}).\]
            
    \end{itemize}

    Now, by construction, the models satisfy $b$ on every arc.
    Furthermore, the order of ending points within each $EP(v)$ is retained,
    and the orderings on starting points are identical in $M$ and $M'$.
    Thus $M'$ locally satisfies $T$ for starting points by \reflm{1.70},
    and by \reflm{1.71}, $M'$ is a model of $T$.

    The proof for $E(b)$ is symmetrical.
  }

\noindent Fortunately, the next proof is much more convenient.

\theorem{1.77}
  {
    The algebra $S^*$ is a starting point algebra,
    and $E^*$ is an ending point algebra.
  }
  {
    We prove only the $S^*$ case, since the $E^*$ case is symmetrical.

    Precisely as in the proof of \refth{1.69}, we obtain an instance $T$ labelled only
    by relations $r$ satisfying
    \eqsp{rcccl}
      {
        (\rlf\ \rlfi)   & \subseteq & r & \subseteq & r_s\cup\inv{r_s}\\
        (\rlf)          & \subseteq & r & \subseteq & r_s\\
        (\rlfi)         & \subseteq & r & \subseteq & \inv{r_s}\\
        (\rlequ)        & \subseteq & r & \subseteq & \rleqssi\\
                        &           & r & =         & \bot.
      }
    First assume that $T$ is locally satisfied for starting points by some model $M$.
    Since $M$ imposes a certain order on starting points of intervals,
    we know that relations $r$ on line $1$ now can be assumed
    to be either $r\cap r_s$ or $r\cap\inv{r_s}$, since relations
    in $r_s$ and $\inv{r_s}$ impose disjoint orderings
    on starting points, as in the proof of \refth{1.69}.
    Thus, without loss of generality,
    we take $T$ to contain only relations from lines $2$ and $4$,
    inverting line $3$ relations while changing their direction
    (relations from line $5$ make every instance unsatisfiable).
    We shall show that $T$ is always satisfiable by constructing
    a model $M'$ of $T$.
    First set $M'(v^-)=M(v^-)$ for every $v\in V$.
    Let $x$ be maximal such that $x=M(v^-)$,
    i.e., $x$ is the largest starting point in $M$.
    Then set $M'(v^+)=x+1$ for every $v\in V$.
    Obviously, for $u,v\in V$, whenever
    $M'(u^-)>M'(v^-)$, then $u(\rlf)v$ is satisfied in $M'$.
    For line $4$ relations $r$, when $u r v$, it has to hold
    that $M'(u^-)=M'(v^-)$, and thus by construction $M'(u^+)=M'(v^+)$,
    and $r$ is satisfied. Thus $M'$ is a model of $T$
    and the result follows.
  }
\noindent It remains to show that \refalg{2} correctly solves
satisfiability for starting and ending point algebras.

\section{Correctness of the Algorithm}\labsec{correctness}

Several concepts are needed for the correctness proof.

\definition{1.001}{Convex combination, Convex}
  {
    Given $x,y\in\tR^n$, a {\em convex combination}
    of $x$ and $y$ is any $z\in\tR^n$ of the form
    $\theta x+(1-\theta)y$, where $0\leq\theta\leq 1$.

    A set $S\subseteq\tR^n$ is said to be {\em convex}
    iff any convex combination of elements in $S$
    is already in $S$.
  }

\definition{1.0011}{Hyperplane}
  {
    A {\em hyperplane} in $\tR^n$ is a non-empty set defined as
    \[\set{x\in\tR^n\st\alpha(x)=b},\]
    for a linear polynomial $\alpha$ in $x_1,\ldots,x_n$, and $b\in\tR$.
  }

\definition{1.002}{Almost convex}
  {
    A set $S\subseteq\tR^n$ is said to be {\em almost convex}
    if for any $x,y\in S$, at most finitely many of the
    convex combinations of $x$ and $y$ are not in $S$.
  }

\example{1.0020}
  {
    The set
    \[S=\tR^3-\set{(x,y,z)\st x,y,z\in\tZ}\]
    is almost convex.
  }

\proposition{1.0021}
  {
    Any intersection of finitely many almost convex sets is almost convex.
  }
  {
    Let $S_1,\ldots,S_k$ be almost convex sets
    and let $S=S_1\cap\ldots\cap S_k$.
    Take $x,y\in S$. Then $x,y\in S_i$ for every $1\leq i\leq k$.
    Thus finitely many of the convex combinations of
    $x$ and $y$ are not in $S_i$.
    But since we intersect only a finite number of sets,
    only finitely many convex combinations are excluded
    from $S$, and the result follows.
  }

\noindent The following is a generalisation of Lemma $13$ of
Jonsson and Bäckström \shortcite{Jonsson:Backstrom:aaai96tcr}
(which is a simplified version of the proof by
\mbox{Lassez and McAloon,~\citeyear{Lassez:McAloon:jsc92}}),
from convex to almost convex sets.

\lemma{1.1.1}
  {
    Let $S\subseteq\tR^n$ be an almost convex set,
    and let $H_1,\ldots,H_k$ be hyperplanes.
    If $S\subseteq\bigcup_{i=1}^k H_i$, then there exists a $j$,
    $1\leq j\leq k$ such that $S\subseteq H_j$.
  }
  {
    Induction on $k$, letting $\cH_k=\bigcup_{i=1}^k H_i$.
    For $k=1$, the result is immediate, since $\cH_1=H_1$.
    Assuming that the result holds for $k$, we wish to show that if
    $S\subseteq\cH_{k+1}$, then there exists a $j$,
    $1\leq j\leq k+1$ such that $S\subseteq H_j$.
    So, suppose $S\subseteq\cH_{k+1}$, i.e., that
    $S\subseteq\cH_k\cup H_{k+1}$.
    If $S\subseteq\cH_k$, then the result follows by induction.
    Also if $S\subseteq H_{k+1}$, or if one of $\cH_k$
    or $H_{k+1}$ is included in the other, the result follows.
    Thus, suppose that $x,y\in S$, $x\in\cH_k$, $y\in H_{k+1}$, satisfying
    $x\not\in H_{k+1}$ and $y\not\in\cH_k$, which is the remaining case.
    
    Consider the line segment $L$ adjoining $x$ and $y$, which
    is the convex combinations of $x$ and $y$.
    Every hyperplane either contains $L$ or intersects $L$ in at most one point.
    If some $H_i$ contains $L$, then $x,y\in H_i$, violating the choice of $x$ and $y$.
    Thus $L$ is intersected by hyperplanes $H_i$ in at most finitely many points,
    and those are the only members of $L$ which can be in $\cH_{k+1}$.
    Since $S$ is almost convex, there are infinitely many points of $L$
    which are in $S$ and are not members of any hyperplane $H_i$,
    contradicting that this remaining case could hold.
    The result follows.
  }

\noindent One may note that this result holds even if $S$ satisfies the
weaker property of containing infinitely many convex combinations
of each pair of elements, but then the proof of \refpr{1.0021}
would not go through.

\lemma{1.0}
  {
    Let $\gamma$ be a satisfiable Horn DLR, and let
    \[S(\gamma)=\set{x\in\tR^n\st\gamma\mbox{\ satisfied by\ }x}\]
    be the set of all solutions to $\gamma$.
    Then $S(\gamma)$ is almost convex.
  }
  {
    By the definition of a Horn DLR,
    for some convex set $C$ and hyperplanes $H_i$, we have
    \[S(\gamma)=C\cup\bigcup_{i=1}^k\overline{H_i}=C\cup\overline{\bigcap_{i=1}^k H_i}.\]
    Take $x,y\in S(\gamma)$.
    If $x,y\in C$, then every convex combination of $x$ and $y$
    is in $S(\gamma)$ by the convexity of $C$.
    If $y\not\in C$ (and $x$ is either in $C$ or not),
    then $y\in\overline{H_l}$ for some $l$.
    Let $L$ be the line segment adjoining $x$ and $y$.
    The hyperplane $H_l$ either contains $L$
    or intersects $L$ in at most one point.
    It cannot contain $L$, since $y\not\in H_l$; thus $H_l$
    intersects $L$ in at most one point, and the remaining
    points of $L$ are members of $\overline{H_l}$,
    and thus are members of $S(\gamma)$.
  }

\lemma{1.1}
  {
    Let $H$ be a satisfiable set of Horn DLRs, and let
    \[S(H)=\set{x\in\tR^n\st\mbox{every\ }\gamma\in H\mbox{\ is satisfied by\ }x}\]
    be the set of all solutions to $H$.
    Then $S(H)$ is almost convex.
  }
  {
    Directly from \reflm{1.0} and \refpr{1.0021}.
  }

\noindent The following is the key result for obtaining correctness
of the algorithm.

\theorem{1.2}
  {
    Let $H$ be a satisfiable set of Horn DLRs,
    and let $x_1,x_2,\ldots,x_n$ be the variables used in $H$.
    Also define the set $\Gamma$ of Horn DLRs by
    \[\Gamma=\set{x_i\not=x_j\st\set{x_i\not=x_j}\cup H\mbox{\ is satisfiable}}.\]
    Then $H\cup\Gamma$ is satisfiable.
  }
  {
    Suppose that $H\cup\Gamma$ is not satisfiable, although $H$
    is satisfiable.
    Let $S$ be the set of solutions of $H$, as defined in \reflm{1.1}.
    By definition, the set of solutions to a 
    formula $x_i\not=x_j\in\Gamma$ is a complement of some hyperplane $H_{ij}$.
    Thus, the set of solutions to $H\cup\Gamma$ is
    $S-\bigcup_{i,j} H_{ij}=\emptyset$,
    equivalent to
    $S\subseteq\bigcup_{i,j} H_{i,j}$.
    By \reflm{1.1}, $S$ is almost convex, and by \reflm{1.1.1},
    $S\subseteq H_{kl}$ for some hyperplane $H_{kl}$.
    But then $S\cap H_{kl}=\emptyset$, contrary to our assumption,
    and the result follows.
  }

\noindent Thus, it is enough to check the formulae in $\Gamma$ {\em separately} for satisfiability.
The correctness proof of the algorithm follows.

\condtheorem{1.9}
  {
    \refalg{2} correctly solves satisfiability for starting point algebras.
    Symmetrically, by exchanging starting and ending points of \refalg{2},
    it correctly solves satisfiability for ending point algebras.
  }
  {
    Suppose that $Q$ is satisfiable.
    Then after line $1$, $Q'$ is satisfiable, by \refpr{1.604}.
    Thus we cannot get reject at line $3$, since $H'$ has
    to be satisfied for $Q'$ to be satisfiable.
    Consider the value of $K$ at line $12$,
    and set $K'=\set{u^-\not=v^-\st u^-\not=v^-\in K}$.
    By the construction of $K$ in lines $4-11$,
    all models of $Q'$ have to satisfy the formulae of $K-K'$.
    Further, using \refth{1.2} and the construction of $K$,
    $H'\cup K'$ is also satisfiable, and thus $H'\cup K$ is satisfiable.
    Now, by the construction of $K$, line $13$ only tests relations
    which have to hold in any model of $\tuple{V,E,H'\cup K}$, and thus cannot
    reject, since then $Q'$ would not be satisfiable.
    Consequently, the algorithm accepts.

    Suppose that $Q$ is not satisfiable, and that it accepts,
    meaning that neither of the tests at lines $2$ or $13$ succeed.
    At line $2$, $Q'$ is not satisfiable, by \refpr{1.604}.
    At line $4$, $H'$ is satisfiable, and
    by the construction of $K$ in lines $4-11$,
    we have $\sep^+(Q',\tuple{V,E,H'\cup K})$ at line $12$.
    By the same argument as above, $H'\cup K$ is satisfiable at line $12$,
    using \refth{1.2}.
    If $\tuple{V,E,H'\cup K}$ were locally satisfiable for starting points,
    then $\tuple{V,E,H'\cup K}$ would be satisfiable, since
    $\cI$ is a starting point algebra, and thus $Q'$ would be satisfiable,
    contrary to our assumption.
    Thus $\tuple{V,E,H'\cup K}$ is not locally satisfiable.
    
    Since the algorithm does not reject in line $14$, the set
    \[P=\set{u^+\eprel^-(r) v^+\st\tuple{u,r,v}\in E\wedge u^-=v^-\in H'\cup K}\]
    is satisfiable by some model $M$.
    We already know that there exists a model $N$ for $H'\cup K$.
    We shall construct an interpretation $M'$ from $M$ and $N$ which locally satisfies
    $\tuple{V,E,H'\cup K}$, a contradiction.
    
    Let $x$ be minimal such that for some $v\in V$,
    $x=M(v^+)$, i.e.\ the smallest ending point in $M$, and let $y$ be
    maximal such that for some $v\in V$, $y=N(v^-)$, i.e.\ the
    largest starting point in $N$.
    Now, for every $v\in V$,
    set $M'(v^-)=N(v^-)$ and $M'(v^+)=M(v^+)-x+y+1$.
    We see that $M'$ still satisfies $P$, since the order on ending points
    is identical in $M$ and $M'$,
    and that it satisfies $H'\cup K$, since $M$ and $M'$ coincide on starting points.
    Furthermore, setting
    \[E'=\set{\tuple{u,r,v}\in E\st u^-=v^-\in H'\cup K},\]
    $\tuple{V,E',H'\cup K}$ is satisfied in $M'$, since $H'\cup K$ and $P$ are,
    and since by construction $M(v^-)<M(v^+)$ is satisfied for every $v\in V$.
    But this is the same as $M'$ locally satisfying $\tuple{V,E,H'\cup K}$,
    and this contradicts the fact that the algorithm does not reject.
    The result follows.
  }

\condtheorem{1.91}
  {
    \refalg{2} runs in polynomial time.
  }
  {
    The transformation in line $1$ is clearly polynomial
    and by \refpr{1a.1}, so is line $2$.
    The loop between lines $5$ to $11$ is executed
    as many times as there are arcs in $E$,
    and lines $6$ to $10$ take only polynomial time,
    thus the loop takes polynomial time.
    The final test on line $12$ is also polynomial-time (even linear),
    by \refpr{1a.2}, and the result follows.
  }

\condcorollary{1.92}
  {
    $\QSISAT(\cI)$ for starting point algebras,
    and $\QEISAT(\cI)$ for ending point algebras,
    is solvable in polynomial time.
  }
  {
    From \refth{1.9} and \refth{1.91}.
  }

\noindent For instances $Q=\tuple{V,E,H}$ where $H$ only
contains point algebra formulae,
we can use {\sc PAsat} instead of {\sc hornDLRsat} in lines $2$ and $6$,
since $\expl^-(Q)$ adds only point algebra formulae to $H$
and $K$ in \refalg{2} also contains only point algebra formulae.
This allows for a much better worst-case complexity, as we shall see.

\condcorollary{1.93}
  {
    If \refalg{2} uses {\sc PAsat} instead of {\sc hornDLRsat} in lines $2$ and $6$,
    its complexity becomes in $O(|E|^2)$.
  }
  {
    The first transformation clearly takes $O(|E|)$ time.
    The initial and final tests take $O(|E|)$ time,
    by \refpr{1a.2}, and the loop is executed
    $|E|$ times, each taking $O(|E|)$ time.
    Thus, the resulting complexity is $O(|E|^2)$.
  }

\noindent Note that we do not have a proof that these algebras
are the {\em only} algebras which are starting or ending point algebras
in Allen's interval algebra.
It seems likely that there should be more algebras with the
same structure. One advantage of the results presented in this paper is that
once a starting or ending point algebra is found (and proved to be one),
both a polynomial-time algorithm for satisfiability
and the extension to metric temporal information
are obtained for free.

\section{Maximality of Tractable Subclasses}\labsec{maximality}

Recently, the search for tractable subalgebras of Allen's interval
algebra has become more systematic, by focusing on finding
tractable algebras that are {\em maximal}, in the sense that
no algebra strictly containing it is tractable.
The pioneering work by Nebel and B\"urckert \shortcite{Nebel:Burckert:jacm95}
was to find a maximal tractable subclass containing
all the thirteen basic relations, the {\em ORD-Horn} algebra,
which in addition is the {\em unique} maximal
algebra containing all the basic relations.
The ORD-Horn algebra contains $868$ relations.
More recently, Drakengren and Jonsson \shortcite{Drakengren:Jonsson:aaai96}
have identified nine more maximal tractable algebras,
eight of which are of size $2178$, and one of size $4097$.
However, the latter is found to be of no use, since
any instance of satisfiability for that algebra
is always satisfiable, unless it contains the relation $\bot$.
The former algebras each contain three basic relations.

In \refpr{1.9101} we saw that the twelve nonmaximal
algebras of Drakengren and Jonsson
\shortcite{Drakengren:Jonsson:aaai96} are included in the algebras
of the current paper. However, it remains to check whether they
are maximal or not.

One of the main tools for analysing maximal tractability
is a {\em closure operation} on subclasses of the algebra,
which preserves tractability.

\definition{0.2}{Closure}
  {
    Let $S\subseteq\cA$.
    Then we denote by $\Cl{S}$ the {\em closure} of $S$ under
    converse, intersection and composition,
    i.e., the least subalgebra (which is uniquely determined)
    containing $S$, which is closed under the three operations.
  }

\noindent The key result for extrapolating tractability results is the 
following.

\proposition{0}
  {
    Let $S\subseteq\cA$.
    Then $\ISAT(S)$ is polynomial-time iff $\ISAT(\Cl{S})$ is, and
    $\ISAT(S)$ is NP-complete iff $\ISAT(\Cl{S})$ is.
  }
  {
    See Nebel and B\"urckert \shortcite{Nebel:Burckert:jacm95}.
  }

\noindent Our main tools for proving intractability are the following
NP-complete subalgebras of $\cA$.

\definition{0.1a}{NP-complete algebras $\cN_1$, $\cN_2$ and $\Delta_0$}
  {
    First let
    \[A=\set{(\rllt\ \rldi\ \rlo\ \rlm\ \rlfi),
             (\rllt\ \rld\ \rlo\ \rlm\ \rls)},\]
    define
    \[\cN_1=A\cup\set{(\rld\ \rldi\ \rloi\ \rlsi\ \rlf)}\]
    and
    \[\cN_2=A\cup\set{(\rldi\ \rlo\ \rloi\ \rlsi\ \rlfi)}.\]
    Also define
    \[\Delta_0=\set{
     (\rlequ\ \rld\ \rldi\ \rlo\ \rloi\ \rlm\ \rlmi\ \rls\ \rlsi\ \rlf\ \rlfi),
     (\rllt\ \rlgt)}.\]
  }

\proposition{0.1b}
  {
    $\ISAT(\cN_1)$, $\ISAT(\cN_2)$ and $\ISAT(\Delta_0)$ are
    all NP-complete.
  }
  {
    For $\cN_1$ and $\cN_2$, see Nebel and B\"{u}rckert
    \shortcite{Nebel:Burckert:jacm95}, and
    for $\Delta_0$, see Golumbic and Shamir \shortcite{Golumbic:Shamir:jacm93}.
  }

\noindent Next, we prove maximality of the current algebras.

\condproposition{2.3}
  {
    The algebras $S(b)$, $E(b)$, $S^*$, $E^*$
    are maximal tractable.
  }
  {
    By running the utility {\tt atry} \cite{Nebel:Burckert:software},
    which generates minimal extensions of subclasses by adding
    a relation and computing the closure of that class.
    All extensions of these algebras contain
    either of the NP-complete algebras $\cN_1$, $\cN_2$ or $\Delta_0$,
    so the result follows by \refpr{0}.
  }

\noindent Briefly, we show that the restriction that we cannot express
starting and ending point information at the same time is essential for
obtaining tractability, once we want to go outside the ORD-Horn algebra.

\condproposition{3.0}
  {
    Let $S\subseteq\cA$ such that $S$ is not a subset of
    the ORD-Horn algebra,
    and let $\mt{SE}$
    be the set of instances $Q=\tuple{V,E,H}$ of $\QISAT(S)$,
    where $H$ may contain only DLRs $u^+=v^-$ for some $u,v\in V$.
    Then the satisfiability problem for $\mt{SE}$ is NP-complete.
  }
  {
    By definition,
    $S$ has to contain some relation outside the ORD-Horn algebra.
    Since the expression $u^+=v^-$ is allowed in $H$,
    we can express the basic relation $\rlm$, and
    assume that it is included in $S$.
    It is easily verified that $\Cl{\set{\rlm}}$ contains
    all the basic relations (using e.g.\ the utility {\tt aclose}
    \cite{Nebel:Burckert:software}), and thus $\Cl{S}$ contains
    all basic relations.
    Since any subclass of Allen's algebra
    containing all the basic relations has to be contained
    in the ORD-Horn algebra in order to be tractable, and
    is NP-complete otherwise \cite{Nebel:Burckert:jacm95},
    NP-completeness follows.
  }

\noindent Despite this result, it seems possible to express constraints
on {\em duration} of intervals, without restricting their absolute
position in time, and still obtain a polynomial-time algorithm,
but this is left for future work.

Now, one might question the relevance of this work on the
grounds that this might be just eight out of thousands (or more)
of tractable subalgebras.
That is, we would like to have a result similar to the unique
maximality result of the ORD-Horn class, showing that these
algebras are the only algebras satisfying some specific criterion
of relevance.
In fact, recent results by the authors
\cite{Drakengren:Jonsson:ijcai97tcr} state
that any tractable subclass that is not yet known
in the literature cannot contain more than three basic
relation including converses (technically, it cannot contain
basic relations other than $(\rlequ)$, $(b)$ and $(\inv{b})$ for
$b\in\set{\rld,\rlo,\rls,\rlf}$).
This means, for instance, that the two algebras $S(\rlgt)$
and $E(\rllt)$ are the only maximal tractable algebras containing
the relation $\rllt$, and that any yet unpublished
tractable subclass has to be less expressive
in terms of the number of basic relations than
the present algebras containing five basic relations.

\section{Discussion}\labsec{discussion}

It seems appropriate to summarise the status of the search for
maximal tractable subclasses of Allen's interval algebra:
The eight new maximal tractable subalgebras
presented in this paper increase the number of currently known maximal
tractable subclasses to eighteen, including the
ORD-Horn class \cite{Nebel:Burckert:jacm95}, and the nine algebras found
by Drakengren and Jonsson \shortcite{Drakengren:Jonsson:aaai96}.

One may note that there is a considerable overlap
between these, since the sizes of the algebras are
$868$ (one), $2178$ (eight), $2312$ (eight), and $4097$ (one),
the sum of the sizes being much more than $8192$.
For instance, we showed in Drakengren and Jonsson
\shortcite{Drakengren:Jonsson:aaai96} that the only relations
of the ORD-Horn algebra that is not included in any of
the algebras discussed in that paper
are the relations $(\rlm)$ and $(\inv{\rlm})$.

Of course, the ultimate goal is to classify the {\em complete}
set of maximal tractable subalgebras, but since there
are $2^{8192}$ subclasses to investigate, this is clearly
a nontrivial task.
Recent results on the {\em RCC-5 algebra} for spatial reasoning
\cite{Jonsson:Drakengren:jair97} show that brute-force methods can have
success in characterising the complete set of tractable subclasses.
The present problem is harder with several orders of magnitude, however,
since the RCC-5 algebra contains only $2^{32}$ relations.
Nevertheless, it is encouraging to note that there are
only four maximal tractable subclasses of the RCC-5
algebra, out of the approximately $4.3\cdot 10^9$ subclasses.
As mentioned above, recent results by the authors
\cite{Drakengren:Jonsson:ijcai97tcr}
also provide a partial classification
of tractability in Allen's algebra, using similar methods.

Concerning metric time, it still remains
to provide the nine maximal tractable algebras of
Drakengren and Jonsson \shortcite{Drakengren:Jonsson:aaai96}
with some kind of metric temporal information.
A simple examination shows that we cannot use the
present technique, since this would make the resulting
algebras NP-complete (just add the qualitative relations induced
by relations on starting or ending points,
run {\tt aclose} \cite{Nebel:Burckert:software},
and verify that at least one of the NP-complete
algebras of \refpr{0.1b} is included),
so for this, some other kind of expressivity is needed.
Searching for other starting or ending point algebras could also be fruitful.
Further, it seems possible that the techniques presented here
can also be used for extending the point-interval algebra \cite{Vilain:aaai82}
with metric time.

\section{Conclusions}\labsec{conclusions}
We have found eight new maximal tractable subclasses of Allen's interval
algebra, and provided them with metric temporal
information on starting or ending points of intervals,
using the formalism of Horn DLRs \cite{Jonsson:Backstrom:aaai96tcr}.
Apart from representing progress in the research aiming
at a complete characterisation of the tractable subclasses
of Allen's interval algebra,
this opens for a combination between the expressivity of the ORD-Horn
algebra and algebras which can express {\em sequentiality} between intervals,
provided that only starting or ending points of intervals are related with
ORD-Horn relations.

\section*{Acknowledgements}
Thanks to Christer Bäckström, Henry Kautz, and the
two anonymous reviewers for helpful comments.

\bibliographystyle{apa}

\input{bibinclude}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 

