Classification Transfer for Qualitative Reasoning Problems

1 Introduction

A classical line of enquiry within Artificial Intelligence (AI) considers an agent's ability to reason about time and space, and a wide variety of formalisms for temporal and spatial reasoning are surveyed in [Dylla et al., 2017]. Famous such examples are the Interval Algebra of [Allen, 1983], the Region Connection Calculus of [Randell et al., 1992] and the Cardinal Direction Calculus of [Ligozat, 1998]. The central computational problem, designated the fundamental task of Qualitative Spatial and Temporal Reasoning in [Renz and Nebel, 2007], has to do with the consistency of some partial information given in one of these formalisms. In his article on Interval Algebras, Hirsch [1996] outlines The Really Big Complexity Problem associated to some subclass of a formalism, that is the (computational) complexity of its consistency problem. The complexity of the entire formalism is usually too blunt a measure, for example the Point Algebra [Vilain and Kautz, 1986] has long been known to be tractable, while the Interval Algebra is NP-complete [Nebel, 1995]. Much more interesting is a map of the complexity-theoretic landscape in terms of subclasses of the formalism. In the case of the Interval Algebra the natural classes of concern are subsets of disjunctions of the basic relations, and there are then a priori 2213 such classes requiring a complexity classification. The tower representation produces unfortunate typography and the relevance of this number is only in its forbidding largeness, so let us replace it henceforth with a /. This classification problem for the Interval Algebra tapped into a rich vein inspiring the popular paper of Nebel and B¨urckert [1995], who identified a class of relations within the /-many that is maximally tractable, in the sense that its consistency problem is in P, yet if one adds any other relation from the log(/)-many the problem becomes NP-complete. This maximal class was named ORD-Horn and owes its tractability to a variant of the local consistency method by which Horn Satisfiability is resolved in P (a very fast algorithm for the latter is given in [Dowling and Gallier, 1984]). A complete classification showing the 18 maximal tractable classes among the /-many was finally given in [Krokhin et al., 2003].

A constraint satisfaction problem (CSP) is a computational problem in which the input consists of a finite set of variables and a finite set of constraints, and where the question is whether there exists a mapping from the variables to some fixed domain such that all the constraints are satisfied. The set of relations that is allowed to formulate the constraints in the input is called the constraint language. It is well-known that the consistency problem for some subclass of a temporal or spatial formalism is an example of a CSP with a constraint language over an infinite domain. Indeed, the modern and algebraic study of CSPs has played an important role in answering some of these classical questions from AI, e.g. for the Interval Algebra in [Krokhin et al., 2003] (though other times, e.g. for the RCC-5, such questions were answered by exhaustive and computer-driven search through roughly /- many cases [Jonsson and Drakengren, 1997]).

By now the literature on infinite-domain CSPs is beginning to mature. Much of the modern work has been motivated by questions originating in AI. The constraint languages are chosen according to what mathematical methods they might be amenable to, rather than their being idiosyncratic to spatio-temporal reasoning. These are often ordinary structures of arithmetic, but may be more elaborate mathematical constructions (such as the Fra¨ıss´e limits used for RCC-8 in [Bodirsky and W¨olfl, 2011]). This need not be a hindrance, after all the Interval Algebra can be embedded in the real line and the majority of the spatio-temporal formalisms (unsurprisingly) have a natural interpretation in some Euclidean space. The notion of definability is usually in first-order logic rather than simple disjunctions of atomic relations. Outstanding work in this direction includes the complexity classifications for the temporal CSPs, fo-definable in (Q;<) [Bodirsky and K´ara, 2010] and discrete temporal CSPs, fo-definable in (Z;<) [Bodirsky et al., 2015]. In these examples, a complexity-theoretic dichotomy, between P and NP-complete, is observable across the different constraint languages. Such a dichotomy is reminiscent of the case for finite-domain CSPs as detailed in the recently-proved [Bulatov, 2017; Zhuk, 2017] Feder-Vardi Conjecture [Feder and Vardi, 1999]. While infinite-domain CSPs may have much higher complexity, e.g. be undecidable [Bodirsky and Grohe, 2008], in well-behaved cases many of the methods developed for the finite-domain are applicable. Thus, the technology exists to answer many instances of the Really Big Complexity Question. Some of the tools and techniques reappear over and again, for example tractability based on Horn's restriction [Horn, 1951] (see [Bodirsky et al., 2012]). Yet, the proofs appearing for the Interval Algebra in [Krokhin et al., 2003] and the temporal CSPs of [Bodirsky and K´ara, 2010] are quite distinct and often rely on local ad-hoc constructions. The observation that the Interval Algebra can be embedded in the (real or) rational line belies a new hope. Can a small number of existing classifications allow the simple derivation of other classifications? Could the classifications for the Interval Algebra and temporal CSPs be obtained, in some form, as a corollary of the other? The answer to this question is (a mildly-qualified) yes, so long as we can assume the basic relation m to be in the language defined in the Interval Algebra, and < to be in the language defined in (Q;<). More interesting is to use existing classifications to simply derive solutions to open problems. In this vein, we will look at the Rectangle Algebra of [Guesgen, 1989; Mukerjee and Joe, 1990] and its generalisation to the rdimensional Block Algebra of [Balbiani et al., 2002].

