A Complete Classification of Complexity in Allens Algebra in the Presence of a Non-Trivial Basic Relation

1 Introduction

Allen's interval algebra [Allen, 1983] is one of the best established formalisms for temporal reasoning. Such reasoning is an important task in many areas of computer science and artificial intelligence (see, e.g., [Golumbic and Shamir, 1993; N¨okel, 1991]). Allen's algebra allows us to specify qualitative information about time intervals. This algebra has also become the kernel of some other formalisms [Meiri, 1996; Angelsmark and Jonsson, 2000]. The interval algebra and some of its extensions are closely related with a number of interval-based temporal logics used for real-time system specification [Bellini et al., 2000].

The basic satisfiability problem in Allen's algebra is NPcomplete [Vilain et al., 1989]), so it is unlikely that efficient algorithms exists for reasoning in the full algebra. The computational difficulty has motivated the search for effective heuristics, e.g., [Ladkin and Reinefeld, 1992], and the study of the complexity of fragments of the algebra, e.g., [Golumbic and Shamir, 1993; Nebel and B¨urckert, 1995].

☎ This research is partially supported by the UK EPSRC grants GR/R22704 and GR/M12926.

✆ This research is partially supported by the Swedish Research Council for Engineering Sciences (TFR) under grants 97-301 and 2000-361.

In this paper we follow the second approach, and we also assume throughout that P ✝ ✞ NP. Research in this direction has focused on identifying maximal tractable fragments, i.e., fragments which cannot be extended without losing tractability. So far, eighteen maximal tractable fragments of the algebra have been identified [Drakengren and Jonsson, 1997a; 1997b; Nebel and B¨urckert, 1995]. It is still unknown whether any others exist.

A complete classification of complexity within a certain large part of Allen's algebra was obtained in [Drakengren and Jonsson, 1998]. This result (as well as most similar results) was achieved by computer-assisted exhaustive search. However, it was noted in [Drakengren and Jonsson, 1998] that, for further progress, theoretical studies of the structure of Allen's algebra are required. There are some theoretical investigations of the structure of Allen's algebra, (see, e.g., [Hirsch, 1996; Ladkin and Maddux, 1994]). However they generally allow more operations on relations than originally used in [Allen, 1983], which makes them inappropriate for classifying complexity within the interval algebra. In this paper we systematically use an algebraic method that is similar to the approach taken in [Ligozat, 1998].

The first novel element in our approach is a new uniform description for all of the maximal tractable subalgebras of Allen's algebra which have already been identified (Table 2). Then we exhibit several new small NP-complete fragments of the algebra, including the first examples of NP-complete singletons (Proposition 2). Finally, we fully exploit the algebraic properties of Allen's algebra by importing a technique from general algebra. This technique has been used in many other contexts to obtain a description of maximal subalgebras of a given algebra with a given property (e.g., [Szendrei, 1995]). Here, for the first time, we systematically apply this technique to Allen's algebra to obtain a complete classification of the complexity of those fragments of the algebra containing a non-trivial basic relation (Theorem 1). Our method also provides (as a by-product) a new elementary proof of maximality of ten tractable subalgebras. In previous papers this proof of maximality has required extensive computer-aided case analysis [Drakengren and Jonsson, 1997a; 1997b].

The paper is organized as follows: in Section 2 we give the basic definitions of Allen's algebra and present the known maximal tractable subalgebras in the new form. Section 3 contains the new classification result, and Section 4 contains a brief discussion of future extensions.

2 Allen's Algebra

Allen's interval algebra [Allen, 1983] is based on the notion of relations between intervals. An interval ✂ is represented as a tuple ✔ ✂ ✟ ✖ ✂ ✄ ✘ of real numbers with ✂ ✟ ☎ ✂ ✄ , denoting the left and right endpoints of the interval, respectively. The possible relations between intervals are the ✛ ✜ ✢ possible unions of 13 basic interval relations, which are shown in Table 1. Relations between intervals will also be written as collections of basic relations so, for instance, the union of the basic relations p, m and f ✡ ☛ is written ✔ p m f ✡ ☛ ✘ . Allen's algebra ✤ consists of the ✛ ✜ ✢ possible relations between intervals together with the operations converse ✦ ✟ ✜ , intersection ✧ and composition ★ which are defined as follows:

It follows that the converse of ✭ ✞ ✔ ❅ ✜ ❇ ❇ ❇ ❅ ❊ ✘ is equal to ✔ ❅ ✟ ✜ ✜ ❇ ❇ ❇ ❅ ✟ ✜ ❊ ✘ . The intersection of two relations can be expressed as the usual set-theoretic intersection. Using the definition of composition, it can be derived that

All algebraic calculations given in Section 3 can be done by hand; however, a simple table showing the results of the composition operation on all pairs of basic relations (which can be found, e.g., in [Ladkin and Maddux, 1994]) makes such calculations considerably easier.

The problem of satisfiability ( ✤ -SAT) of a set of interval variables with relations between them is that of 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. This is defined as follows.

Definition 1 Let ❬ ❭ ✤ be a set of interval relations. An instance ❴ of ✤ -SAT( ❬ ) is a set, ❵ , of variables and a set of constraints of the form ✂ ✭ ✝ where ✂ ✖ ✝ ❜ ❵ and ✭ ❜ ❬ . The question is whether ❴ is satisfiable, i.e., whether there exists a function, ❝ , from ❵ to the set of all intervals such that ❝ ✔ ✂ ✘ ✭ ❝ ✔ ✝ ✘ holds for every constraint ✂ ✭ ✝ in ❴ .

If there exists a polynomial-time algorithm solving all instances of ✤ -SAT( ❬ ) then we say that ❬ is tractable. On the other hand, if ✤ -SAT(❬ ) is NP-complete then we say that ❬ is NP-complete. Since the problem ✤ -SAT(✤ ) is NPcomplete [Vilain et al., 1989], there arises the question of description of tractable subsets of Allen's algebra.

Subsets of ✤ that are closed under the operations of intersection, converse and composition are said to be subalgebras. For a given subset ❬ of ✤ , the smallest subalgebra containing ❬ is called the subalgebra generated by ❬ and is denoted by ❢ ❬ ❣ . It is easy to see that ❢ ❬ ❣ is obtained from ❬ by adding all relations that can be obtained from the relations in ❬ by using the three operations of ✤ .

