# A Fast Algorithm and Lower Bound for Temporal Reasoning

发布时间:2021-10-23 22:31:48

arXiv:0805.1473v1 [cs.AI] 10 May 2008

A FAST ALGORITHM AND LOWER BOUND FOR TEMPORAL REASONING

? MANUEL BODIRSKY AND JAN KARA Humboldt-Universit¨t zu Berlin, Germany a E-mail address: bodirsky@informatik.hu-berlin.de Charles University, Prague, Czech Republic E-mail address: kara@kam.mff.cuni.cz Abstract. We introduce a new tractable temporal constraint language, which strictly contains the Ord-Horn language of B¨rkert and Nebel and the class of AND/OR precedence u constraints. The algorithm we present for this language decides whether a given set of constraints is consistent in time that is quadratic in the input size. We also prove that (unlike Ord-Horn) this language cannot be solved by Datalog or by establishing local consistency.

1. Introduction

Temporal reasoning plays an important role in Arti?cial Intelligence. Almost any area in AI – for instance common-sense reasoning, natural language processing, scheduling, planning – involves some sort of temporal reasoning. In 1993, Golumbic and Shamir [15] listed applications of temporal reasoning problems in archeology, behavioral psychology, operations research, and circuit design. Since then, temporal reasoning became one of the benchmark applications of constraint processing in general [7]. Contributions to the ?eld have various background, e.g. database theory [30], scheduling [26], constraint satisfaction complexity [4], the theory of relation algebras [10, 23], combinatorics [15], and arti?cial intelligence [13]. This paper deals with temporal constraint languages. A temporal constraint language (TCL) is a countable collection of relations with a ?rst-order de?nition in (Q, <), the linear order of the rational numbers; a detailed de?nition is given in Section 2. One of the most fundamental TCLs is the so-called point algebra. This language contains relations for =, <, ≤, and =, interpreted over an in?nite dense linear order in the usual way. Vilain, Kautz, and van Beek showed that consistency of a given set of constraints over this language (aka the constraint satisfaction problem for this language) can be decided in polynomial time by local consistency techniques [24]. Later, van Beek described an algorithm that runs in O(n2 ), where n is the number of variables [29]. A considerably larger tractable TCL was introduced by B¨rkert and Nebel [27]. Their u language, called Ord-Horn, strictly contains the point algebra. B¨rkert and Nebel used u resolution to show that consistency of a set of Ord-Horn constraints can be decided in O(s3 ),

Key words and phrases: constraint satisfaction, temporal reasoning, Ord-Horn, graph algorithms, Datalog, AND/OR precedence constraints. Supported by Project 1M0021620808 of the Ministry of Education of the Czech Republic.

1

2

? M. BODIRSKY AND J. KARA

where s is the size of the input. They also showed that establishing path-consistency can be used to decide whether a given set of Ord-Horn constraints has a solution. Koubarakis [21] later presented an algorithm with a running time in O(s2 ). Ord-Horn is motivated by temporal reasoning tasks for constraints on time intervals. The study of constraints on intervals (which can be used to model temporal information about events) was initiated by Allen [1], who introduced an algebra of binary constraint relations on intervals. The complexity to decide the consistency of a given set of constraints from Allen’s algebra is NP-complete in general [1]. However, for several fragments of Allen’s interval algebra the consistency problem is decidable in polynomial time. All such fragments have been classi?ed [9,22]. It is well-known that every relation on intervals from Allen’s algebra can be translated to a relation on time points. Hence, algorithmic results for temporal reasoning with time points can be used for reasoning with time intervals as well. B¨rkert u and Nebel used this translation to identify one of the tractable fragments of Allen’s interval algebra, namely the set of all interval constraints that translate to Ord-Horn constraints on points. Another important temporal constraint language with applications in scheduling are AND/OR-precedence constraints [26]. An AND-constraint can be used to express that some job cannot be started before a set of other jobs has been completed. An OR-constraint can be used to express that a job cannot be started before one of a given set of jobs has been completed. Feasibility of AND/OR precedence constraints can indeed be modeled as a constraint satisfaction problem for a TCL: AND-constraints can be represented by conjunctions of formulas of the form x > y, and OR-constraints by formulas of the form x > x1 ∨ · · · ∨ x > xn . There are temporal constraint languages where one can not expect a polynomial time algorithm. A well-known TCL with an NP-complete consistency problem consists of a single ternary relation, the betweenness relation {(x, y, z) | x<y<z ∨ z<y<x}; another example of such an NP-complete language consists of the cyclic ordering relation, which is the ternary relation {(x, y, z) | x<y<z ∨ y<z<x ∨ z<x<y}. The constraint satisfaction problems for these two languages are listed as NP-complete in the book of Garey and Johnson [14]. We want to remark that the complexity of temporal constraint satisfaction problems for a ?xed and ?nite number of time points was completed recently [6]; however, the restriction to a ?nite number of time points changes the nature of the problem considerably. We present a new tractable TCL that strictly contains all Ord-Horn relations and all AND-OR precedence constraints (and also contains relations that are neither Ord-Horn nor AND-OR precedence constraints). Our language is de?ned by a universal-algebraic closure property, and we call it the class of ll-closed relations. We show in Section 3 that a relation is ll-closed if and only if it can be de?ned by a formula of the form (x1 = y1 ∧ · · · ∧ xk = yk ) → (z0 > z1 ∨ · · · ∨ z0 > zl ) , or (x1 = y1 ∧ · · · ∧ xk = yk ) → (z0 > z1 ∨ · · · ∨ z0 > zl ∨ (z0 = z1 = · · · = zl )) (where k and l might be 0). It has been shown in [3] that ll-closed constraints are a largest tractable language in the sense that every TCL that strictly contains one of our two languages has an NP-complete constraint satisfaction problem. The presented algorithm for ll-closed constraints has a running time that is quadratic in the size of its input. Traditionally, one of the main algorithmic tools in constraint satisfaction, and in particular in temporal reasoning, are local consistency techniques [1, 9, 15, 24, 27], for instance algorithms based on establishing path-consistency. Consistency based algorithms can be

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

3

formulated conveniently as Datalog programs [2, 12, 20]. Roughly speaking, Datalog is Prolog without function symbols, and comes from Database theory [11]. We show that, unlike Ord-Horn [27], ll-closed and dual ll-closed constraints can not be solved by a Datalog program. In our proof we apply a pebble-game argument that was originally introduced for ?nite domains [12, 20], but has been shown to generalize to a wide range of in?nite domain constraint languages, including TCLs [2]. This is interesting from a theoretical point of view: for constraint satisfaction problems of languages over a ?nite domain, all known algorithms are essentially based on algebraic algorithms or Datalog [12]. However, the algorithm we present for temporal reasoning is neither algebraic nor based on Datalog. Many proofs in this paper are moved to the appendix.

2. Temporal Constraint Languages