ORD-Horn is known to be a tractable fragment not only for the Interval Algebra but also for its generalisations to the (2dimensional) Rectangle Algebra and (r-dimensional) Block Algebra [Balbiani et al., 2002]. In that paper it is noted that: "The problem of the maximality of this tractable subset [ORD-Horn] remains an open problem. Usually to prove the maximality of a fragment of a relational algebra an extensive machine-generated analysis is used. Because of the huge size ... we cannot proceed in the same way." Our method is able to answer that ORD-Horn is indeed maximally tractable for the Rectangle Algebra as well as the r-dimensional Block Algebra, without a computational search, but via knowledge of maximal classes from [Bodirsky and K´ara, 2010].

This paper is structured as follows. We introduce the preliminaries as well as the key notions of interpretations and homotopy in Section 2. Our principal results on classification transfer are given in Section 3, while we address maximal tractability of ORD-Horn in Section 4.

2 Preliminaries

Let B be a finite (relational) structure, that is a domain B embellished with a finite set of relations on that domain. The sequence of arities of these relations (together with their names)

constitutes the signature of B. Of course, one may equivalently think of B as a finite set of relations over the same domain. We may now give a formal definition of the constraint satisfaction problem when it is parameterised by a set of relations, equivalently a (relational) structure. The problem CSP(B), where B is known as the constraint language, is defined as follows:

Instance: A set V of variables and a set C of constraints of the form R(v1, . . . , vk), where k is the arity of R, v1, . . . , vk ∈ V and R a relation of B.

Question: Is there a function f : V → B such that (f(v1), . . . , f(vk)) ∈ R for every R(v1, . . . , vk) ∈ C?

First-order formulas φ over the signature τ (or, in short, τformulas) are inductively defined using the logical symbols of universal and existential quantification (∀ and ∃), disjunction (∨), conjunction (∧), negation (¬), equality, bracketing, variable symbols and the symbols from τ. The semantics of a first-order formula over some τ-structure is defined in the usual Tarskian style. When φ is a formula without free variables (a sentence), we write B |= φ to indicate that φ is true on B.

One can use first-order formulas to define relations over a given structure B: for a formula φ(x1, ..., xk) the corresponding relation R is the set of all k-tuples (t1, ..., tk) ∈ Bk such that φ(t1, ..., tk) is true in B. In this case we say that R is first-order definable over B. Note that our definitions are always parameter-free, i.e. we do not allow the use of domain elements in them. A structure A is said to be first-order definable over B when all of its relations are first-order definable in B, it is first-order expansion of B if it further includes all of the relations of B.

The fragment of first-order logic called primitive positive (pp) is that which involves only existential quantification (∃) and conjunction (∧). In particular, primitive positive formulas may involve equality, but no negation. An alternative definition of CSP(B), logspace equivalent to that which we gave, is furnished by the model-checking problem for primitive positive logic, on the fixed model B. In this formulation it is easy to see the following folkloric result.