It is known [Nebel and B¨urckert, 1995], and easy to prove, that, for every ❬ ❭ ✤ , the problem ✤ -SAT( ❢ ❬ ❣ ) is polynomially equivalent to ✤ -SAT(❬ ). Therefore, to classify the complexity of all subsets of ✤ it is only necessary to consider subalgebras of ✤ . Obviously, adding relations to a subalgebra can only increase the complexity of the corresponding satisfiability problem. Thus, since ✤ is finite, the problem of describing tractability in ✤ can be reduced to the problem of describing the maximal tractable subalgebras in ✤ , i.e., subalgebras that cannot be extended without losing tractability.

The known maximal tractable subalgebras [Drakengren and Jonsson, 1997a; 1997b; Nebel and B¨urckert, 1995] are presented in Table 2. In our proofs as well as in Table 2 we use the symbol ❦ , which should be interpreted as follows. A condition involving ❦ means the conjunction of two conditions: one corresponding to ❧ and one corresponding to ♠ . For example, condition ✔ o ✘ ♥ ✜ ❭ ✭ ✯ ✔ d ✘ ♥ ✜ ❭ ✭ means that both ✔ o ✘ ❭ ✭ ✯ ✔ d ✘ ❭ ✭ and ✔ o ✡ ☛ ✘ ❭ ✭ ✯ ✔ d ✡ ☛ ✘ ❭ ✭ hold. The main advantage of using the ❦ symbol is conciseness: in any subalgebra of ✤ , the ❧ and the ♠ conditions are satisfied (or not satisfied) simultaneously, and, therefore only one of them needs to be verified.

In previous papers, the subalgebras from Table 2 were defined in other ways. However, in all cases except for a115 , it is very straightforward to verify that our definitions are equivalent to the original ones. The subalgebra a115 was originally defined as the 'ORD-Horn algebra' [Nebel and B¨urckert, 1995], but has also been characterized as the algebra of 'pre-convex' relations (see, e.g., [Ligozat, 1998]). Using the latter description it is not hard to show that our definition of a115 is equivalent. Finally, we note that there is one more known maximal tractable subalgebra that is not included in Table 2. That subalgebra is defined as ◆ a116 ❨ ✉ ◆ ✭ ❜ ✤ ❘ ✔ ✏ ✘ ❭ ✭ ❨ and the only basic relation it contains is ✔ ✏ ✘ .

a0 p ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmod ✡ ☛ f ✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ p ✘ ♥ ✜ ❭ ✭ ❨ ✄ p ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmods ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ p ✘ ♥ ✜ ❭ ✭ ❨ a0 d ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmod ✡ ☛ f ✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ d ✡ ☛ ✘ ♥ ✜ ❭ ✭ ❨ ✄ d ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmods ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ d ✘ ♥ ✜ ❭ ✭ ❨ a0 o ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmod ✡ ☛ f ✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ o ✘ ♥ ✜ ❭ ✭ ❨ ✄ o ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmods ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ o ✘ ♥ ✜ ❭ ✭ ❨ ✤ ✜ ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmod ✡ ☛ f ✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ s ✡ ☛ ✘ ♥ ✜ ❭ ✭ ❨ ✆ ✜ ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmods ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ f ✡ ☛ ✘ ♥ ✜ ❭ ✭ ❨ ✤ ✝ ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmod ✡ ☛ f ✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ s ✘ ♥ ✜ ❭ ✭ ❨ ✆ ✝ ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmods ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ f ✘ ♥ ✜ ❭ ✭ ❨ ✤ ✢ ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmodf ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ s ✘ ♥ ✜ ❭ ✭ ❨ ✆ ✢ ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmod✡ ☛ s✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ f ✡ ☛ ✘ ♥ ✜ ❭ ✭ ❨ ✤ ✟ ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmodf ✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ s ✘ ♥ ✜ ❭ ✭ ❨ ✆ ✟ ✞ ◆ ✭ ❘ ✭ ✧ ✔ pmod✡ ☛ s ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ f ✡ ☛ ✘ ♥ ✜ ❭ ✭ ❨ ✄ ✡ ✞ ☞ ✭ ✌ ✌ ✌ ✌ ✎ ✘ ✭ ✧ ✔ pmod ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ s ✘ ♥ ✜ ❭ ✭ , and ✛ ✘ ✭ ✧ ✔ ff ✡ ☛ ✘ ✝ ✞ a116 ✁ ✔ ✏ ✘ ❭ ✭ ✏ a0 ✡ ✞ ☞ ✭ ✌ ✌ ✌ ✌ ✎ ✘ ✭ ✧ ✔ pmod ✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ f ✡ ☛ ✘ ♥ ✜ ❭ ✭ , and ✛ ✘ ✭ ✧ ✔ ss✡ ☛ ✘ ✝ ✞ a116 ✁ ✔ ✏ ✘ ❭ ✭ ✏ a115 ✞ ✒ ✔ ✕ ✭ ✌ ✌ ✌ ✌ ✌ ✌ ✎ ✘ ✭ ✧ ✔ os ✘ ♥ ✜ ✝ ✞ a116 ✼ ✭ ✧ ✔ o ✡ ☛ f ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ d ✘ ♥ ✜ ❭ ✭ , and ✛ ✘ ✭ ✧ ✔ ds ✘ ♥ ✜ ✝ ✞ a116 ✼ ✭ ✧ ✔ d ✡ ☛ f ✡ ☛ ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ o ✘ ♥ ✜ ❭ ✭ , and ✖ ✘ ✭ ✧ ✔ pm ✘ ♥ ✜ ✝ ✞ a116 ✼ ✭ ✝ ❭ ✔ pm ✘ ♥ ✜ ✁ ✔ o ✘ ♥ ✜ ❭ ✭ ✗ ✘ ✙

Finally, we observe that when a0 is one of the algebras ✄ ✡ , a0 ✡ , ✤ a80 , or ✆ a80 ( ✎ ❯ ❚ ❯ ✣ ), then ❅ ✚ ✷ ✔ a0 ✘ is either ◆ ✏ ✖ s ✖ s ✡ ☛ ❨ or ◆ ✏ ✖ f ✖ f ✡ ☛ ❨ . With the help of computer-aided exhaustive search, it was proved in [Drakengren and Jonsson, 1997a; 1997b] that these ten algebras are maximal tractable subalgebras of Allen's algebra. Since we do not use computer-aided results in Subsection 3.2, our results provide a new elementary proof of maximality for these algebras.