A (qualitative) temporal relation is a relation that is ?rst-order de?nable in an unbounded countable dense strict linear order. All such linear orders are isomorphic [18, 25], but for convenience we always use (Q, <), i.e., the dense linear order on the rational numbers1. An example of a temporal relation is the ternary Betweenness relation {(x, y, z) ∈ Q3 | (x<y ∧ y<z) ∨ (z<y ∧ y<x)} mentioned in the introduction. It is well-known that every temporal relation also has a quanti?er-free de?nition [18,25], i.e., we can de?ne every temporal relation with a formula that is a Boolean combination of literals of the form x < y (as above in the case of the Betweenness relation). A temporal constraint language (TCL) is an (at most countable) set of relation symbols R1 , R2 , . . . , where each relation symbol Ri is associated with an arity ki ≥ 2, and is interpreted by a ki -ary temporal relation. For simplicity, we use the same symbol for the relation symbol and the corresponding temporal relation. As an example, consider the set of binary relation symbols Γ0 := {=, ≤, <, =}, with the obvious interpretation over (Q, <). In this paper, we study the complexity of the validity problem for ?rst-order sentences of the form ?x1 , . . . , xn . φ1 ∧ · · · ∧ φp , where Φ := {φ1 , . . . , φp } is a set of atomic formulas with variables from x1 , . . . , xn and relation symbols from a ?xed constraint language Γ. This problem is also called the constraint satisfaction problem of Γ, CSP(Γ). The set Φ is called an instance of the CSP, and the atomic formulas φ1 , . . . , φp are called the constraints of the instance. For a constraint φ = R(x1 , . . . , xk ) we say that φ has arity ar(φ) = k and for xi from {x1 , . . . , xk } we say that φ is imposed on xi . A tuple (a1 , . . . , an ) ∈ Qn is called a solution for Φ if the assignment xi := ai satis?es all formulas in Φ. If there is no solution for Φ, then we say that Φ is unsatis?able, and satis?able (or consistent) otherwise. Thus, CSP(Γ) is the problem to decide whether a given set of constraints over relations from Γ is satis?able. Example. Let R(x, y, u, v) be the 4-ary temporal relation de?ned by (x=y ∧ y<u ∧ u=v) ∨ (x<y ∧ y<u ∧ u<v). Consider the instance Φ1 := {R(x1 , x2 , y1 , y2 ), R(x1 , x2 , y2 , y3 ), R(x1 , x2 , y3 , y1 )} of CSP({R}). It is easy to see that the sentence ?x1 , x2 , y1 , y2 , y3 φ∈Φ1 φ is true , and a solution to Φ1 is (0, 0, 1, 1, 1). It is straightforward to verify that whether or not an n-tuple t is a solution to an instance only depends on the weak linear order tp(t) de?ned on {1, . . . , n} by (i, j) ∈ tp(t)

1One could also consider dense linear orders on arbitrary in?nite base sets, e.g. (R, <); but it is easy to see all the results in this paper also apply to this case.

4

? M. BODIRSKY AND J. KARA

i? t[i] ≤ t[j]. We also say that t satis?es tp(t) 2. This observation leads to a natural way to represent temporal relations. If R is a k-ary temporal relation, R can be represented by a set R of weak linear orders on {1, . . . , k} as follows. For every k-tuple t ∈ R, the weak linear order tp(t) is contained in R. Conversely, for every weak linear order w in R there is a k-tuple t ∈ R such that w = tp(t). For example, the relation R in the example above can be characterized as the set of all tuples that satisfy either tp((0, 0, 1, 1)) or tp((0, 1, 2, 3)). Another natural way of representing a temporal relation is by specifying a formula de?ning the relation. However, general Boolean combinations of literals of the form x < y are obviously too expressive if we are interested in e?cient algorithms (it is NP-hard to decide whether such a formula represents a non-empty relation), so we have to restrict the set of all formulas appropriately; such a syntactic restriction will be presented in Section 3. A ?nite constraint language Γ is called tractable if CSP(Γ) can be solved in polynomial time (note that because Γ is ?nite this concept is independent from the actual representation of relations). The constraint language Γ0 mentioned at the beginning of this section, for example, corresponds to the well-studied point-algebra that we mentioned in the introduction, and is tractable. Classically, an in?nite constraint language Γ is called tractable if every ?nite subset of the constraint language is tractable. However, the algorithmic results established for the tractable languages in the present paper are stronger. An (?nite or in?nite) constraint language Γ is called globally tractable, if CSP(Γ) can be solved in polynomial time in the input size. In case of global tractability the actual representation of the relations in the instance matters. For TCLs we allow a relation to be represented in one of the following two ways: either as a set of weak linear orders as described above3 or as a formula with the syntactic restriction discussed in Section 3. If we are interested in global tractability, we measure the input size of a given instance Φ by the number n of variables in Φ and the weighted number m = R(x1 ,...,xk )∈Φ k|R| of constraints. This is, m denotes the size of the representations of all the constraints in the instance. In this paper we present an algorithm that shows that a large temporal constraint language is globally tractable (both with respect to the representation of constraint relations by tuples, and the representation of constraint relations by formulas). Even though this requires that we have to go into more detail as compared to a local tractability result, we would like to present the stronger global tractability result in this paper, because this allows us to relate our algorithm with previous algorithms in temporal reasoning, for example for Ord-Horn (which is an in?nite temporal constraint language). If Γ is the set of all temporal relations, then CSP(Γ) is well-known to be NP-complete. For containment in NP, note that one can verify in polynomial time whether a given weak linear order on n variables corresponds to a solution for a given instance Φ with n variables. We can therefore decide non-deterministically in polynomial time whether there exists a weak linear order on n elements and an (arbitrary) n-tuple t satisfying this weak linear order such that t is a solution to Φ. For NP-hardness, recall that already the constraint language that only contains a single relation symbol for the Betweenness relation is NPcomplete [14].

2The notation tp is motivated by the concept of (complete) types in model theory [18, 25]. 3The representation of a temporal relation by a set of weak linear orders corresponds to the standard

representation of a relation over a ?nite domain by its set of tuples, even though also for ?nite domains, a representation by formulas might sometimes be more natural, for example for boolean Horn satis?ability. For ?nite domains, it is an open problem whether the notion of tractability and the notion of global tractability coincide (and in fact it has been conjectured that they do [5]).

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

5

3. ll-closed Languages

We ?rst introduce fundamental concepts from model theory and universal algebra; they are standard, see e.g. [18, 28]. We say that a k-ary function (also called operation) f : Qk → Q preserves an m-ary relation R ? Qm if whenever R(ai , . . . , ai ) holds for m 1 all 1 ≤ i ≤ k, then R f (a1 , . . . , ak ), . . . , f (a1 , . . . , ak ) holds as well. If f preserves all m m 1 1 relations of a TCL Γ, we say that f is a polymorphism of Γ. Unary bijective polymorphisms are called the automorphisms of Γ; the set of all automorphisms of Γ is denoted by Aut(Γ). Let lex be a binary operation on Q such that lex(a, b) < lex(a′ , b′ ) if either a < a′ , or a = a′ and b < b′ . It is easy to see that the set of temporal relations preserved by lex is not a?ected by the choice of the binary operation lex if lex has the properties above. Thus for all the arguments in this paper, it does not matter which operation lex we are chosing. Also note that every such operation is by de?nition injective. Let ll be a binary operation on Q such that ll(a, b) < ll(a′ , b′ ) if one of the following cases applies. ? a ≤ 0 and a < a′ ? a ≤ 0 and a = a′ and b < b′ ? a, a′ > 0 and b < b′ ? a > 0 and b = b′ and a < a′ See Figure 1 for illustration. In diagrams like in Figure 1 we draw a directed edge from (a, b) to (a′ , b′ ) if ll(a, b) < ll(a′ , b′ ). Again, it is easy to see that the set of temporal relations preserved by ll is not a?ected by the exact choice of the binary operation ll. Also observe that every temporal relation that is preserved by ll is also preserved by lex. We say that a relation is ll-closed if it is preserved by ll. It is possible to decide algorithmically whether a constraint language is ll-closed. Proposition 3.1. Given a ?nite constraint language where all relations are represented as lists of weak linear orders, one can decide in polynomial time in the input size whether the constraint language is ll-closed. Similarly to the ll operation we can de?ne a dual ll operation, as depicted in Figure 1. To show that the language of all ll-closed relations is di?erent from the language of all dual ll-closed relations, we use the following two relations, which will be also of importance in later arguments. De?nition 3.2. We de?ne Rmin to be the ternary relation {(x, y, z) | x>y ∨ x>z}, and Rmax to be {(x, y, z) | x<y ∨ x<z}. Observe that Rmin (x, y, z) holds if and only if x is larger than the minimum of y and z. Similarly, Rmax (x, y, z) holds if and only if x is smaller than the maximum of y and z. It was shown in [26] and independently in [16] that CSP(Q, Rmax ) can be solved in polynomial time. For the proof of the next lemma we prove that the relation Rmin is ll-closed; the proof can be adapted easily to show that all k-ary relations de?ned by formulas of the form x1 > x2 ∨ · · · ∨ x > xk are ll-closed as well, which are the relations to model AND/OR precedence constraints. Proposition 3.3. The language of ll-closed relations does not contain the class of dual ll-closed relations and vice versa. The temporal constraint language of all ll-closed relations also contains the important class of Ord-Horn relations, introduced by B¨rckert and Nebel [27] to identify a tractable u