Lemma 1 (Theorem 3.4 in [Jeavons, 1998]). If a structure A has a finite number of relations, all of which are pp-definable in B, then there is a polynomial-time reduction from CSP(A) to CSP(B).

Suppose now B is a structure with a finite number of relations, each of which has arity m (this set is referred to as the basic relations). Define B∨= to contain every m-ary relation R such that R(x) holds if and only if B1(x) ∨ · · · ∨ Bt(x) holds, where ∨ is the disjunction operator, {B1, . . . ,Bt} ⊆ B, and x = (x1, . . . , xm) is a variable vector. Clearly, B∨= is a constraint language with a finite set of relations. When B contains binary relations, we write x(B1 B2 . . . Bt)y instead of B1(x, y) ∨ B2(x, y) ∨ · · · ∨ Bt(x, y).

2.1 The Interval and Block Algebras

The interval algebra [Allen, 1983] (IA) is a formalism that is both well-known and well-studied in AI. The variable domain is

i.e. the variable domain consists of all closed intervals [a, b] of rational numbers. If I = [a, b] ∈ I, then we write I - for a and I + for b. The basic relations are the 13 relations defined in Table 1. We let IA denote the structure that is the set of basic interval relations over I. Clearly, the 8192 relations of the IA are the contents of the set IA∨=. Among them is the binary relation ⊤ which holds for all pairs of intervals.

Given a sequence S = (s1, . . . , sp), we let S[i] = si, 1 ≤ i ≤ p. Let p ≥ 1 be an integer. We will now define the p-dimensional block algebra (BAp). The domain is Ip . Given a sequence (r1, . . . , rp) where r1, . . . , rp are relations of IA, we define the binary relation B(r1,...,rp) = {(X, Y ) ∈ (Ip )2 | X[i](ri)Y [i], 1 ≤ i ≤ p}. The basic relations in BAp constitute the structure BAp := {B(r1,...,rp) | r1, . . . , rp from IA} and the relations of BAp are the members of BA∨= p . We note that BA1 is the interval algebra and that BA2 is often referred to as the rectangle algebra which we denote as RA with associated structure RA. Let us note here that, for each p, BA∨= p coincides with the set of binary relations first-order definable over BAp, since this latter structure admits quantifier elimination.

2.2 Interpretations

A first-order interpretation I of a structure B over signature τ, in a structure A over signature σ, is a triple (k, δ, g) where k ∈ N is the dimension of the reduction, δ is a firstorder definable subset of Ak and g is a surjection from δ to B. We further require that, for every s-ary relation S in B, as well as for equality, there is a first-order definable φ(x11 , . . . , xk1 , . . . , x1s , . . . , xks ) over σ so that, for all (x11 , . . . , xk1 ), . . . , (x1s , . . . , xks ) ∈ δ:

When φ is the first-order definition of R in B, then S is the relation defined by φI in A, where φI is built from φ by substituting each atomic formula in the first-order definition by its translation under I. We will be most interested in the situation where all these fo-definitions are in fact pp-definitions, in which case we talk of a primitive positive interpretation.

I1 := (i, δ1, g1), . . . , Ij := (i, δj, gj), of B in A; together with J := (j, ϵ, h), a j-ary interpretation of C in B. Then we can define J ◦ (I1, . . . , Ij) in the following fashion. Consider the partial ij-ary surjection h(g1, . . . , gj), defined through h(g1(x1, . . . , xi), . . . , gj(xij-i+1, . . . , xij)), from Aij to C. Note that it is defined precisely on ijtuples satisfying δ1(x1, . . . , xi)∧. . .∧δj(xij-i+1, . . . , xij)∧ ϵ(g1(x1, . . . , xi), . . . , gj(xij-i+1, . . . , xij)). Indeed, interpretations may be seen as partial surjections and partial surjections are closed under the composition we have just seen. The partial surjection h(g1, . . . , gj) bestows a natural map from atomic relations of C to relations of A but there is no guarantee of nice (pp-, or even fo-) definability in A. Even the definition we have given for the domain of h(g1, . . . , gj) is not syntactic in the sense of fo-definability. However, let us now consider the case C = A in which h(g1, . . . , gj) is itself pp-definable, in the sense that the ij + 1-ary relation on A given by h(g1(x1, . . . , xi), . . . , gj(xij-i+1, . . . , xij)) = y is ppdefinable. This is exactly J ◦(I1, . . . , Ij) being pp-homotopic with the identity interpretation (what we may paraphrase in future as simply "pp-homotopy", when the context is clear) 1 . In this case, it is clear that domain and relations, for J ◦ (I1, . . . , Ij), are pp-definable. For example, the domain formula is ∃y h(g1(x1, . . . , xi), . . . , gj(xij-i+1, . . . , xij)) = y and a k-ary relation R of A gives rise to its interpreting ijkary relation of A given by