Throughout this section we shall assume that a non-trivial relation is also non-empty; this will cause no confusion.

3.1 NP-completeness results

This subsection contains the NP-completeness proofs that we need in the sequel. Our reductions are based on the NP-complete problem BETWEENNESS [Garey and Johnson, 1979]:

INSTANCE: A finite set ✥ and a collection ✦ of ordered ✚ ❅ ★

QUESTION: Is there a total ordering ☎ on ✥ such that for ✚ ✖ ❅ ✖ ★ ❜ ✦ , we have either ✚ ☎ ❅ ☎ ★ or ★ ☎ ❅ ☎ ✚ ?

triples ✔ ✖ ✖ ✘ of distinct elements from ✥ . each ✔ ✘

Let us fix relations ✫ ✖ ✫ ✜ ✖ ✫ ✝ ❜ ✤ . Then we define ✬ ✔ ✚ ✖ ❅ ✖ ★ ✖ ✂ ✖ ✝ ✘ to be the following problem instance over the variables ◆ ✚ ✖ ❅ ✖ ★ ✖ ✂ ✖ ✝ ❨ :

Further, define ✬ ✜ ✞ ✬ ✔ ✚ ✖ ❅ ✖ ★ ✖ ✂ ✖ ✝ ✘ ✉ ◆ ✚ ✫ ❅ ✖ ❅ ✫ ★ ❨ , ✬ ✝ ✞ ✬ ✔ ✚ ✖ ❅ ✖ ★ ✖ ✂ ✖ ✝ ✘ ✉ ◆ ❅ ✫ ✚ ✖ ❅ ✫ ★ ✖ ✚ ✫ ✉ ✫ ✟ ✜ ★ ❨ , and ✬ ✢ ✞ ✬ ✔ ✚ ✖ ❅ ✖ ★ ✖ ✂ ✖ ✝ ✘ ✉ ◆ ✚ ✫ ❅ ✖ ★ ✫ ❅ ✖ ✚ ✫ ✉ ✫ ✟ ✜ ★ ❨ .

Lemma 1 Let ✫ ❜ ◆ ✔ p ✘ ✖ ✔ d ✘ ✖ ✔ o ✘ ✖ ✔ s ✘ ❨ , ✫ ✜ ✖ ✫ ✝ ❜ ✤ , and let ✬ ✜ , ✬ ✝ , ✬ ✢ be as above. If ✬ ✜ is satisfiable while ✬ ✝ and ✬ ✢ are not, then ◆ ✫ ✉ ✫ ✟ ✜ ✖ ✫ ✜ ✖ ✫ ✝ ❨ is NP-complete.

Proof. Polynomial-time reduction from BETWEENNESS. Let ✔ ✥ ✖ ✦ ✘ be an arbitrary instance of the problem and construct an instance ❴ of ✤ -SAT( ◆ ✫ ✉ ✫ ✟ ✜ ✖ ✫ ✜ ✖ ✫ ✝ ❨ ) as follows:

1. for each pair of distinct elements ✚ ✖ ❅ ❜ ✥ , add the constraint ✚ ✫ ✉ ✫ ✟ ✜ ❅ to ❴ ; and

3 Main Result

Throughout the paper, a0 denotes a subalgebra of ✤ . We denote by ❅ ✚ ✷ ✔ a0 ✘ the set of basic relations in a0 . Our result is an extension of the following proposition which was proved in [Drakengren and Jonsson, 1998].

Proposition 1

1) Let a0 be a subalgebra of ✤ with ❘ ❅ ✚ ✷ ✔ a0 ✘ ❘ ✎ ✖ . Then a0 is tractable if and only if it is contained in one of the following 7 algebras: a0 p, a0 d, a0 o, ✄ p, ✄ d, ✄ o, and a115 . Otherwise a0 is NP-complete.

2) Let a0 be a subalgebra of ✤ such that ✔ m ✘ ❜ a0 or ✔ p ✘ ❜ a0 . If a0 is tractable then a0 ❭ a0 p, or a0 ❭ ✄ p, or a0 ❭ a115 . Otherwise a0 is NP-complete.

We improve this result by showing that any so far unknown tractable subalgebra can contain only a trivial basic relation. Throughout the paper, by a trivial basic relation we mean the equality relation ✏ .

Theorem 1 Suppose a0 is a subalgebra of ✤ containing a non-trivial basic relation. Then a0 is tractable if and only if it is contained in one of the 17 algebras listed in Table 2. Otherwise a0 is NP-complete.

We can assume, without loss of generality, that a0 contains the relation ✔ ✏ ✘ , since it is easy to show that a0 and a0 ✉ ◆ ✔ ✏ ✘ ❨ have the same complexity (up to polynomial-time equivalence). This implies that the size of ❅ ✚ ✷ ✔ a0 ✘ is odd since a0 is closed under converse. By combining Proposition 1(1) and the previous observation, we may consider only the case ❘ ❅ ✚ ✷ ✔ a0 ✘ ❘ ✞ ✖ . By Proposition 1(2), it suffices to consider the cases where ❅ ✚ ✷ ✔ a0 ✘ is one of the following sets: ◆ ✏ ✖ s ✖ s ✡ ☛ ❨ , ◆ ✏ ✖ f ✖ f ✡ ☛ ❨ , ◆ ✏ ✖ d ✖ d✡ ☛ ❨ , or ◆ ✏ ✖ o ✖ o✡ ☛ ❨ .

The rest of this section is organized as follows. In Subsection 3.1 we describe some NP-complete sets of relations which we use in our proofs later. In Subsection 3.2, we give a complete proof of Theorem1 for the cases where ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ s ✖ s ✡ ☛ ❨ and ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ f ✖ f ✡ ☛ ❨ . Finally, in Subsection 3.3 we give a sketch of a proof of Theorem 1 for the cases where ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ d ✖ d✡ ☛ ❨ and ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ o ✖ o✡ ☛ ❨ .

1. for each triple ✔ ✚ ✖ ❅ ✖ ★ ✘ ❜ ✦ , introduce two fresh variables ✂ ✖ ✝ and add ✬ ✔ ✚ ✖ ❅ ✖ ★ ✖ ✂ ✖ ✝ ✘ to ❴ .

It is a routine verification to show that ❴ is satisfiable if and only if ✔ ✥ ✖ ✦ ✘ has a solution. a0