6

? M. BODIRSKY AND J. KARA

y

y

x

x

Figure 1: A visualization of the ll (left side) and the dual ll operation (right side). class of interval constraints. A relation is Ord-Horn if it can be de?ned by a conjunction of formulas of the form (x1 = y1 ∧ · · · ∧ xk = yk ) → x0 O y0 , where O ∈ {=, <, ≤, =}. It is always possible to translate interval constraints into temporal constraints [24]. If the translation of an interval constraint language falls into a tractable TCL, the interval constraint language is tractable as well. B¨rckert and Nebel showed that u the class of interval constraints having a translation into Ord-Horn temporal constraints is a largest tractable fragment of Allen’s interval algebra. Note that this does not imply that the class of Ord-Horn constraints is a largest tractable TCL on time points. Indeed, this is not the case. Proposition 3.4 below shows that the class of Ord-Horn constraints is ll-closed. Since the relation Rmin de?ned in this section is ll-closed but not Ord-Horn, the class of ll-closed constraints is strictly larger than Ord-Horn. Finally, we prove in Section 4 that ll-closed constraints are tractable. Proposition 3.4. All relations in Ord-Horn are preserved by ll and by dual ll. It turns out that a temporal relation is preserved by ll if and only if it can be de?ned by a class of formulas which we call ll-Horn formulas. This class properly extends the class of Ord-Horn formulas. A formula is called ll-Horn if it is a conjunction of formulas of the following form (slightly abusing terminology, we call these formulas the clauses of the ll-Horn formula) (x1 = y1 ∧ · · · ∧ xk = yk ) → (z0 > z1 ∨ · · · ∨ z0 > zl ) , or (x1 = y1 ∧ · · · ∧ xk = yk ) → (z0 > z1 ∨ · · · ∨ z0 > zl ∨ (z0 = z1 = · · · = zl )) where 0 ≤ k, l. Note that k or l might be 0: if k = 0, we obtain a formula of the form z0 > z1 ∨ · · · ∨ z0 > zl or (z0 > z1 ∨ · · · ∨ z0 > zl ∨ (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. Also note that the clause z1 > z2 ∨ z3 > z4 is not equivalent to any ll-Horn formula. Proposition 3.5. A temporal relation is ll-closed if and only if it can be de?ned by an ll-Horn formula. This motivates our the second way of representing the constraints in the input instance of the constraint satisfaction problem for an ll-closed T CL — the constraints may be given as ll-Horn formulas. We would like to remark that there are ll-closed temporal relations where the tuple representation is more succinct than the ll-Horn representation, and vice versa.

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

7

Note that since every Ord-Horn formula is obviously an ll-Horn formula, the algorithm we present for the ll-Horn representation in Section 4 strictly generalizes the existing algorithms for Ord-Horn constraints. For simplicity, we assume that in instances of the constraint satisfaction problem for ll-closed TCLs the formulas representing the constraints consist of just one clause (we can always transform a constraint into several constraints of this form).

4. An Algorithm for ll-closed Constraints

In this section we present an algorithm for ll-closed constraints. It is straightforward to ‘dualize’ the algorithm and all arguments, and we will therefore also obtain an algorithm for dual ll-closed constraints. One of the underlying ideas of the algorithm is to use a subroutine that tries to ?nd a solution where every variable has a di?erent value. If this is impossible, the subroutine must return a set of at least two variables that denote the same value in all solutions. It is one of the fundamental properties of ll-closed constraints that this is always possible. To formally introduce our algorithm we need the following de?nitions. Let φ = R(x1 , . . . , xk ) be an atomic formula where R is a temporal relation that is preserved by an operation f . Clearly, for all xi from x1 , . . . , xk the temporal relation de?ned by ?xi .φ is preserved by f as well. Therefore, if Φ is an instance of the CSP with constraints that are preserved by f , and y is a sequence of some of the variables of Φ, then Φ′ := {?y.φ | φ ∈ Φ} can also be viewed as an instance of the CSP with constraints preserved by f . We call Φ′ the projection of Φ to X \ y. Note that if Φ′ is unsatis?able, then Φ is unsatis?able as well. The i-th entry in a k-tuple t is called minimal if t[i] ≤ t[j] for every j ∈ [k]. It is called strictly minimal if t[i] < t[j] for every j ∈ [k] \ {i}. De?nition 4.1. Let R be a k-ary relation. A set of entries S ? [k] is called a min-set for the i-th entry in R if there exists a tuple t ∈ R such that the i-th entry is minimal in t, and for every j ∈ S it holds that t[i] = t[j]. We say that t is a witness for this min-set. Let R be a k-ary relation that is preserved by lex (recall that ll-closed constraints are preserved by lex as well), and suppose that the i-th entry has the min-sets S1 , . . . , Sl , for l ≥ 1, with the corresponding witnesses t1 , . . . , tl . Consider the tuple t := lex(t1 , lex(t2 , . . . lex(tl?1 , tl ))). Since the entry i is minimal in every tuple t1 , . . . , tl , and since lex preserves both < and ≤, it is also minimal in t. Because lex is injective, we have that t[i] = t[j] if and only if these two entries are equal in each tuple t1 , . . . , tl . Hence, the min-set for the i-th entry in R witnessed by the tuple t is a subset of every other min-set S1 , . . . , Sl . We then call this set the minimal min-set for the i-th entry in R. Lemma 4.2. Let R be a k-ary relation preserved by lex, t ∈ R, i ∈ [k] and S be the minimal min-set for the i-th entry in R. If t is such that t[j] ≥ t[i] for every j ∈ S, then t[i] = t[j] for every j ∈ S. To develop our algorithm, we use a speci?c notion of constraint graph of a temporal CSP instance, de?ned as follows. De?nition 4.3. The constraint graph GΦ of a temporal CSP instance Φ is a directed graph (X, E) de?ned on the variables X of Φ. For each constraint of the form R(x1 , . . . , xk ) from Φ we add a directed edge xi xj to E if in every tuple from R where the i-th entry is minimal the j-th entry is minimal as well.

8

? M. BODIRSKY AND J. KARA

Example. We return to the example from Section 2. The constraint graph GΦ1 for the instance Φ1 in this example has the vertices x1 , x2 , y1 , y2 , y3 , edges from y1 , y2 , y3 to all other variables, and an edge from x2 to x1 . De?nition 4.4. If Φ contains a constraint φ imposed on y such that φ does not admit a solution where y denotes the minimal value, the we say that y is blocked (by φ). We can easily determine for each constraint which variables are blocked by this constraint: For a constraint represented by a set of tuples we just check all the tuples and build a set of variables that are not minimal in any of them. For a constraint represented by an ll-Horn formula, a variable xi is blocked if and only if the formula is of the form xi > z1 ∨ · · · ∨ xi > zl . Thus, by inspecting all the constraints it is possible to compute the blocked variables in linear time in the input size. We would like to use the constraint graph to identify variables that have to denote the same value in all solutions, and therefore introduce the following concepts. De?nition 4.5. A strongly connected component K of the constraint graph GΦ for a temporal CSP instance Φ is called a sink component if no edge in GΦ leaves K, and no variable in K is blocked. A vertex of G that belongs to a sink component of size one is called a sink. Example. In the previous example, the variables y1 , y2 , y3 are blocked, and x1 and x2 are not blocked. The set of vertices {y1 , y2 , y3 } forms a strongly connected component, which is not a sink component, because there are outgoing edges. (Moreover, the variables in K are blocked.) The singleton-set {x1 } is a strongly connected component without outgoing edges and without blocked vertices, and thus x1 is a sink. The following lemma shows an important consequence of lex-closure of constraints. Lemma 4.6. Let K be a sink component of the graph GΦ for an instance Φ with lex-closed constraints. Then all variables from K must have equal values in all solutions of Φ. Lemma 4.6 immediately implies that we can add constraints of the type x = y for all variables x, y from the same sink component K. Equivalently, we can consider the CSP instance Φ′ where all the variables in K are contracted, i.e., where all variables from K are replaced by the same variable. In some cases, a solution to a projected instance with ll-closed constraints can be used to construct a solution to the original constraint. We say that a tuple (in particular, a solution of an instance) x is injective if xi = xj for all i = j. Lemma 4.7. Let Φ be an instance of the CSP with variables X and ll-closed constraints. Let x be a sink in GΦ . If the projection Φ′ of Φ to X \ {x} has an injective solution, then Φ has an injective solution as well. We are ready to state our algorithm for instances with ll-closed constraints; the algorithm works for both representations of the constraints (sets of tuples, ll-Horn formulas). Theorem 4.10. The procedure Solve(Φ) in Algorithm 4.9 decides whether a given set of ll-closed constraints Φ has a solution. There is an implementation of the algorithm that runs in time O(nm), where n is the number of variables of Φ and m is the weighted number of constraints in Φ. Proof sketch. The correctness of the procedure Spec immediately implies the correctness of the procedure Solve. In the procedure Spec, after iterated deletion of sinks in G′ , we have to distinguish three cases.

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

9

Algorithm 4.8. Spec(Φ) { // Input: Φ constraints with variables X // Output: If algorithm returns false // then Φ has no solution // If Φ has an injective solution, then return true // Otherwise return S ? X, |S| ≥ 2, s.t. for all // x, y ∈ S we have x = y in all solutions of Φ G := ConstructGraph(Φ) Y := ?, Φ′ := Φ, G′ := G While G′ contains a sink s Y := Y ∪ {s} Φ′ := projection of Φ′ to X \ Y G′ := ReconstructGraph(Φ′) If Y = X then return true else if G′ has sink component S return S else return false end if }

Algorithm 4.9. Solve(Φ): { // Input: instance Φ with variables X // Output: true or false S := Spec(Φ) If S = false then return false else if S = true then return true else Let Φ′ be contraction of S in Φ return Solve(Φ′) end if }

Figure 2: An algorithm for ll-closed constraints. In the ?rst case, Y = X. We prove by induction that Φ has an injective solution. Let x1 , . . . , xn be the elements from Y in the reverse order in which they were included into Y . For 0 ≤ i ≤ n, let Φi be the instance Φ projected to X \ {x1 , . . . , xi }. Note that Φ0 = Φ, and that Φn = Φ′ is the projection of Φ to the empty set, which trivially has an injective solution. We inductively assume that Φi , for i ≤ n, has an injective solution. Then Lemma 4.7 applied to xi , the instance Φi?1 , and the injective solution to Φi implies that also Φi?1 has an injective solution. By induction, Φi has an injective solution for all 0 ≤ i ≤ n, and in particular Φ0 = Φ has an injective solution. Therefore, the output true of Spec is correct. Otherwise, in the second case, G′ contains a sink component S with |S| ≥ 2. We claim that for all variables x, y ∈ S we have x = y in all solutions to Φ. Lemma 4.6 applied to the projection of Φ to X \ Y implies that whenever some variables are in the same sink component, they must have the same value in every solution, and hence the output is correct in this case as well. In the third case, Y = X, but G′ does not contain a sink component. Note that in every solution to Φ′ some variable must take the minimal value. However, since each strongly connected component without outgoing edges contains a blocked vertex, there is no variable that can denote the minimal element, and hence Φ′ has no solution. Because Φ′ is a projection of Φ to X \ Y , the instance Φ is inconsistent as well. Since in each recursive call of Solve the instance in the argument has at least one variable less, Solve is executed at most n times. It is not di?cult to implement the algorithm such that the total running time is cubic in the input size. However, it is possible to implicitely represent the constraint graph and to implement all sub-procedures such that the total running time is in O(nm), for both types of representations of the constraints studied in this paper. The details are described in the appendix.

10

? M. BODIRSKY AND J. KARA

5. ll-closed Constraints and Datalog

In this section, we prove that the constraint satisfaction problem for ll-closed constraints can not be solved by Datalog programs4. For simplicity, the de?nition of the sematics of Datalog that we use here will be purely operational; for the standard semantical approach to the evaluation of Datalog programs see [11]. A Datalog program is a ?nite set of Horn clauses, i.e., clauses of the form ψ ← φ1 , . . . , φl , where l ≥ 0 and where ψ, φ1 , . . . , φl are atomic formulas of the form R(x). The formula ψ is called the head of the rule, and φ1 , . . . , φl are called the body. We assume that all variables in the head also occur in the body. The relation symbols occurring in the head of some clause are called intentional, and all other relation symbols in the clauses are called extensional. If Γ is a ?nite TCL, we might use Datalog programs to solve CSP(Γ) as follows. Let Π be a Datalog program whose extensional symbols are from Γ. We assume that there is one distinguished 0-ary intentional relation symbol false. Now, suppose we are given an instance Φ of CSP(Γ). An evaluation of Π on Φ proceeds in steps i = 0, 1, . . . At each step i we maintain a set of literals Φi with extensional and intentional relation symbols; it always holds that Φi ? Φi+1 . Each clause of Π is understood as a rule that may derive a new literal from the literals in Φi . Initially, we have Φ0 := Φ. Now 0 0 suppose that R1 (x1 , . . . , x11 ), . . . , Rl (xl , . . . , xl l ) are literals in Φi , and R0 (y1 , . . . , yk0 ) ← 1 1 k k ′ 1 1 l l i i′ R1 (y1 , . . . , yk1 ), . . . , Rl (y1 , . . . , ykl ) is a rule from Π, where yj = yj ′ if and only if xi = xi ′ . j j Then R0 (x0 , . . . , x0 ) is the newly derived literal in Φi+1 , where x0 = xi ′ if and only if 1 j l j 0 i yj = yj ′ . The procedure stops if no new literal can be derived. We say that Π solves CSP(Γ), if for every instance Φ of CSP(Γ) there exists an evaluation of Π on Φ that derives false if and only if Φ has no solution. We want to remark that the so-called method of establishing path-consistency, which is very well-known and frequently applied in Arti?cial Intelligence, can be formulated with Datalog programs where the intentional symbols are at most binary and all rules use at most three variables in the body. We prove that already for the TCL that only consists of Rmin there is no Datalog program that solves the corresponding constraint satisfaction problem. We use a pebblegame characterization of the expressive power of Datalog, which was originally shown in [12] and [20] for ?nite domain constraint satisfaction, and which holds for a wide variety of in?nite domain constraint languages as well, including qualitative TCLs (see the journal version of [2]). Let Γ be a ?nite TCL, and let Φ be an instance of CSP(Γ). Then the existential kpebble game on Φ is the following game between the players Spoiler and Duplicator. Spoiler has k pebbles p1 , . . . , pk . He places his pebbles on variables from Φ. Initially, no pebbles are placed. In each round of the game Spoiler picks some of these pebbles. If they are already placed on Φ, then Spoiler ?rst removes them from Φ. He then places the pebbles on variables from Φ, and Duplicator responds by assigning elements from Q to these variables. This assignment has to satisfy all the constraints φ ∈ Φ where all variables in φ are pebbled, otherwise Spoiler wins the game. Duplicator wins, if the game continues forever, i.e., if Spoiler can never win the game.

4This result should not be confused with the weaker fact that establishing k-consistency does not imply

global consistency, for any k. This was shown for Ord-Horn in [21]. But recall that Ord-Horn can be solved by a Datalog program [27].

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

11

Theorem 5.1 (from [2]). Let Γ be a ?nite TCL. There is no Datalog program that solves CSP(Γ) if and only if for every k there exists an inconsistent instance of CSP(Γ) such that Duplicator wins the existential k-pebble game on Φ. We present the essential construction for the proof of the following theorem; due to space restriction, the full proof has been moved to the appendix. Theorem 5.2. There is no Datalog program that solves CSP({Rmin }). Proof idea. Let k be an arbitrary number. To apply Theorem 5.1 we have to construct an inconsistent instance Φ of CSP({Rmin }) such that Duplicator wins the existential k-pebble game on Φ. For this, let G be a 4-regular graph of girth at least 2k + 1, i.e., all cycles in G have more than 2k vertices. It is known and easy to see that such graphs exist, e.g. with the methods in [19]. Orient the edges in G such that there are exactly two outgoing and two incoming edges for each vertex in G. Since G is 4-regular, there exists an Euler tour for G (see e.g. [8]), which shows that such an orientation exists. Now we can de?ne our instance Φ of CSP({Rmin }) as follows. The variables of Φ are the vertices from G. The instance Φ contains the constraint Rmin (w, u, v) i? uw and vw are the two incoming edges at vertex w. We claim that Φ does not have a solution: if there was a solution, some variable w must denote the minimal value. But for every variable w we ?nd a constraint Rmin (w, u, v) in Φ, and this constraint is violated since either u or v must be strictly smaller than w. The proof that Duplicator has a winning strategy for the existential k-pebble game on this instance can be found in the appendix.

6. Conclusion

While most of the polynomial algorithms that are known and used to solve in?nitedomain constraint satisfaction problems are based on local consistency techniques, we used graph algorithms on an appropriately de?ned notion of constraint graph to both improve applicability (the constraint languages we can solve with our approach contain constraint relations whose CSP can not be solved with local consistency techniques – Theorem 5.2) and running time (our algorithm has quadratic running time, whereas resolution or establishing path consistency would require cubic time). We believe that similar approaches can lead to faster algorithms and larger tractable languages for many problems where the only known algorithms are based on local consistency techniques.

Acknowledgements

We would like to thank Christopher Rudolf for implementing the algorithm.

12

? M. BODIRSKY AND J. KARA

References

[1] J. F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832– 843, 1983. [2] M. Bodirsky and V. Dalmau. Datalog and constraint satisfaction with in?nite templates. In STACS, pages 646–659, 2006. [3] M. Bodirsky and J. K?ra. The complexity of temporal constraint satisfaction problems. In Proceedings a of STOC’08, 2008. [4] A. Bulatov, P. Jeavons, and A. Krokhin. The complexity of constraint satisfaction: An algebraic approach (a survey paper). In: Structural Theory of Automata, Semigroups and Universal Algebra (Montreal, 2003), NATO Science Series II: Mathematics, Physics, Chemistry, 207:181–213, 2005. [5] A. Bulatov, A. Krokhin, and P. G. Jeavons. Classifying the complexity of constraints using ?nite algebras. SIAM Journal on Computing, 34:720–742, 2005. [6] N. Creignou, M. Hermann, A. Krokhin, and G. Salzer. Complexity of clausal constraints over chains. Research Report, Ecole Polytechnique, 2005. [7] R. Dechter. Constraint Processing. Morgan Kaufmann, 2003. [8] R. Diestel. Graph Theory. Springer–Verlag, New York, 1997. [9] T. Drakengren and P. Jonsson. Twenty-one large tractable subclasses of Allen’s algebra. Arti?cial Intelligence, 93:297–319, 1997. [10] I. D¨ntsch. Relation algebras and their application in temporal and spatial reasoning. Arti?cial Intelu ligence Review, 23:315–357, 2005. [11] H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer, 1999. 2nd edition. [12] T. Feder and M. Vardi. The computational structure of monotone monadic SNP and constraint satisfaction: A study through Datalog and group theory. SIAM Journal on Computing, 28:57–104, 1999. [13] M. Fisher, D. Gabbay, and L. Vila, editors. Handbook of Temporal Reasoning in Arti?cial Intelligence. Elsevier, 2005. [14] M. Garey and D. Johnson. A guide to NP-completeness. CSLI Press, 1978. [15] M. C. Golumbic and R. Shamir. Complexity and algorithms for reasoning about time: a graph-theoretic approach. Journal of the ACM, 40(5):1108 – 1133, 1933. [16] W. Guttmann and M. Maucher. Variations on an ordering theme with constraints. In Fourth IFIP International Conference on Theoretical Computer Science (TCS’06), IFIP International Federation for Information Processing 209, pages 77–90, 2006. [17] P. Hell and J. Neˇetˇil. Graphs and Homomorphisms. Oxford University Press, 2004. s r [18] W. Hodges. A shorter model theory. Cambridge University Press, 1997. [19] S. Janson, T. Luczak, and A. Rucinski. Random Graphs. John Wiley and Sons, 2000. [20] P. G. Kolaitis and M. Y. Vardi. Conjunctive-query containment and constraint satisfaction. In Proceedings of PODS’98, pages 205–213, 1998. [21] M. Koubarakis. Tractable disjunctions of linear constraints: Basic results and applications to temporal reasoning. Theoretical Computer Science, 266:311–339, 2001. [22] A. A. Krokhin, P. Jeavons, and P. Jonsson. Reasoning about temporal relations: The tractable subalgebras of Allen’s interval algebra. JACM, 50(5):591–640, 2003. [23] P. B. Ladkin and R. D. Maddux. On binary constraint problems. Journal of the Association for Computing Machinery, 41(3):435–469, 1994. [24] H. K. Marc Vilain and P. van Beek. Constraint propagation algorithms for temporal reasoning: A revised report. Reading in Qualitative Reasoning about Physical Systems, pages 373–381, 1989. [25] D. Marker. Model Theory: An Introduction. Springer, 2002. [26] R. H. M¨hring, M. Skutella, and F. Stork. Scheduling with and/or precedence constraints. SIAM J. o Comput., 33(2):393–415, 2004. [27] B. Nebel and H.-J. B¨rckert. Reasoning about temporal relations: A maximal tractable subclass of u Allen’s interval algebra. JACM, 42(1):43–66, 1995. [28] A. Szendrei. Clones in universal Algebra. Seminaire de mathematiques superieures. Les Presses de L’Universite de Montreal, 1986. [29] P. van Beek. Reasoning about qualitative temporal information. Arti?cial Intelligence, 58:297–326, 1992. [30] R. van der Meyden. The complexity of querying inde?nite information about linearly ordered domains. Journal of Computer and Systems Science, 54(1):113–135, 1997.

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

13

Appendix A. Appendix: Proofs

A.1. Proposition 3.1. Given a constraint language where all relations are represented as lists of weak linear orders, one can decide in polynomial time in the input size whether the constraint language is ll-closed. Proof. We test for each relation R in the constraint language separately whether it is llclosed. A k-ary relation R is preserved by ll if and only if for every two weak orders o1 and o2 in R and every index e ≤ k the weak order o3 is also in R, where o3 is de?ned as follows: (i, j) ∈ o3 i? one of the following holds ? (i, j) ∈ o1 and (i, j) ∈ o2 , ? (i, j) ∈ o1 , (j, i) ∈ o1 , and (i, e) ∈ o1 , or / ? (i, j) ∈ o2 , (j, i) ∈ o2 , (e, j) ∈ o1 , and (j, e) ∈ o1 . / / For all pairs (o1 , o2 ) of weak linear orders on {1, . . . , k} in the representation of R, and for each index e ≤ k, we can verify in linear time in k whether the weak linear order o3 as described above is also contained in the representation of R. A.2. Proposition 3.3 The language of ll-closed constraints does not contain the language of dual ll-closed constraints and vice versa. Proof. To show that the language of ll-closed constraints does not contain the language of dual ll-closed constraints, we show that there is a temporal relation that is preserved by ll but not by dual ll. We claim that the relation Rmin is preserved by the ll operation: Let (x1 , x2 , x3 ) and (y1 , y2 , y3 ) be triples that are both in the relation Rmin . Without loss of generality, x1 > x2 (note that the relation is symmetric in the second and third argument). If in this case y1 ≥ y2 , then, because ll preserves ≤, we have that ll(x1 , y1 ) ≥ ll(x2 , y2 ), and because ll is injective, we have that ll(x1 , y1 ) > ll(x2 , y2 ). Therefore (ll(x1 , y1 ), ll(x2 , y2 ), ll(x3 , y3 )) is in Rmin , and we are done. So let us assume that x2 > y2 , and therefore x2 < z2 . We can then show that (ll(x1 , y1 ), ll(x2 , y2 ), ll(x3 , y3 )) is in Rmin unless x1 < x3 . So let us assume that x1 < x3 . Now, in case that x2 > 0, the operation ll preserves Rmin , since in this case ll acts like a lexicographic order on the two triples. Otherwise, x ≤ 0. It is easy to check that then ll(x2 , y2 ) < ll(x1 , y1 ) because x1 > x2 . However, Rmin is not preserved by the dual ll operation: consider the tuples t1 := (?1, 1, ?2) and t2 := (?1, ?2, 1) that are both in Rmin . If we apply the dual ll operation to these two tuples, we obtain dual-ll(?1, ?1) < dual-ll(?2, 1) < dual-ll(1, ?2), and hence the tuple dual-ll(t1 , t2 ) is not in the relation Rmin . This shows that the language of ll-closed constraints does not contain the language of dual ll-closed constraints. Analogously, we can use the relation Rmax to show that the language of dual ll-closed constraints does not contain the language of ll-closed constraints.

14

? M. BODIRSKY AND J. KARA

A.3. Proposition 3.4. All relations in Ord-Horn are preserved by ll and by dual ll. Proof. We will give the argument for the ll operation only; the argument for the dual ll operation is analogous. It su?ces to show that every relation that can be de?ned by a formula Φ of the form (x1 = y1 ∧ · · · ∧ xk?1 = yk?1 ) → xk O yk is preserved by ll, where C ∈ {<, ≤, =}. Let t1 and t2 be two 2k-tuples that satisfy Φ. Consider a 2k-tuple k3 obtained by applying ll componentwise to t1 and t2 . We distinguish two cases: either there is an i ≤ k ? 1 such that in one of the tuples xi = yi is not satis?ed – in this case xi = yi is not satis?ed in t3 as well by injectivity of ll, and therefore the tuple t3 satis?es Φ. Or xi = yi holds for all i ≤ k ? 1 in both tuples t1 and t2 . But then, as t1 and t2 satisfy Φ, the literal xk Oyk holds in both t1 and t2 . Since ll preserves all relations in {<, ≤, =}, the literal xk Oyk holds in t3 , and therefore t3 satis?es Φ as well. A.4. Proposition 3.5 A temporal relation is ll-closed if and only if it can be de?ned by an ll-Horn formula. We ?rst have to prove the following lemma. Lemma A.1. Let R be a temporal relation that only contains tuples with pairwise distinct entries. Then R can be de?ned by a conjunction of formulas of the form z0 > z1 ∨· · ·∨z0 > zl . Proof. Let φ(x1 , . . . , xn ) be a de?nition of R in conjunctive normal form, i.e., φ is a conjunction of disjunctions of literals where each literal is of the form xu > xv or xu ≤ xv (every temporal relation has such a de?nition). Because of our assumption on R, we can replace literals of the form xu ≤ xv by xu < xv and obtain an equivalent formula. So we can assume that φ does not contain literals of the form xu ≤ xv . Among all such formulas, choose φ to be one which has a minimal number of bad clauses, i.e., clauses C of a form that is di?erent from the form in the statement of the lemma. Any such clause must have two literals l1 := xu > xv and l2 := xr > xs where xu and xr are distinct variables. Suppose that φ contains a bad clause C. Then there must be a tuple t1 such that l1 is the only literal satis?ed in C if we assign t1 [i] to xi , and a tuple t2 such that l2 is the only literal satis?ed in C if we assign t2 [i] to xi . We ?rst study the case that t1 can be chosen such that t1 [r] is smaller than t1 [s], t1 [u], and t1 [v]. Let α be an automorphism of (Q, <) such that t1 [r] is mapped to 0. Consider the tuple t = ll(α(t1 ), t2 ). Observe that if a literal in some clause of φ is not satis?ed in both tuples t1 and t2 , then it is also not satis?ed in t, because ll and α preserve ≥. Therefore only the literals l1 and l2 of C can be satis?ed by t. Since t[r] is strictly smaller than t[s] (by the properties of ll), the literal l2 cannot be satis?ed by t in C. Since t2 [u] < t2 [v], it also holds that t[u] < t[v] (by the properties of ll), and hence l1 is not satis?ed in t either. So t does not give a satisfying assignment for Φ, a contradiction with the assumption that Φ de?nes an ll-closed relation. Similarly, we can argue that t2 cannot be chosen such that t2 [u] is smaller than t2 [v], t2 [r], and t2 [s]. Therefore Φ implies the two clauses (xu > xv ∨ xu > xs ) and (xr > xv ∨ xr > xs ) (here we use again our assumption on R). The formula Φ′ obtained from Φ by removing C and adding these two clauses has less bad clauses. Therefore, if we show that Φ′ is

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

15

equivalent to Φ, we obtain a contradiction to the choice of Φ. Then Φ cannot contain bad clauses, and we are done. We have already seen that Φ implies Φ′ . For the opposite direction, let t be any satisfying assignment of Φ′ . Clearly, all the clauses of Φ except for C are satis?ed by t, because they are also present in Φ′ . We can reformulate the two additional clauses in Φ′ to (xu > xv ∧ xr > xv ) ∨ (xu > xv ∧ xr > xs ) ∨ (xu > xs ∧ xr > xv ) ∨ (xu > xs ∧ xr > xs ) . If the ?rst, the second, or the fourth disjunct is satis?ed by t, then t[xu ] > t[xv ]∨t[xr ] > t[xs ], and therefore C holds in t. If the third disjunct is satis?ed by t and the literal l1 does not hold (i.e., t[xu ] < t[xv ]), we have the chain of inequalities t[xs ] < t[xu ] < t[xv ] < t[xr ] and hence t[xr ] > t[xs ]. Thus, also in this last case C holds. Proof of Proposition 3.5. The proof that every relation de?ned by an ll-Horn formula is ll-closed is similar to the proof of Proposition 3.4. We just need to additionally check that the relation de?ned by z0 > z1 ∨ · · · ∨ z0 > zl and the relation de?ned by z0 > z1 ∨ · · · ∨ z0 > zl ∨ (z0 = · · · = zl ) are preserved by ll, which is straightforward. The proof of the reverse implication is by induction on the arity n of the temporal relation R. We assume that R is ll-closed. For n = 2 the statement of the proposition holds, because all binary temporal relations can be de?ned by ll-Horn formulas. For n > 2, we construct the formula φ that de?nes R as follows. Let inj (R) be the relation that consists of all tuples in R with pairwise distinct entries. It is straightforward to verify that inj (R) is ll-closed as well. Let φinj (x1 , . . . , xn ) be the formula de?ning inj (R) as stated in Lemma A.1. For all pairs of entries i, j ∈ {1, . . . , n}, i < j, let Ri,j be the projection of the relation R(x1 , . . . , xi?1 , xj , xi+1 , . . . , xn ) to x1 , . . . , xj?1 , xj+1 , . . . , xn . Because also Ri,j is ll-closed, it has an ll-Horn de?nition φi,j by inductive assumption. We add to each clause of φi,j a literal xi = xj to the premise of the implication, such that φi,j remains an ll-Horn formula. Let φ be the formula that contains ? all the modi?ed clauses from all formulas φi,j ; ? all clauses C(z0 , . . . , zl ) of φinj such that R does not contain a tuple where z0 , z1 , . . . , zl all get the same value; ? the clause C(z0 , . . . , zl ) ∨ (z0 = z1 = · · · = zl ) for all other clauses C of φinj with variables z0 , z1 , . . . , zl . Obviously, φ is an ll-Horn formula. We have to verify that φ de?nes R. Let t be an n-tuple such that t ∈ R. If t has only pairwise distinct entries, then t ∈ inj (R) and hence some / / clause C(z0 , z1 , . . . , zl ) of φinj is not satis?ed by t. The variables z0 , z1 , . . . , zl of C cannot all have the same value in t, and so φ is not satis?ed either. If there are i, j such that t[i] = t[j] then the tuple tj = (t[1], . . . , t[j ? 1], t[j + 1], . . . , t[n]) ∈ Ri,j . Therefore some / clause C of φi,j is not satis?ed by tj , and C ∨ xi = xj is not satis?ed by t. Thus, in this case t does not satisfy φ, too. We also have to verify that all t ∈ R satisfy φ. Let C be a clause of φ created from some clause in φi,j . If t[i] = t[j], then C is satis?ed by t because C contains xi = xj . If t[i] = t[j], then (t[1], . . . , t[j ? 1], t[j + 1], . . . , t[n]) ∈ Ri,j and thus this tuple satis?es φi,j . This also implies that t satis?es C. Finally, let C be a clause of φ created from some clause of φinj . The clause C is of the form xu0 > xu1 ∨ · · · ∨ xu0 > xum and possibly contains a formula xu0 = xu1 = · · · = xum . If t is constant on the variables of C, then, by construction of φ, C contains xu0 = xu1 = · · · = xum and is satis?ed. So suppose t is not constant on

16

? M. BODIRSKY AND J. KARA

the variables of C. Also assume that t[u0 ] ≤ t[ui ] for all i ∈ [m] (otherwise t satis?es C and we are again done). Since t is not constant, there is a j ∈ [m] such that t[u0 ] < t[uj ]. Because φinj is reduced, there is a tuple t′ ∈ inj (R) that satis?es only the literal xu0 > xuj in C. Consider the tuple t′′ = lex (t, t′ ). Because t′ has pairwise distinct entries and lex is an injective operation, t′′ also has pairwise distinct entries. Since t[u0 ] ≤ t[ui ] for all i ∈ [m], t′ [u0 ] < t′ [ui ] for all i ∈ [m] \ {j}, and because lex preserves ≤, we get that t′′ [u0 ] < t′′ [ui ] for all i ∈ [m] \ {j}. Finally, since t[u0 ] < t[uj ] we also have that t′′ [u0 ] < t′′ [uj ] by the properties of lex. Hence, t′′ [u0 ] < t′′ [ui ] for all i ∈ [m] and therefore t′′ does not satisfy C and thus also does not satisfy φinj . But t′′ is injective and is from R (because R is ll-closed) and therefore t′′ satis?es inj (R). A contradiction with the assumption that φinj de?nes inj (R). A.5. Lemma 4.2. Let R be a k-ary relation preserved by lex, let i ∈ [k] and S be the minimal min-set for the i-th entry in R. If t[j] ≥ t[i] for every j ∈ S, then t[i] = t[j] for every j ∈ S. Proof. Let t′ ∈ R be the tuple that witnesses the minimal min-set S. Suppose there is a tuple t ∈ R such that not all entries in S are equal (in particular, |S| > 1). Consider the tuple t′′ := lex(t′ , t). By the properties of lex it holds that t′′ [i] < t′′ [j] for every j ∈ [k] \ S. Furthermore, t′′ [i] ≤ t′′ [j] for j ∈ S if and only if t[i] ≤ t[j]. Thus, unless t′′ witnesses a smaller min-set for i in R (which would be a contradiction), we have that t′′ [i] > t′′ [j] for some j ∈ S. A.6. Lemma 4.6. Let K be a sink component of the graph GΦ for a constraint Φ with lex-closed constraints. Then all variables from K must have equal values in all solutions of Φ. Proof. We assume that Φ has a solution, and that K has at least two vertices (otherwise the lemma is trivial). Let t be a solution of Φ, and let M ? K be the set of variables that have in t the minimal value among the variables of the sink component K. If M = K, we are done. Otherwise, because K is a strongly connected component, there is an edge in GΦ from some vertex u ∈ M to some vertex v ∈ K \ M . By the de?nition of GΦ , there is a constraint φ in Φ such that whenever u denotes the minimal value of a solution of φ, then v has to denote the minimal value as well. By permuting arguments, we can assume without loss of generality that φ is of the form R(w1 , . . . , wk ) where w1 = u and w2 = v. Because K is a sink component, the variable u cannot be blocked, and hence there is a minimal min-set S for the ?rst entry in R. Clearly, S contains 2, because v is the second argument of φ. Note that GΦ contains an edge from u to wi for all i ∈ S. Since K is a strongly connected component, all these variables wi are in K. Because u has in t the minimal value among the variables in K, there is no variable wi , i ∈ S, which has a smaller value than u in t. This contradicts Lemma 4.2, because the value for u in t is di?erent than the value for v.

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

17

A.7. Lemma 4.7. Let Φ be an instance of the CSP with variables X and ll-closed constraints. Let x be a sink in GΦ . If the projection Φ′ of Φ to X \ {x} has an injective solution, then Φ has an injective solution as well. Proof. Let s be an injective solution to Φ′ . Consider a constraint φ = R(x1 , . . . , xk ) from Φ that is imposed on x. By the de?nition of Φ′ there is a tuple t ∈ R such that t agrees with s on {x1 , . . . , xk } \ {x}. Because x is a sink, there is tuple t′ ∈ R such that the entry corresponding to x is strictly minimal. It is now easy to check that there are automorphisms α, β of (Q, <) such that the tuple t′′ = α(ll(β(t′ ), t)) agrees with s on X \ {x}, and such that the entry corresponding to x is strictly minimal. As R is ll-closed, t′′ ∈ R. Thus we see that for each constraint R(x1 , . . . , xk ) imposed on x there is a tuple in R where the entry corresponding to x is strictly minimal, and the rest of the tuple agrees with s on X \ {x}. Hence, we can extend s by assigning to x a value smaller than any value used in s, and the lemma readily follows. A.8. Theorem 4.10. The procedure Solve(Φ) in Algorithm 4.9 decides whether a given set of ll-closed constraints Φ has a solution. There is an implementation of the algorithm that runs in time O(nm), where n is the number of variables of Φ and m is the weighted number of constraints in Φ. Proof. We have already shown the correctness of the algorithm, and only have to discuss how to implement the algorithm such that it runs in O(nm). In fact, we describe an implementation of the procedure Spec that is linear in the input size. First we show how to deal with constraints represented by ll-Horn clauses. Observe that if an ll-Horn clause has a non-empty left hand side of the implication, then a constraint for this clause creates neither edges nor blocked vertices in the constraint graph. Also constraints of the type z0 > z1 ∨ · · · ∨ z0 > zl do not create edges in GΦ . Thus, when constructing GΦ , we only care about constraints of the type z0 > z1 ∨ · · · ∨ z0 > zl ∨ (z0 = z1 = · · · = zl ). For such constraints we add edges from z0 to z1 , . . . , zl to GΦ . When the constrains in the input instance are represented by sets of tuples we have to be more careful, and do not represent the edges of GΦ explicitely. We sort the tuples in each set according to their number of equivalence classes. Now, the data structure contains for each variable and each constraint that is imposed on this variable a reference to the tuple t in this constraint such that v has the least value in t and t has the largest number of equivalence classes. Moreover, for each value in each tuple we create a list that contains the entries where this value appears in the tuple. Finally, for each variable v we also have a list that contains the constraints that are imposed on v and that block v. With bucket sort, the total cost to set up this data structure is linear in the input size. Even though the constraint graph GΦ is not explicitely represented, it is possible to use the above data structure to compute the strongly connected components of GΦ in linear time, using depth-?rst search. Now we have to describe how the algorithm ?nds sinks, how the data structure is updated after projections, and how the algorithm ?nds sink components if there is no sink left and not all variables have been projected out. To ?nd sink and sink components, we also have to be able to determine e?ciently whether a node is blocked or not.

18

? M. BODIRSKY AND J. KARA

Initially, because we have computed the strongly connected components, and because we know which variables are blocked, we can create a list that contains all sinks of the initial instance. Suppose that s is a sink of G at some iteration of the while-loop. We then ?rst compute the projection of Φ′ to X \ Y by updating only the constraints imposed on s in Φ′ . At this step we can also determine whether a constraint no longer blocks a variable v, and in this case we can update the list of blocking constraints for v. As soon as this list becomes empty, we know that v is no longer blocked. In this case, if v does not have outgoing edges in the current constraint graph, which we can determine e?ciently using our updated data structure, we add v to the list of sinks. The total number of operations we have to perform in all iterations of the while-loop is then bounded by m. Finally, if there is no sink left, but not all variables have been projected out, then we can compute the strongly connected components of the resulting constraint (again, this can be done in linear time using depth-?rst search on our data structure), and since we know which variables are blocked, we can also ?nd the sink components. Note that we can assume that n is smaller than m. Otherwise, the constraint is not connected (we use the notion of connectivity for instances of the CSP as e.g. in [17]). We can in this case use the same implementation, analyse the running time for each of the connected components separately, and will get the same result. This concludes the proof that for both representations studied in this paper the algorithm can be implemented such that it runs in time O(nm). A.9. Theorem 5.2. There is no Datalog program that solves CSP({Rmin }). Proof. Let G be the graph constructed in the proof of Theorem 5.2 so far. Consider a connected non-empty subgraph G′ of G having at most 2k vertices where only one vertex r has no outgoing edges, and where all vertices have either two or no incoming edges. Since G has girth 2k + 1, G′ must be a binary tree with root r. We call G′ dominated, if all leaves in G′ are pebbled. Duplicator always maintains the property that whenever the root r in a dominated tree is pebbled during the game, then the value assigned to r is strictly larger than the minimum of all the values assigned to the leaves. Clearly, this property is satis?ed at the beginning of the game. Suppose that during the game Spoiler pebbles the variable u. Let T1 , . . . , Ts be those newly created dominated trees in G that have pebbled roots r1 , . . . , rs , for s ≥ 0. If s > 0, let ri be the root that received the minimal value a among all the roots r1 , . . . , rs . We claim that if u is the root of a dominated tree T , then a is strictly larger than the minimum b of all the values assigned to the leaves of T . Otherwise, the graph T ∪ Ti was a dominated tree that violates the invariant even before the variable u has been pebbled, a contradiction. Therefore, in this case Duplicator can choose a value c between b and a for the variable u. Since c is smaller than a, in all the new dominated trees T1 , . . . , Ts in G the value assigned to r1 , . . . , rs is strictly larger than c, and hence the invariant is preserved. In particular, if Rmin (w, u, v) (or Rmin (w, v, u)) is a constraint in Φ where w and v have been pebbled, then this constraint is satis?ed by the assignment.

A FAST ALGORITHM AND LOWER BOUND

FOR TEMPORAL REASONING

19

Since c is larger than b, this choice also guarantees that if v, v ′ are pebbled variables then any constraint of the form Rmin (u, v, v ′ ) is satis?ed, because in this case the variables u, v, v ′ induce a dominated tree with root u in G. If there is no dominated tree T where u is the root, then Duplicator assigns a value to u that is smaller than all values assigned to other variables. If s = 0, Duplicator plays a value that is larger than all values assigned to other variables. In both cases it is easy to check that Duplicator maintains the invariant, and satis?es all constraints φ ∈ Φ where all variables are pebbled. By induction, we have shown that Duplicator has a winning strategy for the existential k-pebble game on Φ.