where here subscripts are read lexicographically before superscripts.

By way of example, let us consider the binary interpretation of IA∨= in (Q; <), given by I = (2, x < y, h), in which h(X-,X+) = [X-,X+] maps an ascending pair of rationals to the interval whose endpoints they specify. It is easy to verify that each of the relations of IA∨= is first-order definable in (Q;<). Indeed, each of the (basic) relations of IA is pp-definable in (Q;<) (see the third column of Table 1). Thus IA is even pp-interpretable in (Q; <).

Two structures are said to be mutually pp-interpretable when there is a pp-interpretation of each in the other. When these further satisfy the pp-homotopy condition then we will have enough for classification transfer.

3 Classification Transfer

Let C be a structure with finite relational signature. By the classification project for C we mean a complexity classification for CSP(B) for all first-order expansions B of C that have finite relational signature. For instance, the classification project for the random graph is treated in [Bodirsky and Pinsker, 2015] and the classification project for (Q; <) is treated in [Bodirsky and K´ara, 2010].

1 We are following the terminology from [Ahlbrandt and Ziegler, 1986].

Sometimes, it is possible to derive the (complexity) classification project for a structure C from the (complexity) classification project for another structure D. The following lemma is our principal tool and gives us the method by which we can demonstrate classification transfer.

Lemma 2. Suppose D has j i-ary primitive positive interpretations I1, . . . , Ij in C, and C has a j-ary primitive positive interpretation J in D such that J ◦(I1, . . . , Ij) is pp-homotopic to the identity interpretation of C. Then for every first-order expansion C ′ of C there is a first-order expansion D′ of D such that C ′ and D′ are mutually pp-interpretable.

Proof. Let I1 = (i,U1, g1), . . . , Ij = (i,Uj, gj) and J = (j, V, h) be the primitive positive interpretations from the statement, and let C ′ be a first-order expansion of C. Then we set D′ to be the expansion of D that contains for every k-ary atomic formula (derived from atomic relation R) in the signature of C ′ the jk-ary relation S defined as follows. When φ is the first-order definition of R in C, then S is the relation defined by φJ in D (recall that φJ is built from φ by substituting each atomic formula in the first-order definition by its translation under J).

We claim that C ′ is primitive positive interpretable in D′ , indeed by (j, V, h). First note that V is primitive positive definable in D′ since D′ is an expansion of D. An atomic formula ψ with free variables x1, . . . , xk in the signature of C ′ can be interpreted in D′ as follows. We replace the relation symbol in ψ by its definition in C, and obtain a formula φ in the language of C. Let S be the symbol in the language of D′ for the relation defined by φJ(x11 , . . . , xj1 , . . . , x1k , . . . , xjk ) over D′ . Then indeed S(x11 , . . . , xj1 , . . . , x1k , . . . , xjk ) is a defining formula for ψ, because

for all a1, . . . , ak ∈ V .