The restriction ✫ ❜ ◆ ✔ p ✘ ✖ ✔ d ✘ ✖ ✔ o ✘ ✖ ✔ s ✘ ❨ is imposed to ensure that we get a natural total ordering in the reduction. Many other relations such as ✔ dsf ✘ have this property but there are also relations without this property, e.g., ✔ ✏ ✘ and ✔ mm ✡ ☛ ✘ .

Suppose ❬ ❭ ✤ and ❴ is an instance of ✤ -SAT(❬ ). Let variables ✂ ✖ ✝ be involved in ❴ . Further, let ✭ ❜ ✤ be the relation defined as follows. A basic relation ✭ ❏ is included in ✭ if and and only if the instance obtained from ❴ by adding the constraint ✂ ✭ ❏ ✝ is satisfiable. In this case, we say that ✭ is derived from ❬ . It can be easily checked that the problems ✤ -SAT( ❬ ) and ✤ -SAT( ❬ ✉ ◆ ✭ ❨ ) are polynomially equivalent. Looking now at the definition of the three operations of the interval algebra, it is easy to see that, generally, one can derive more relations from a given ❬ ❭ ✤ than one can generate using these operations. On the other hand, derivation is essentially harder to manage while the operations of Allen's algebra give us the advantage of employing algebraic techniques. Therefore, in this paper, we use derivation only once in the proof of the following statement.

Proposition 2 The following subsets of ✤ are NP-complete: 1) ◆ ✔ d ✘ ✖ ✔ oo ✡ ☛ ✘ ❨ , ◆ ✔ d ✡ ☛ ✘ ✖ ✔ pp ✡ ☛ ✘ ❨ , and ◆ ✔ o ✘ ✖ ✔ dd ✡ ☛ ✘ ❨ . 2) ◆ ✭ ❨ with ✔ ods ✡ ☛ ✘ ❭ ✭ ❭ ✔ pmods ✡ ☛ f ✡ ☛ ✘ .

Proof. For part (1), applyLemma 1with ✫ ✞ ✔ o ✘ , ✫ ✜ ✞ ✔ d ✘ , ✫ ✝ ✞ ✔ oo ✡ ☛ ✘ , or with ✫ ✞ ✔ p ✘ , ✫ ✜ ✞ ✔ d ✡ ☛ ✘ , ✫ ✝ ✞ ✔ pp ✡ ☛ ✘ , or with ✫ ✞ ✔ d ✘ , ✫ ✜ ✞ ✔ o ✘ , ✫ ✝ ✞ ✔ dd ✡ ☛ ✘ , respectively.

To prove part (2), let ✭ ✢ be the union of all basic relations except for ✏ and s ✡ ☛ , and consider the instance ✬ ✟ ✞ ◆ ✚ ✭ ❅ ✖ ❅ ✭ ★ ✖ ★ ✭ ✚ ✖ ✁ ✭ ❅ ✖ ✁ ✭ ★ ❨ over the variables ✚ ✖ ❅ ✖ ★ ✖ ✁ . In the cases when ✭ ✞ ✔ ods ✡ ☛ ✘ or ✭ ✞ ✔ pmods ✡ ☛ f ✡ ☛ ✘ , it can be shown that ✬ ✟ ✉ ◆ ✁ ✭ ❏ ✚ ❨ is satisfiable for every basic relation ✭ ❏ ❭ ✭ ✢ but not satisfiable for any other choice of ✭ ❏ . Hence, we can derive ✭ ✢ from ✭ , and we can also derive the relations ✭ ✟ ✞ ✭ ✧ ✭ ✢ ✞ ✭ ♠ ✔ s ✡ ☛ ✘ and ✭ ✄ ✞ ✭ ✟ ★ ✭ ✟ . It is easy to check that

which implies that ✭ ✄ ✧ ✭ ✟ ✜ ✞ ✔ s ✘ . Furthermore, we have ✔ s ✘ ★ ✔ s ✡ ☛ ✘ ✞ ✔ ✏ ss ✡ ☛ ✘ , and ✭ ★ ✭ is the disequality relation, so the relation ✔ ss✡ ☛ ✘ can be obtained from the relation ✭ . If ✫ ✞ ✔ s ✘ , ✫ ✜ ✞ ✭ ✟ ✜ and ✫ ✝ ✞ ✭ , then these relations satisfy the conditions of Lemma 1 so ◆ ✔ ss ✡ ☛ ✘ ✖ ✭ ✟ ✜ ✖ ✭ ❨ is NPcomplete. Since all of these relations can be derived from the single relation ✭ , it follows that ◆ ✭ ❨ is NP-complete. a0

3.2 The s ✆ f case

We will show that if ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ s ✖ s ✡ ☛ ❨ , then either a0 is NP-complete or a0 is contained in one of the subalgebras a0 p, a0 d, a0 o, ✄ ✡ , a115 , or in one of ✤ a80 , ✎ ❯ ❚ ❯ ✣ . By using the obvious symmetry between the relations ✔ s ✘ and ✔ f ✘ , it immediately follows that if ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ f ✖ f ✡ ☛ ❨ , then either a0 is NP-complete or contained in one of ✄ p, ✄ d, ✄ o, a0 ✡ , a115 , or ✆ a80 , ✎ ❯ ❚ ❯ ✣ . For the remainder of this subsection, it is assumed that ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ s ✖ s ✡ ☛ ❨ .

Given a relation ✭ , we write ✭ ✡ to denote the relation ✭ ✧ ✭ ✟ ✜ . Throughout the proofs we use the obvious fact that if ✭ ✜ ❭ ✭ ✝ then, for any ✭ , we have ✭ ★ ✭ ✜ ❭ ✭ ★ ✭ ✝ and ✭ ✜ ★ ✭ ❭ ✭ ✝ ★ ✭ . If ❅ is a basic relation then ✭ ✝ denotes the least relation ✭ ❜ a0 such that ✔ ❅ ✘ ❭ ✭ , i.e. the intersection of all ✭ ❜ a0 with this property. It is easy to show that the relation ✭ ✝ exists in a0 for every basic relation ❅ , except for two very simple cases: when every ✭ ❜ a0 satisfies exactly one of conditions ✭ ❭ ✔ ✏ ss ✡ ☛ ✘ and ✭ ❭ ✔ ✏ ff ✡ ☛ ✘ . In both cases, we have a0 ❭ a115 .

Lemma 2 If a0 contains the relation ✔ od ✘ , then every relation in a0 satisfies condition 3) of a115 .