Conversely, we claim that D′ has each of the primitive positive interpretations (i,U1, g1), . . . , (i,Uj, gj) in C ′ . As before, each of U1, . . . ,Uj is primitive positive definable in C ′ since C ′ is an expansion of C. Let φ be a k-ary atomic formula in the (relational) signature of D′ . If φ is already in the signature of D, then there is a primitive positive interpreting formula in C and therefore also in C ′ . Otherwise, by the definition of D′ , the relation symbol in φ has arity jk′ , and has been introduced for a (k ≤) k′ -ary relation R from C ′ (if k < k′ some coordinates were identified in R). We have to find a defining formula having ijk free variables, but we will build one with ijk′ variables in which some have to be identified in line with our previous comment. Let θ(x0, x1, . . . , xij) be the primitive positive formula of arity ij + 1 that shows that h(g1(x1, . . . , xi), . . . , gj(xij-i+1, . . . , xij)) = x0 is primitive positive definable in C. Then the defining formula for the atomic formula φ(x1 , . . . , xk′ ), where some of these variables are identified, is ∃x1 , . . . , xk′ (R(x1 , . . . , xk′ ) ∧

∧k′ ℓ=1 θ(xℓ , xℓ1 , . . . , xℓij )), where here subscripts are read lexicographically before superscripts.

Corollary 1. Suppose D has j i-ary primitive positive interpretations I1, . . . , Ij in C, and C has a j-ary primitive positive interpretation J in D such that J ◦ (I1, . . . , Ij) is pphomotopic to the identity interpretation of C. Then for every first-order expansion C ′ of C there is a first-order expansion D′ of D such that there are polynomial time reductions between CSP(C ′ ) and CSP(D′ ).

Proof. Lemma 2 tells us that for every first-order expansion C ′ of C there is a first-order expansion D′ of D such that C ′ and D′ are mutually pp-interpretable. Thus it is now incumbent on us only to argue that there are polynomial time reductions between CSP(C ′ ) and CSP(D′ ). This essentially generalises the proof of (the hitherto unproved) Lemma 1 and is most easily given in the alternative definition of the CSP as the model-checking problem for primitive positive logic. Let J ′ = (j,U, g) be a pp-interpretation of C ′ in D′ where U is given as an j-ary pp-formula φU and each k-ary relation R of C ′ is given as a jk-ary formula φR. From an instance of CSP(C ′ ), that is a pp-sentence in n variables, we build a pp-sentence in jn variables, in which each variable v becomes a sequence v1 , . . . , vj that is constrained by φU, and where each atom of the form R(v1, . . . , vk) is replaced by φR(v1 1 , . . . , vj1 , . . . , v1 k , . . . , vjk ). This procedure can clearly be made in polynomial time and that it is indeed a reduction follows from it being derived from the corresponding interpretation. The argument for reducing CSP(D′ ) to CSP(C ′ ) is dual, and the result follows.

3.1 The Interval Algebra

We now investigate classification transfer for the Interval Algebra.

Lemma 3. There are 2 unary pp-interpretations, I1 and I2, of (Q;<) in (I, s, f), and a binary pp-interpretation J of (I, s, f) in (Q; <), so that J ◦ (I1, I2) is pp-homotopic to the identity.

Proof. Let I1 and I2 be (1,⊤, p1) and (1,⊤, p2), where p1 and p2 are the binary projections to start and finish point of the interval, respectively. Let J be (2,X- < X+, h) where h(X-, X+) = [X-, X+] maps pairs of points X- < X+ to the interval they specify in the line.

Define (X < Y )I1 and (X < Y )I2 by ∃Y ′ ,W (Y (s)Y ′ ∧ X(s)W ∧ Y ′ (f)W ) and ∃X′ ,W (X(f)X′ ∧ Y (f)W ∧ X′ (s)W ), respectively. Define ((u1, u2)(s)(v1, v2))J by u1 = v1 ∧ u2 < v2 and ((u1, u2)(f)(v1, v2))J by u1 < v1 ∧ u2 = v2.

Define (X = Y )I1 as X(s)Y and (X = Y )I2 as X(f)Y . Define ((u1, u2)(≡)(v1, v2))J as u1 = v1 ∧ u2 = v2. Now J ◦ (I1, I2) maps ([X-,X+], [Y -, Y +]) to [Z -,Z +] := [X-, Y +] and pp-homotopy is given by X(s)Z∧Y (f)Z.