Proof. Arbitrarily choose ✭ ❜ a0 . Since ✔ od ✘ ❜ a0 , it follows that ✭ d ✞ ✭ o ✞ ✔ od ✘ and ✔ o ✘ ♥ ✜ ❭ ✭ ✯ ✔ d ✘ ♥ ✜ ❭ ✭ . Furthermore, ✭ ✜ ✞ ✔ s ✘ ★ ✔ od ✘ ✞ ✔ pmod ✘ ❜ a0 so ✭ p ❭ ✭ ✜ and ✭ m ❭ ✭ ✜ . Since ✔ pm ✘ ★ ✔ pm ✘ ✞ ✔ p ✘ , we have ✭ p ✝ ❭ ✔ pm ✘ and ✭ m ✝ ❭ ✔ pm ✘ , which implies that ✭ p ✧ ✔ od ✘ ✝ ✞ a116 and ✭ m ✧ ✔ od ✘ ✝ ✞ a116 . Now it follows that ✔ od ✘ ❭ ✭ p and ✔ od ✘ ❭ ✭ m. Thus, if ✭ ✧ ✔ pm ✘ ✝ ✞ a116 , then ✔ od ✘ ❭ ✭ and ✭ satisfies condition 3) of a115 . a0

Lemma 3 If a0 contains a non-trivial relation ✭ ❏ with ✭ ❏ ❭ ✔ ✏ pp ✡ ☛ mm ✡ ☛ ff ✡ ☛ ✘ then a0 is included in one of a115 , ✄ ✡ , or a0 p, or else a0 is NP-complete.

Proof. Case 1. ✭ ❏ ✞ ✔ ff ✡ ☛ ✘ Since ✔ ff ✡ ☛ ✘ ★ ✔ s ✘ ✞ ✔ od ✘ ❜ a0 , it follows that any ✭ ❜ a0 satisfies condition 3) of a115 , by Lemma 2. Now it follows that, for any ✭ ❜ a0 , we have ✔ o ✘ ♥ ✜ ❭ ✭ ✯ ✔ d ✘ ♥ ✜ ❭ ✭ and also ✔ f ✘ ❭ ✭ ✯ ✔ f ✡ ☛ ✘ ❭ ✭

Suppose that a0 ✝ ❭ a115 , i.e. some ✭ ❜ a0 fails to satisfy condition 1) or condition 2) of a115 . Then, using the facts from the previous paragraph, it can be shown that we can choose ✭ so that ✔ s ✡ ☛ ff ✡ ☛ ✘ ❭ ✭ ❭ ✔ ✏ pmodss ✡ ☛ ff ✡ ☛ ✘ or ✔ ods ✡ ☛ ✘ ❭ ✭ ❭ ✔ ✏ pmodss ✡ ☛ ff ✡ ☛ ✘ . In both cases, composing the relations with ✔ s ✘ from the left we get

✔ ✏ pmodss✡ ☛ ✘ ❭ ✔ s ✘ ★ ✭ ❭ ✔ ✏ pmodss✡ ☛ ✘ ❇

Therefore ✔ ✏ pmodss ✡ ☛ ✘ ❜ a0 , and ✔ pmods ✡ ☛ ✘ can be obtained as

Then a0 is NP-complete, by Proposition 2(2).

Composing ✭ ❏ and its inverse we get ✔ ✏ ff ✡ ☛ ✘ , so we may assume that ✭ ❏ ✞ ✔ ✏ ff ✡ ☛ ✘ . If some relation ✭ ✝ ❜ a0 fails to satisfy condition 2) of ✄ ✡ , then ✭ ✝ ✧ ✭ ❏ is either one of ✔ f ✘ and ✔ f ✡ ☛ ✘ , which is impossible under our assumptions, or ✔ ff ✡ ☛ ✘ going back to Case 1. Suppose now that each ✭ ❜ a0 satisfies condition 2) of ✄ ✡ .

We have ✭ ❏ ★ ✔ s ✘ ✞ ✔ ods ✘ ❜ a0 . If ✔ od ✘ belongs to a0 then ✭ ❏ ✧ ✔ ✔ s✡ ☛ ✘ ★ ✔ od ✘ ✘ ✞ ✔ ff ✡ ☛ ✘ ❜ a0 , which implies a0 ❭ a115 . Otherwise we have ✭ ✧ ✔ od ✘ ♥ ✜ ✝ ✞ a116 ✁ ✔ s ✘ ♥ ✜ ❭ ✭ for every ✭ ❜ a0 . Assume a relation ✭ ✢ ❜ a0 does not satisfy condition 1) of ✄ ✡ , that is ✭ ✢ ✧ ✔ pmod ✘ ✝ ✞ a116 and ✔ s ✘ ✝ ❭ ✭ ✢ . Since ✔ pmods ✘ ✞ ✔ s ✘ ★ ✭ ❏ ❜ a0 , we have ✭ ✟ ✞ ✭ ✢ ✧ ✔ pmods ✘ ❜ a0

and ✭ ✟ ❭ ✔ pm ✘ . This implies ✭ ✟ ★ ✭ ✟ ✞ ✔ p ✘ , a contradiction. Therefore the relations in a0 must satisfy both conditions of ✄ ✡ , that is a0 ❭ ✄ ✡ .

Case 3. ✭ ❏ ❭ ✔ ✏ mm ✡ ☛ ff ✡ ☛ ✘ and ✭ ❏ ✧ ✔ mm ✡ ☛ ✘ ✝ ✞ a116 . Without loss of generality we may assume that ✔ m ✘ ❭ ✭ ❏ . Then the relation ✔ ✭ ❏ ✧ ✔ ✭ ❏ ★ ✔ s ✡ ☛ ✘ ✘ is equal either to ✔ mm ✡ ☛ ✘ or to ✔ m ✘ . In the former case it follows that the relation ✔ m ✘ ✞ ✔ mm ✡ ☛ ✘ ✧ ✔ ✔ mm ✡ ☛ ✘ ★ ✔ s ✡ ☛ ✘ ✘ belongs to a0 as well. A contradiction.

Case 4. ✭

❏

✧

✔ pp ✡

☛

✘

✞

✝

a116 .