Let us make the simple observation that all the basic relations of IA are pp-definable with <. Now we can derive the following from Corollary 1.

Corollary 2. Let Γ be first-order definable in IA containing the basic relations s and f. Then either CSP(Γ) is in P or it is NP-complete.

Noting that s and f are pp-definable in m, though the converse is false, we note that we could have derived the previous corollary with m in place of s and f. Corollary 2 should be compared to the main result in [Krokhin et al., 2003]. They are formally incomparable, since Corollary 2 requires certain basic relations to be present, while [Krokhin et al., 2003] only considers binary first-order definable relations.

3.2 The Rectangle Algebra

We now investigate classification transfer for the Rectangle Algebra. We will use the obvious fact that certain relations are pp-definable from the basic relations. Let (s,⊤) := (s, p) ∨ . . . ∨ (s,≡) be the disjunction with all 13 basic relations relations of the IA in the second coordinate. Then X(s,⊤)Y iff ∃Z (X(s, p)Z ∧Z(s, p⌣)Y ). Note also that, e.g., (s,⊤) is pp-definable in RA by ∃Z (X(≡, d)W ∧ Y (≡, d)W ∧ X(s, ≡)W).

Lemma 4. There are 4 unary pp-interpretations, I1, I2, I3 and I4, of (Q;<) in RA, and a 4-ary pp-interpretation J of RA in (Q;<), so that J ◦ (I1, I2, I3, I4) is pp-homotopic to the identity.

Proof. For i ∈ [4], let Ii be (1,⊤, pi), where pi is the 4-ary projection to the ith coordinate. Let J be (4,X- < X+ ∧ Y - < Y +, h) where h(X-,X+, Y -, Y +) = r maps two pairs of intervals to the rectangle they specify in the plane.

Define (X < Y )Ii as follows.

Define ((u1, u2, u3, u4)(s, ⊤)(v1, v2, v3, v4))J by u1 = v1 ∧ u2 < v2 and ((u1, u2, u3, u4)(f, ⊤)(v1, v2, v3, v4))J by u1 < v1 ∧ u2 = v2. The other relations of RA are defined in the obvious fashion.

Define (X = Y )I1 , (X = Y )I2 , (X = Y )I3 and (X = Y )I4 as X(s,⊤)Y , X(f,⊤)Y , X(⊤, s)Y and X(⊤, f)Y , respectively. Define ((u1, u2, u3, u4)(≡)(v1, v2, v3, v4))J as u1 = v1 ∧ u2 = v2 ∧ u3 = v3 ∧ u4 = v4. Now, for i ∈ {1, 2, 3, 4}, let Wi = (Xi, Yi) where Xi and Yi are intervals and not rectangles. J ◦ (I1, I2, I3, I4) maps

Now we can derive the following from Corollary 1.

Corollary 3. Let Γ be first-order definable in RA containing the basic relations (s, p), (s, p⌣), (f, p), (f, p⌣), (p, s), (p⌣, s), (p, f) and (p⌣, f). Then either CSP(Γ) is in P or it is NP-complete.

4 Maximal tractability and ORD-Horn

A set of relations Γ, over the same domain, is described as maximally tractable among ∆ ⊇ Γ, if every finite subset of Γ gives a structure B so that CSP(B) is in P; while for each R ∈ ∆ \ Γ, there is a finite subset of Γ given by B, so that CSP(B; R) is NP-hard.

4.1 The Rectangle Algebra

In [Balbiani et al., 2002], the strongly pre-convex relations are tied precisely to ORD-Horn, yet maximal tractability of this class, among RA∨=, remains open. Here we settle the question by proving that ORD-Horn is indeed maximally tractable in the Rectangle Algebra. We will do this by using maximal tractability among languages first-order definable in (Q; <) (where in fact ORD-Horn is not maximally tractable).

A formula is called ll-Horn if it is a conjunction of formulas of the following form