We may assume, without loss of generality, that ✔ p ✘ ❭ ✭ ❏ . Then ✔ p ✘ ❭ ✔ s ✘ ★ ✭ ❏ ❭ ✔ pp✡ ☛ mm✡ ☛ ods ✘ . Furthermore, ✔ p ✘ ❭ ✭ ✄ ✞ ✭ ❏ ✧ ✔ ✔ s ✘ ★ ✭ ❏ ✘ ❭ ✔ pp ✡ ☛ mm ✡ ☛ ✘ , and we have ✔ p ✘ ❭ ✭ a0 ✞ ✭ ✄ ★ ✔ s ✡ ☛ ✘ ❭ ✔ pp ✡ ☛ m ✘ . If ✔ p ✡ ☛ ✘ ✝ ❭ ✭ a0 then ✭ a0 ★ ✭ a0 ✞ ✔ p ✘ ❜ a0 , a contradiction. Otherwise we have ✔ pp ✡ ☛ ✘ ✞ ✭ ✡ a0 ❜ a0 . Then ✔ p ✘ ❭ ✭ ✯ ✔ p ✡ ☛ ✘ ❭ ✭ holds for every ✭ ❜ a0 .

We have ✔ s ✡ ☛ ✘ ★ ✔ pp ✡ ☛ ✘ ✞ ✔ pp ✡ ☛ mod ✡ ☛ f ✡ ☛ ✘ ❜ a0 . For every non-empty ✭ ✁ ❭ ✔ modf ✡ ☛ ✘ , we have ✔ ✔ s ✘ ★ ✭ ✁ ✘ ✧ ✔ pp✡ ☛ ✘ ✞ ✔ p ✘ . Therefore no such ✭ ✁ belongs to a0 . We conclude that, for any ✭ ❜ a0 , if ✭ ✧ ✔ mod ✡ ☛ f ✡ ☛ ✘ ✝ ✞ a116 then ✔ p ✘ ❭ ✭ , whichmeans that a0 ❭ a0 p. a0

We assume further that, for every non-trivial ✭ ❜ a0 , we have ✭ ✧ ✔ oo ✡ ☛ dd ✡ ☛ ss ✡ ☛ ✘ ✝ ✞ a116 . In the next four lemmas we consider the case when a0 contains a non-trivial relation ✭ ❏ with ✭ ❏ ✧ ✔ ss✡ ☛ ✘ ✞ a116 . In view of the assumption just made we may consider that ✭ ❏ is either ✭ d or ✭ o. It is not hard to verify that these four lemmas indeed cover all possible cases for ✭ d and ✭ o.

Lemma 4 Suppose ✭ d ✧ ✔ ss ✡ ☛ ✘ ✞ a116 . If ✭ d ✧ ✔ oo ✡ ☛ dd ✡ ☛ ✘ ✞ ✔ d ✘ or ✔ dd ✡ ☛ ✘ ❭ ✭ d then a0 ❭ a0 d.

Proof. Case 1. ✭ d ✧ ✔ oo✡ ☛ dd✡ ☛ ✘ ✞ ✔ d ✘ .

By assumption, the relation ✭ d satisfies condition ✔ d ✘ ❭ ✭ d ❭ ✔ ✏ pp ✡ ☛ mm ✡ ☛ dff ✡ ☛ ✘ . Let ✭ ✜ be calculated as ✭ d ✧ ✔ ✔ s ✘ ★ ✭ d ✘ . Then we have ✔ d ✘ ❭ ✭ ✜ ❭ ✔ pp✡ ☛ mm✡ ☛ d ✘ . By minimality of ✭ d we get ✔ d ✘ ❭ ✭ d ❭ ✔ pp ✡ ☛ mm ✡ ☛ d ✘ . Calculating ✭ ✜ again, we get ✔ d ✘ ❭ ✭ d ❭ ✔ pp ✡ ☛ m ✡ ☛ d ✘ . Since ✔ pp ✡ ☛ ✘ ✝ ❜ a0 , and since we have ✔ m ✡ ☛ d ✘ ❭ ✭ d ★ ✔ s ✘ only if ✔ p ✡ ☛ ✘ ❭ ✭ d, we may assume that ✭ d is either ✔ pd ✘ , or ✔ p ✡ ☛ d ✘ , or ✔ p ✡ ☛ m ✡ ☛ d ✘ . The first case is impossible because of ✔ pd ✘ ✧ ✔ ✔ p ✡ ☛ d ✡ ☛ ✘ ★ ✔ s ✘ ✘ ✞ ✔ d ✘ . Let ✔ p ✡ ☛ d ✘ ❭ ✭ d ❭ ✔ p ✡ ☛ m ✡ ☛ d ✘ . Then ✔ p ✡ ☛ m ✡ ☛ o ✡ ☛ df ✘ ✞ ✭ d ★ ✔ s ✘ ❜ a0 . Suppose a0 contains a non-empty subrelation ✭ ✝ of ✔ p✡ ☛ m✡ ☛ o✡ ☛ f ✘ . Then ✭ ✢ ✞ ✭ d ✧ ✔ ✭ ✝ ★ ✔ s ✡ ☛ ✘ ✘ is a non-empty subrelation of ✔ p ✡ ☛ m ✡ ☛ ✘ implying that ✔ p ✡ ☛ ✘ ✞ ✭ ✢ ★ ✭ ✢ ❜ a0 , a contradiction. Therefore, for every ✭ ❜ a0 , we have ✭ ✧ ✔ p ✡ ☛ m✡ ☛ o✡ ☛ f ✘ ✝ ✞ a116 ✁ ✔ d ✘ ❭ ✭ , which means that a0 ❭ a0 d.

Suppose a relation ✭ ✟ ❜ a0 satisfies both ✭ ✟ ✝ ❭ ✔ ✏ ss✡ ☛ ✘ and ✔ dd ✡ ☛ ✘ ✝ ❭ ✭ ✟ . Then it is not hard to verify that either ✔ ✔ s ✡ ☛ ✘ ★ ✭ ✟ ✘ ✧ ✭ d or ✔ ✭ ✟ ★ ✔ s ✘ ✘ ✧ ✭ d contains exactly one of ✔ d ✘ and ✔ d ✡ ☛ ✘ which contradicts the minimality of ✭ d. Thus, for every ✭ ❜ a0 such that ✭ ✝ ❭ ✔ ✏ ss✡ ☛ ✘ , we have ✔ dd ✡ ☛ ✘ ❭ ✭ . This implies that a0 ❭ a0 d. a0

Case 2. ✔ dd ✡ ☛ ✘ ❭ ✭ d ✧ ✔ oo ✡ ☛ dd ✡ ☛ ✘ .

Lemma 5 Suppose ✭ o ✧ ✔ ss ✡ ☛ ✘ ✞ a116 . If ✭ o ✧ ✔ oo ✡ ☛ dd ✡ ☛ ✘ ✞ ✔ o ✘ or ✔ oo✡ ☛ ✘ ❭ ✭ o then a0 ❭ a0 o.

Proof. Similar to the previous lemma.

Lemma 6 If ✭ d ✞ ✭ o✡ ☛ and ✭ d ✧ ✔ oo✡ ☛ dd✡ ☛ ss✡ ☛ ✘ ✞ ✔ o✡ ☛ d ✘ then a0 ❭ a0 d.

Proof. As in the proof of Lemma 4, we can obtain ✔ o ✡ ☛ d ✘ ❭ ✭ d ❭ ✔ pp✡ ☛ m✡ ☛ o✡ ☛ df ✘ . If ✔ po✡ ☛ d ✘ ❭ ✭ d then ✔ ✭ d ★ ✔ s✡ ☛ ✘ ✘ ✡ ✞ ✔ pp✡ ☛ ✘ ❜ a0 , a contradiction. Therefore we have ✔ o ✡ ☛ d ✘ ❭ ✭ d ❭ ✔ p ✡ ☛ m ✡ ☛ o ✡ ☛ df ✘ , and ✔ p ✡ ☛ m ✡ ☛ o ✡ ☛ df ✘ ✞ ✭ d ★ ✔ s ✡ ☛ ✘ ❜ a0 . If some non-empty subrelation ✭ ✜ of ✔ p ✡ ☛ m ✡ ☛ f ✘ belongs to a0 then ✭ ✝ ✞ ✭ ✜ ✧ ✔ ✭ ✜ ★ ✔ s✡ ☛ ✘ ✘ is a non-empty subrelation of ✔ p ✡ ☛ m ✡ ☛ ✘ . Then ✭ ✝ ★ ✭ ✝ ✞ ✔ p ✡ ☛ ✘ which contradicts our assumptions. Therefore, for every ✭ ❜ a0 , we have ✭ ✧ ✔ p ✡ ☛ m ✡ ☛ o ✡ ☛ f ✘ ✝ ✞ a116 ✁ ✔ d ✘ ❭ ✭ , which means that a0 ❭ a0 d. a0

Lemma 7 If ✭ d ✞ ✭ o and ✭ d ✧ ✔ oo ✡ ☛ dd ✡ ☛ ss ✡ ☛ ✘ ✞ ✔ od ✘ then a0 ❭ a115 or a0 is NP-complete.

Proof. As in the previous lemmas, it can be shown that ✔ od ✘ ❭ ✭ d ❭ ✔ pp ✡ ☛ mm ✡ ☛ od ✘ . It follows that ✭ ✡ d ✞ a116 and ✔ pmod ✘ ✞ ✔ s ✘ ★ ✭ d ❜ a0 . Furthermore, ✔ oo ✡ ☛ dd ✡ ☛ ff ✡ ☛ ✘ ✞ ✔ ✔ s ✡ ☛ ✘ ★ ✔ pmod ✘ ✘ ✡ ❜ a0 and ✔ od ✘ ✞ ✔ pmod ✘ ✧ ✔ oo✡ ☛ dd✡ ☛ ff ✡ ☛ ✘ ❜ a0 . By Lemma 2, we know that every ✭ ❜ a0 satisfies condition 3) of a115 . Suppose some ✭ ✜ ❜ a0 does not satisfy condition 1) of a115 . Then ✭ ✜ can be chosen so that ✔ s ✡ ☛ f ✡ ☛ ✘ ❭ ✭ ✜ ❭ ✔ ✏ pmodss ✡ ☛ ff ✡ ☛ ✘ or ✔ os ✡ ☛ ✘ ❭ ✭ ✜ ❭ ✔ ✏ pmodss ✡ ☛ ff ✡ ☛ ✘ . If ✔ f ✘ ❭ ✭ ✜ then ✔ ff ✡ ☛ ✘ ✞ ✔ ✭ ✜ ✧ ✔ oo ✡ ☛ dd ✡ ☛ ff ✡ ☛ ✘ ✘ ✡ ❜ a0 which contradicts our assumptions. Further, if ✔ od ✘ ✝ ❭ ✭ ✜ then ✭ ✜ ✧ ✔ oo ✡ ☛ dd ✡ ☛ ff ✡ ☛ ✘ ✞ ✔ f ✡ ☛ ✘ ❜ a0 , a contradiction. Therefore we may assume that ✔ ods ✡ ☛ f ✡ ☛ ✘ ❭ ✭ ✜ ❭ ✔ ✏ pmodss✡ ☛ f ✡ ☛ ✘ . Now it can be checked that ✭ ✝ ✞ ✭ ✜ ✧ ✔ ✭ ✟ ✜ ✜ ★ ✔ o ✡ ☛ d ✡ ☛ ✘ ✘ satisfies ✔ ods ✡ ☛ f ✡ ☛ ✘ ❭ ✭ ✝ ❭ ✔ pmods ✡ ☛ f ✡ ☛ ✘ . Then ◆ ✭ ✝ ❨ is NPcomplete by Proposition 2(2). One can proceed similarly if condition 2) of a115 fails in a0 . a0

It remains to consider the case when each non-trivial ✭ ❜ a0 satisfies ✭ ✧ ✔ ss ✡ ☛ ✘ ✝ ✞ a116 .

Lemma 8 If ✭ ✧ ✔ ss ✡ ☛ ✘ ✝ ✞ a116 for any non-trivial ✭ ❜ a0 then a0 ❭ ✤ a80 for some ✎ ❯ ❚ ❯ ✣ .

Proof. Case 1. ✭ p ✧ ✔ ss✡ ☛ ✘ ✞ ✔ s✡ ☛ ✘ .