where 0 ≤ k, l. ORD-Horn is the subclass in which we insist at most a single atom appears in each sequent. Note that k or l might be 0: if k = 0, we obtain a formula of the form z1 < z0∨· · ·∨zl < z0 or (z1 < z0∨· · ·∨zl < z0∨(z0 = z1 = · · · = zl)), and if l = 0 we obtain a disjunction of disequalities. Also note that the variables x1, . . . , xk, y1, . . . , yk, z0, . . . , zl need not be pairwise distinct. On the other hand, the clause z1 < z2 ∨ z3 < z4 is an example of a formula that is not ll-Horn. The dual class, dual -ll -Horn, can be defined as ll -Horn, but with all < replaced by >. The following result is from [Bodirsky and K´ara, 2010] using the characterisation of [Bodirsky and K´ara, 2015].

Lemma 5. The class of relations definable in ll -Horn (resp., dual -ll -Horn) is a maximally tractable subclass of relations fo-definable in (Q;<).

Lemma 6. The relation x = y ⇒ u = v sits in precisely two maximally tractable classes of constraint languages with respect to relations fo-definable in (Q;<), which are those whose relations are definable in ll -Horn and those whose relations are definable in dual -ll -Horn.

Proof. Here we can not avoid some parlance from [Bodirsky and K´ara, 2010]. Let pp (resp., dual -pp) be the binary operation on Q that maps (x, y) to x, if x < 0, and y, otherwise (resp., maps (x, y) to y, if x < 0, and x, otherwise). A relation is violated by an operation if, when the operation is applied component-wise to some tuples in the relation, one can obtain a tuple that is not in the relation. Reading from Figure 9 in [Bodirsky and K´ara, 2010], one sees that the present lemma follows if we can prove that pp and dual -pp both violate x = y ⇒ u = v. To see this for pp, consider the tuples (-1, -1, 2, 2) and (1, 2, 1, 2) for which pp produces the tuple (-1, -1, 1, 2) which is not in the relation. The case dual -pp is achingly similar.

Call a definition in ll -Horn minimal if all of its clauses are needed and none can be replaced by one with a smaller sequent on the right-hand side of an implication. We may thus assume that the z0, . . . , zl as in the definition are distinct in each clause. Note that relations definable in ORD-Horn over (Q;<) is a strict subset of both those relations definable in ll -Horn and those relations definable in dual -ll -Horn.

Theorem 1. The class ORD-Horn on the Rectangle Algebra is maximally tractable among the binary relations fodefinable in RA.

Proof. We know from [Balbiani et al., 2002] that the ORDHorn relations among RA∨= give a CSP that is tractable. Let R be some binary relation not definable in ORD-Horn and let J be as in Lemma 4. Suppose we translate R to an 8ary relation S over (Q;<) via J, and let us make the similar translation for all ORD-Horn relations of the Rectangle Algebra, which will become the set of relations Γ fo-definable in (Q;<). Owing to Lemma 4, we need only argue that CSP(Q; Γ, S) is NP-hard (we abuse notation by presuming Γ defines also a set of relations over I).