We have ✔ ps ✡ ☛ ✘ ❭ ✭ p and ✔ s ✘ ✝ ❭ ✭ p. Let ✭ ✜ ✞ ✔ s✡ ☛ ✘ ★ ✭ p ❜ a0 . Then it is easy to check that ✔ pmod✡ ☛ s✡ ☛ f ✡ ☛ ✘ ❭ ✭ ✜ , and that ✭ ✜ ✧ ✔ ✏ s ✘ ✞ a116 . It follows that ✭ ✜ ✞ ✔ pmod ✡ ☛ s ✡ ☛ f ✡ ☛ ✘ , since otherwise ✭ ✡ ✜ is non-empty and ✭ ✡ ✜ ✧ ✔ ss ✡ ☛ ✘ ✞ a116 . No nonempty subrelation of ✔ pmod ✡ ☛ f ✡ ☛ ✘ can belong to a0 . Therefore, for any ✭ ❜ a0 , ✭ ✧ ✔ pmod ✡ ☛ f ✡ ☛ ✘ ✝ ✞ a116 implies ✔ s ✡ ☛ ✘ ❭ ✭ . Hence a0 ❭ ✤ ✜ .

Case 2. ✭ d ✧ ✔ ss ✡ ☛ ✘ ✞ ✔ s ✡ ☛ ✘ .

The proof is similar to Case 1; the only change is that ✭ ✜ ✞ ✭ d ★ ✔ s✡ ☛ ✘ , andwe deduce that ✭ ✜ ✞ ✔ p✡ ☛ m✡ ☛ o✡ ☛ ds✡ ☛ f ✘ , and, hence, a0 ❭ ✤ ✝ .

Case 3. ✭ o ✧ ✔ ss ✡ ☛ ✘ ✞ ✔ s ✡ ☛ ✘ .

In view of Cases 1 and 2 we may assume that ✔ os ✡ ☛ ✘ ❭ ✭ o ❭ ✔ ✏ p✡ ☛ mm✡ ☛ od✡ ☛ s✡ ☛ ff ✡ ☛ ✘ . Let ✭ ✜ ✞ ✔ s✡ ☛ ✘ ★ ✭ o. It is easy to check that

• Since ✭ ✡ ✜ ✝ ✞ ✔ oo ✡ ☛ ✘ , we obtain ✭ ✜ ❭ ✔ p ✡ ☛ m ✡ ☛ od ✡ ☛ s ✡ ☛ f ✡ ☛ ✘ . It can straightforwardly be verified that if ✭ ✜ ✝ ✞ ✔ od ✡ ☛ s ✡ ☛ f ✡ ☛ ✘ , then ✭ ✝ ✞ ✔ ✭ ✜ ★ ✭ ✜ ✘ ✡ ❜ a0 , but ✭ ✝ ✧ ✔ pp✡ ☛ ss✡ ☛ ✘ ✞ ✔ pp✡ ☛ ✘ , which contradicts the assumption made. Therefore, ✭ ✜ ✞ ✔ od ✡ ☛ s ✡ ☛ f ✡ ☛ ✘ , and ✔ pmod ✡ ☛ s ✡ ☛ f ✡ ☛ ✘ ✞ ✭ ✜ ★ ✭ ✜ ❜ a0 . Hence, for any ✭ ❜ a0 , ✭ ✧ ✔ pmod ✡ ☛ f ✡ ☛ ✘ ✝ ✞ a116 implies ✔ s✡ ☛ ✘ ❭ ✭ , and we have a0 ❭ ✤ ✜ .

Case 4. ✭ m ✧ ✔ ss ✡ ☛ ✘ ✞ ✔ s ✡ ☛ ✘ . Similarly to Case 3, we infer that a0 ❭ ✤ ✜ .

Case 5. ✔ s ✘ is contained in each of ✭ p, ✭ d, ✭ o, and ✭ m. We have ✭ f ✧ ✔ ss✡ ☛ ✘ ✝ ✞ a116 . Then it follows that if ✔ s ✘ ❭ ✭ f then a0 ❭ ✤ ✢ . Otherwise, ✔ s ✡ ☛ ✘ ❭ ✭ f and we have a0 ❭ ✤ ✟ . a0

3.3 The d✆ o case

Suppose ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ d ✖ d ✡ ☛ ❨ . We give a sketch of a proof that either a0 is contained in a0 d or in ✄ d (and therefore is tractable), or else it contains ✔ oo ✡ ☛ ✘ or ✔ pp ✡ ☛ ✘ (and then it is NP-complete by Proposition 2(1)).

Let ✷ ✝ ❳ ✔ a0 ✘ ✞ ◆ ✭ ✡ ❘ ✭ ❜ a0 ❨ . First it can be shown that either ✷ ✝ ❳ ✔ a0 ✘ is contained in a0 d or in ✄ d, or else a0 contains ✔ oo ✡ ☛ ✘ or ✔ pp ✡ ☛ ✘ . Then one can check, similarly to Lemma 3, that if there exists a non-trivial ✭ ❜ a0 such that ✭ ✧ ✔ dd ✡ ☛ ✘ ✞ a116 then ✭ satisfies ✭ ❭ ✔ ✏ ss ✡ ☛ ✘ or ✭ ❭ ✔ ✏ ff ✡ ☛ ✘ , and in this case, once again, a0 is contained in a0 d or in ✄ d, respectively, or else a0 contains ✔ oo ✡ ☛ ✘ or ✔ pp ✡ ☛ ✘ . Finally, we assume that each non-trivial ✭ ❜ a0 satisfies ✭ ✧ ✔ dd ✡ ☛ ✘ ✝ ✞ a116 , and then the required result can be proved by analysing the minimal relations ✭ p, ✭ m, ✭ o, ✭ s, and ✭ f, as in the proof of Lemma 8.

The case ❅ ✚ ✷ ✔ a0 ✘ ✞ ◆ ✏ ✖ o ✖ o✡ ☛ ❨ is very similar to the previous one. The only essential difference is that the relation ✔ pp ✡ ☛ ✘ cannot belong to a0 ; otherwise we get ✔ o ✘ ★ ✔ o ✘ ✞ ✔ pmo ✘ and ✔ p ✘ ✞ ✔ pp✡ ☛ ✘ ✧ ✔ pmo ✘ ❜ a0 , a contradiction.

4 Conclusion

We have proved that any so far unknown tractable fragment of Allen's algebra can contain no other basic relation than ✔ ✏ ✘ . We believe that, by extending the algebraic techniques used to establish our result, it will be possible to show that there are in fact no other forms of tractability in Allen's algebra. In other words, we conjecture that all maximal tractable subalgebras are already identified. However, the proof of this conjecture requires a more elaborate algebraic argument than the proofs in this paper, since in the general case we have no particular relation to start with. Algebraic techniques similar to the one used in this paper can also be applied to the study of the complexity in other temporal and spatial formalisms.