Since the (ORD-Horn) relation {s,≡, s⌣} × (⊤ \ {s,≡ , s⌣} translates to X- = U - ⇒ Y - = V - in Γ, we can deduce from Lemma 6 that the only maximally tractable classes for relations fo-definable in (Q;<) that {S} ∪ Γ can sit in are those corresponding with ll and dual -ll . In particular, if S is outside of these classes then it follows immediately that CSP(Q; Γ, S) is NP-hard. Let us therefore assume w.l.o.g. that S is within ll , as the other case is dual, and we will seek a contradiction.

Let φ be some minimal ll -Horn specification of S. Consider some clause that is not ORD-Horn. It involves some sequent of the form either z1 < z0 ∨ . . . ∨ zl < z0 or z1 < z0 ∨ . . . ∨ zl < z0 ∨ z0 = z1 = . . . = zl where z0, z1, . . . , zl are distinct variables. Now, since R was binary, we know that some rectangle is mentioned twice among the z0, z1, . . . , zl. If some comparison involves (w.l.o.g.) I - and I +, then we can remove this and we contradict minimality (note that X- < X+ because we do not allow point-like intervals). Thus, if we are not already ORD-Horn we must have something of the form, again w.l.o.g., X- < Y - ∨X- < Y + ∨. . . in the sequent, but this can be simplified to X- < Y + ∨ . . . contradicting minimality. Thus the assumption that we be minimal actually makes us ORD-Horn.

4.2 The r-dimensional Block Algebra

Firstly, we will profit from studying certain automorphisms of the Block Algebra. An automorphism of a structure B is a permutation f on its domain so that, for all relations R of B, of arity k, and all k-tuples of domain elements x1, . . . , xk ∈ B, R(x1, . . . , xk) iff R(f(x1), . . . , f(xk)). The Interval Algebra IA enjoys all translation automorphisms, of the form [X-,X+] ↦→ [q + X-, q + X+], for any q ∈ Q. The Block Algebra BAr enjoys these similarly, independently for each of its axes. That is, BAr has all automorphisms of the form ([X1 ,X+ 1 ], . . . , [Xr ,X+ r ]) ↦→ ([q1 + X1 , q1 + X+ 1 ], . . . , [qr + Xr , qr + X+ r ]). In particular, there is an automorphism of BAr that translates one axis any amount, while leaving the other axes where they are. An important property of automorphisms that we will use is that the truth of a first-order formula is invariant under an automorphism. That is, if φ(x1, . . . , xk) is a first-order formula over BAr, and h is an automorphism of BAr, then BAr |= φ(x1, . . . , xk) iff BAr |= φ(h(x1), . . . , h(xk)).

A hypercuboid is a polytope specified in k-dimensional space by the intersection of intervals ci ≤ xi ≤ di, for ci, di ∈ Q and i ∈ {1, . . . , k}. We are now in a position to extend our classification transfers to the r-dimensional Block Algebra.

Theorem 2. The class ORD-Horn on the r-dimensional Block Algebra is maximally tractable with respect to the binary relations fo-definable in BAr.

Proof. We follow the proof of the Theorem 1 up to the point where we consider some clause that is not ORD-Horn. It involves some sequent of the form either z1 < z0∨. . .∨zl < z0 or z1 < z0 ∨ . . . ∨ zl < z0 ∨ z0 = z1 = . . . = zl where z0, z1, . . . , zl are distinct variables. Now, since R was binary, we know that some hypercuboid is mentioned twice among the z0, z1, . . . , zl.

Case A. The same dimension is mentioned twice. This has been dealt with in the proof of Theorem 1.

Case B. No dimension is mentioned twice, but we have an atom of the form Xp < Y q , for p, q ∈ {+,-}, where I and J are different dimensions of the same hypercuboid. The r-dimensional Block Algebra enjoys an automorphism that translates the dimension associated with X while leaving unchanged all the other dimensions. Consider the evaluation that witnesses that the atom Xp < Y q is true whilst everything else in that clause is false. Now applying an automorphism we can falsify this atom while leaving all the others of that clause false (remember Xp is not repeated and Xp , where p ∈ {-,+} \ {p}, does not appear anywhere since then we would be in Case A). This demonstrates that φ does not specify a correct translation from the r-dimensional Block Algebra (the truth of φ should be invariant under these automorphisms).

Thus the assumption that we be minimal actually makes us ORD-Horn.

Note that our proof that ORD-Horn is maximally tractable works also for the Interval Algebra, where that result famously originated in [Nebel and B¨urckert, 1995]. The only change we need to make is with Lemma 6, because x = y ⇒ u = v can not originate from the Interval Algebra, but x = y ⇒ u = v ∧ y > x ∧ v > u can, and suffices for our argument. Note that the analog of Corollary 3 for the Block Algebra BAr proceeds with almost identical proof.

Acknowledgements

Manuel Bodirsky has received funding from the ERC under the European Community's Seventh Framework Programme (Grant Agreement no. 681988, CSP-Infinity), and the DFG-funded project 'Homogene Strukturen, Bedingungserf¨ullungsprobleme, und topologische Klone' (Project number 622397). Peter Jonsson is partially supported by the Swedish Research Council (VR) under Grant 201704112. Antoine Mottet is supported by the DFG programme QuantLA.