Discrete-Time Temporal Reasoning with Horn DLRs

1 Introduction

Reasoning about time is ubiquitous in artificial intelligence and many different branches of computer science. Noteworthy examples include planning, diagnosis, and temporal databases. For a general overview of temporal reasoning, see, for instance, the handbook [Fisher et al., 2005]. The temporal constraint satisfaction problem is very well-studied and there has lately been substantial progress in understanding the complexity of this problem. Bodirsky and K´ara [2010] have presented a complete classification of the temporal constraint problem for relations that are first-order definable in the structure (Q; <). This result subsumes much of the previous work on qualitative (that is, the case where we cannot refer to individual time points in the underlying time structure) temporal constraints such as Allen's algebra. There are no such unifying result for metric temporal constraints, but many partial results are known, cf. [Jonsson and B¨ackstr¨om, 1998; Krokhin et al., 2004].

∗ Partially supported by the Swedish Research Council (VR) under grant 621-2009-4431

† Partially supported by the Swedish National Graduate School in Computer Science (CUGS).

The situation is very different if we turn our attention to discrete temporal constraints where the set of time points is some subset of the set of integers Z. There are some scattered complexity results (cf. [Bettini et al., 1998; Meiri, 1996]) but a coherent picture is lacking. This is unsatisfactory since reasoning about discrete time is an important part of AI: let us just mention temporal logics, plan generation, and discrete time Markov chains as three concrete examples. Reasoning about discrete time is also inevitable in many 'industrial' settings: for systems that are repeatedly sampled (for monitoring or other purposes), we are implicitly forced to assume that the underlying model of time is discrete. Our goal with this paper is to initiate a systematic study of temporal constraint satisfaction under the assumption that time is discrete instead of continuous. The focus will be on the computational complexity of such problems; more precisely, we aim at identifying restricted classes of constraints such that the corresponding constraint satisfaction problem can be solved in polynomial time. Obtaining a full classification of hard and easy cases is of course highly desirable - it gives us a very powerful tool for studying the complexity of problems that can be modelled within the language. Since temporal constraint reasoning appears as a subproblem in many different types of automated reasoning, we expect such results to be useful in many other contexts, too. For instance, note that discrete semilinear relations (to be defined later on) have been used intensively for a long time in, for example, formal verification [Boujjani and Habermehl, 1996], distributed computing [Angluin et al., 2007], and automata therory [Parikh, 1966],

In order to introduce temporal constraint reasoning formally, we first define the general constraint satisfaction problem.

Definition 1 Let Γ be a set of finitary relations over some set D of values. The constraint satisfaction problem over Γ (CSP(Γ)) is defined as follows:

Instance: A set V of variables and a set C of constraint applications R(v1, . . . , vk) where k is the arity of R, v1, . . . , vk ∈ V and R ∈ Γ.

Question: Is there a total function f : V → D such that (f(v1), . . . , f(vk)) ∈ R for each constraint R(v1, . . . , vk) in The set Γ is referred to as the constraint language. Given a set D, we let Γ|D denote Γ restricted to D, i.e. Γ|D = {R∩Dn | R ∈ Γ and R has arity n}. We sometimes slightly abuse notation to avoid unnecessary clutter. For instance, we may say 'the relation x = y + z' instead of 'the relation {(x, y, z) ∈ Z3 | x = y + z}.' A constraint satisfaction problem CSP(Γ) is globally tractable if CSP(Γ) is in P and locally tractable if CSP(Γ′ ) is in P for every finite set Γ′ ⊆ Γ. Similarly, CSP(Γ) is globally NP-hard if CSP(Γ) is NP-hard and locally NP-hard if CSP(Γ′ ) is NP-hard for some finite set Γ′ ⊆ Γ.

The separation of local and global tractability/NP-hardness is motivated by the following result: let 〈Γ〉 (the closure or coclone of Γ) denote all relations that are pp-definable in Γ. A relation R is pp-definable in Γ if it can be defined by a firstorder formula over Γ without using disjunction and negation, and with only existential quantification.

Theorem 2 [Jeavons, 1998] For every finite Θ ⊆ 〈Γ〉, CSP(Θ) is polynomial-time reducible to CSP(Γ). Furthermore, if R ∈ 〈Γ〉, then CSP(Γ ∪ {R}) and CSP(Γ) are polynomial-time equivalent problems.

This implies, for instance, that if CSP(Γ) is globally tractable, then CSP(〈Γ〉) is locally tractable.

Let us now turn our attention to temporal constraint problems. We let D ⊆ R denote a set of time points. Let the set SD contain all relations {(x1, . . . , xn) ∈ Dn | C1∧. . .∧Ck} where each clause Ci denotes a disjunction (p1r1c1 ∨ . . . ∨ pmrmcm). Here, cj is an integer, rj ∈ {<,≤,=, ̸=,≥,>} and pj(x1, . . . , xn) is a linear polynomial (i.e. the degree of p equals one) with integer coefficients. We adopt a simple representation of relations in SD: every relation R in SD is represented by its defining formula where each coefficient is written in binary. Let DD ⊆ SD contain the relations that are defined by a single clause. Let HD ⊆ DD contain the relations that are defined by a single clause that contains at most one relation that is not of the type p(¯x) ̸= c. The names S, D, and H are chosen to reflect the names given to the corresponding relations in the literature: the relations in SD are called semilinear relations, the relations in DD are called disjunctive linear relations (DLRs), and the relations in HD are called Horn DLRs. DLRs and Horn DLRs were introduced in [Jonsson and B¨ackstr¨om, 1998] but only for continuous time structures (in fact, only for the set R of real numbers).

Before we continue, we need some NP-hardness results. For distinct a, b ∈ Z, define Ta,b = {(a, a, b), (a, b, a), (b, a, a)}. Clearly, CSP({Ta,b}) is NPhard problems since it corresponds to 1-IN-3-SAT restricted to clauses without negated literals.

Theorem 3 CSP(HR) is globally tractable while CSP(HZ) is locally NP-hard. Furthermore, CSP(DD) and CSP(SD) are locally NP-hard when D ∈ {Z, R}.

Proof: Global tractability of CSP(HR) and local NP-hardness of CSP(DR) and CSP(SR) follows from [Jonsson and B¨ackstr¨om, 1998]. For the remaining cases, it is sufficient to prove local NP-hardness of CSP(HZ). Simply note that we can pp-define T0,1 in HZ by T0,1(x, y, z) ≡ x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ x + y + z = 1 and apply Theorem 2. □

Since CSP(HZ) is locally NP-hard, it makes sense to start looking for tractable fragments within HZ, and this is a natural first step in a bottom-up approach to classifying the complexity of CSP(DZ) and CSP(SZ). Also note that the modelling power (in continuous time) of HR is quite high; many tractable fragments described in the literature are within HR [Jonsson and B¨ackstr¨om, 1998]. This indicates that HZ may be interesting from a modelling point of view, too.

Due to the NP-hardness of CSP(HZ), we will concentrate on identifying tractable fragments and study their maximality in the forthcoming three sections. Given constraint languages Γ ⊆ Θ, we say that Γ is maximally tractable in Θ if CSP(Γ) is globally tractable and CSP(Γ∪{R}) is locally NP-hard for every R ∈ Θ\Γ. Maximality can obviously be defined in different ways with respect to local and global properties but this definition is sufficent for our purposes. We consider problems where solutions can be 'scaled' in Section 2, problems connected to linear equations in Section 3, and so-called k-valid constraints in Section 4. In the proofs, we demonstrate how concepts and ideas like reduced formulas [Bodirsky et al., 2010a] and the independence property [Cohen et al., 2000] can be used for studying discrete-time temporal constraints. We also show how some of the maximality results can be generalised to hardness results for larger classes of constraints. We conclude the paper with a brief discussion concerning the results and future research directions.

2 Scalable constraints

One way to start looking for tractable fragments of HZ is to ask under which circumstances a solution to an instance I of CSP(HR) implies a solution to the corresponding instance I|Z of CSP(HZ). We begin with the following lemma.

Lemma 4 Let Γ be a constraint language over R such that the following holds.

1. Every satisfiable instance of CSP(Γ) is satisfied by some rational point.
2. For each R ∈ Γ, it holds that if ¯x = (x1, x2, . . . , xk) ∈ R, then (ax1, ax2, . . . , axk) ∈ R for all a ∈ {y ∈ R | y ≥ 1} \ X where X is a (possibly empty) finite set. The set X may depend on both R and ¯x.
3. CSP(Γ) is globally (or locally) tractable.

Then, the problem CSP(Γ|Z) is also globally (or locally) tractable.

Proof: Let I be an arbitrary satisfiable instance of CSP(Γ) with a rational solution ¯x = (x1/y1, . . . , xk/yk) where x1, . . . , xk ∈ Z and y1, . . . , yk ∈ Z+ \ {0}. Let n = ∏ki=1 yi and note that n ≥ 1.

For an arbitrary constraint R in I, we know that it is satisfied by a¯x for every a ∈ {y ∈ R | y ≥ 1} \ X where X is finite. For every constraint Ci in I, let Xi denote the set of 'exception' points, and let t = ∑mi=1 |Xi| (where m is the number of constraints in I).

It follows that there is at least one a in the set {y ∈ Z | 1 ≤ y ≤ t + 1} such that an¯x satisfies I. The vector an¯x is integral due to choice of n which concludes the proof. □

Given a real vector ¯x = (x1, . . . , xk), let ||¯x|| denote its Euclidean norm, i.e. √x21 + . . . + x2k . Recall that ||¯x+ ¯ y|| ≤ ||¯x|| + ||¯ y|| and ||α¯x|| = |α| · ||¯x|| for all real vectors ¯x, ¯ y and arbitrary α ∈ R.

Theorem 5 If I is a satisfiable instance of CSP(SR), then I is satisfied by at least one rational point.

Proof: Let ¯ r be a satisfying real point. Assume I contains the constraints {C0, . . . , Cn} where each Ci is a disjunction li1 ∨ li2 ∨ . . . ∨ lik. There is (at least) one lij from each Ci that is satisfied by ¯ r. Since a ≤ b ≡ a < b ∨ a = b, a ≥ b ≡ a > b ∨ a = b, and a ̸= b ≡ a < b ∨ a > b, we can without loss of generality assume that either lij ≡ p(¯x) < c or lij ≡ p(¯x) = c. It is clearly sufficient to find a rational satisfying point, ¯ q, that satisfies the formula l0j0 ∧ . . . ∧ lnjn .

First consider the literals of the type p(¯x) < c. The sets of satisfying points to these kinds of relations are clearly open. Hence, there is some rational number δ > 0 so that all points ¯x for which ||¯ r - ¯x|| < δ satisfy these relations.

The remaining literals are of the form p(¯x) = c and we can view them as a linear equation system A¯x = ¯b. Every satisfiable system of linear equations has a rational solution and a vector ¯x is a solution if and only if it can be expressed as ¯x = ¯ c + x1 ¯ v1 + . . . + xk ¯ vk where A¯ vi = ¯0, A¯ c = ¯b, ¯ c, ¯ v1, . . . , ¯ vk are rational vectors, and x1, . . . , xk are real numbers.

Since ¯ r satisfies A¯ r = ¯b, it can be expressed as ¯ r = ¯ c + r1 ¯ v1 + . . . rk ¯ vk, with ri ∈ R. The rational numbers are dense in the real numbers so we can find rational numbers qi satisfying |ri - qi| < δe for all i and for any δe > 0. Let ¯ q = ¯ c + q1 ¯ v1 + . . . + qk ¯ vk and we find that ||¯ r - ¯ q|| = ||(r1 - q1)¯ v1 + . . . + (rk - qk)¯ vk|| ≤ |r1-q1|·||¯ v1||+. . .+|rk-qk|·||¯ vk|| < δe·(||¯ v1||+. . .+||¯ vk ||). By choosing ¯ q so that δe gets sufficiently small, we can achieve ||¯ r - ¯ q|| < δ. It follows that ¯ q satisfies l0j0 ∧ l1j1 ∧ . . . ∧ lnjn . □

Thus, HR satisfies requirement 1) and 3) of Lemma 4. We let ΛZ ⊆ HZ contain the relations that satisfy requirement 2) and have thus proved the following.

Theorem 6 The problem, CSP(ΛZ) is tractable.

We now verify that ΛZ is maximally tractable in HZ. We need the concept of reduced relations.

Definition 7 [Bodirsky et al., 2010a] Let θ(x1, . . . , xn) be a formula in conjunctive normal form. We call θ reduced if it is not logically equivalent to any of its subformulas, i.e. there is no formula ψ obtained from θ by deleting literals of clauses such that θ(a) = ψ(a) for all a ∈ Zn .

An important property of reduced formulas is that if R is defined by a reduced formula l1 ∨ . . . ∨ ln, then for each li, we can find a vector ¯x that satisfies li but not lj for all j ̸= i.

Theorem 8 CSP(ΛZ) is maximally tractable in CSP(HZ).

Proof: Let R be an arbitrary relation (of arity n) in HZ that does not satisfy requirement 2). Hence, there exists a real nvector ¯ y and an infinite set S ⊆ R such that ¯ y satisfies R but for every s ∈ S, s¯ y does not satisfy R. Assume without loss of generality that R is defined by a reduced formula l1(¯x) ∨ ... ∨ lk(¯x) where l1, . . . , lk are linear expressions.

Suppose that some li ≡ p(¯x) ̸= c where c ̸= 0. If p(¯ y) ̸= c, then p(k¯ y) ̸= c for all k ∈ R+ except at most one, and the same holds for R(k¯ y). If p(¯ y) = c, then p(k¯ y) ̸= c for all k ∈ R+ except at most one, and the same holds for R(k ¯ y). This leads to a contradiction and we can assume that if a literal li ≡ p(¯x) ̸= c, then c = 0.

If ¯ y satisfies some literal li ≡ p(¯x) ̸= 0, then p(k¯ y) ̸= 0 for all k ∈ R except at most one, and the same holds for R(k¯ y). Thus, ¯ y only satisfies a literal lj ≡ q(¯x)ra where r ∈ {<,≤ ,=,≥,>}. By observing that p(¯x) < a ⇔ p(¯x) ≤ a - 1, we may additionally assume that r ∈ {≤,=,≥}. Assume without loss of generality that a ≥ 0; if a < 0, then consider the equivalent inequality obtained by multiplying with -1. If r = (≥), then k¯ y satisfies R for all k ≥ 1. Thus, r ∈ {≤, =}. If p(¯ y) = 0, then k¯ y satisfies R for all k ∈ R so we can safely assume that a > 0. We conclude that R is on one of the following forms: (1) p(¯x) = a∨q1(¯x) ̸= 0∨. . .∨qn(¯x) ̸= 0 or (2) p(¯x) ≤ a ∨ q1 ̸= 0 ∨ . . . ∨ qn(¯x) ̸= 0 where a > 0.

Assume first that R is of type (1). In ΛZ ∪ {R}, we can pp-define the following relation:

The definition of R is reduced so there exists a vector ¯x such that p(¯x) = a and qi(¯x) = 0, 1 ≤ i ≤ n. Thus, S(z) holds if and only if z = a; in other words, we have defined a non-zero constant. This implies that we can pp-define the constant 1 since z = 1 ⇔ ∃x1, ..., xa, y.z = x1∧S(y)∧x1 ≥ 1 ∧ . . . ∧ xa ≥ 1 ∧ y = x1 + . . . + xa. It is now straightforward to pp-define the relation T0,1 and we have proved that CSP(Γ ∪ {R}) is locally NP-hard.

Assume instead that R is of type (2). Analogously to the construction of S, we can construct a non-empty unary relation S′ that is upper bounded by a. Thus, S′ contains a largest element b and the constant b can be pp-defined since z = b ⇔ S(z)∧z ≥ b. The proof procedes as above. □

The maximality proof also gives a characterisation of the relations R ∈ HZ that do not satisfy requirement 2): given a relation R, reduce it and check whether it is of one of the two 'bad' types identified in the proof. The maximality proof can also be generalised to a hardness result for constraint languages that are not necessarily subsets of HZ.

Corollary 9 Let Γ be a constraint language over Z such that the relations x = y + z and x ≥ 1 are in 〈Γ〉. Then, Γ ∪ {R} is NP-hard whenever R ∈ HZ \ ΛZ.

Proof: (Sketch) By Theorem 2, we may without loss of generality assume that x = y + z and x ≥ 1 are members of Γ. By inspecting the proof of Theorem 8, we see that CSP({R} ∪ X) is NP-hard where X is a finite set of homogeneous equations and (possibly) a relation p(¯x) ≥ a with a > 0. Every homogeneous equation can be pp-defined with the aid of x = y + z. Every relation x ≥ a with a > 0 can be pp-defined since x ≥ a ⇔ ∃y1, . . . , ya.x = y1+. . .+ya∧y1 ≥ 1∧...∧ya ≥ 1 and the equation x = y1 + . . . + ya is homogeneous. Thus, p(¯x) ≥ a can be pp-defined since p(¯x) ≥ a ⇔ ∃y.y = p(¯x) ∧ y ≥ a. □

3 Linear equations

In the previous section, we found a large maximally tractable subset ΛZ of HZ. Clearly, ΛZ does not contain any linear equations p(¯x) = a with a ̸= 0. We will now look at fragments of HZ that contain such equations. Similar fragments have been considered before: it is known that finding integer solutions to linear equation systems is a tractable problem [Kannan and Bachem, 1979]. A related problem has also been discussed in [Bodirsky et al., 2010b, Section 6] but they restrict themselves to homogeneous equations. We will now work 'backwards' compared to the previous section; instead of starting with HZ and remove relations, we will extend the set of linear equations.

The algorithmic part will use results from [Cohen et al., 2000] and a property known as 1-independence. We note that the original definitions by Cohen et al. are slightly more general than those presented here; they do not restrict themselves to constraint languages. By the notation CSPΔ≤k(Γ∪Δ), we mean the CSP problem with constraints over Γ∪Δ but where the number of constraints over Δ is less than or equal to k.

Definition 10 For two constraint languages Γ and Δ, we say that Δ is k-independent with respect to Γ if the following condition holds: any instance I of CSP(Γ∪Δ) has a solution provided every subinstance of I belonging to CSPΔ≤k(Γ ∪ Δ) has a solution.

1-independence gives us a way to handle disjunctions efficiently. For constraint languages Γ and Δ, let the constraint language Γ×∨Δ∗ contain all relations R(¯x) ≡ c(¯x) ∨ d1(¯x) ∨ . . . ∨ dn(¯x), n ≥ 0, where c(¯x) is a constraint over Γ and d1(¯x), . . . , dn(¯x) are constraints over Δ.

Theorem 11 [Cohen et al., 2000] Let Γ and Δ be constraint languages. If CSPΔ≤1(Γ ∪Δ) is globally tractable, and Δ is 1-independent with respect to Γ, then CSP(Γ×∨Δ∗ ) is globally tractable.

Let Γ ⊆ HZ denote all relations p(¯x) = b and Δ ⊆ HZ denote all relations p(¯x) ̸= b. We will now prove that CSP(Γ×∨Δ∗ ) is globally tractable (Theorem 12) and that it is a maximal tractable fragment of HZ (Theorem 13). We will also extend the maximality result in a way similar to Corollary 9; the omitted proof is analogous.

Theorem 12 CSP(Γ×∨Δ∗ ) is globally tractable.

Proof: We first prove that Δ is 1-independent with respect to Γ. Let IΓ be an instance of CSP(Γ) and IΔ an instance of Δ. Assume that IΓ ∪{di} is satisfiable for each di ∈ IΔ with di ≡ pi(¯x) ̸= ci.

We will perform an induction on the size of IΔ. If |IΔ| = 1, then satisfiability follows from the assumptions. Assume that |IΔ| = d, d > 1, and that the statement holds for all I ′Δ ⊂ IΔ. We show that IΓ ∪ IΔ is satisfiable, too.

Let I iΔ = IΔ \ {pi(¯x) ̸= ci} and consider the instance IΓ ∪ I iΔ for each i. Let Di, 1 ≤ i ≤ d, be the set of satisfying points to these subproblems. The sets D1, . . . ,Dd are nonempty due to the induction hypothesis. Arbitrarily choose an element ¯xi ∈ Di for each i. If ¯xi ∈ Dj for any j ̸= i, then it is a solution to the entire instance and we are done. So we can assume that pi(¯xi) = ci for all i.

Take two points ¯x1 and ¯x2 and define ¯xk = k¯x1 + (1 - k)¯x2 for k ∈ Z. Observe that ¯xk satisfies IΓ for all k. We will now show that there is a k such that ¯xk ∈ Di for all i; by the previous comment, it is sufficient to consider the disequations.

For i = 1 we note that p1(¯xk ) ̸= c1 ⇔ kp1(¯x1) + (1 - k)p1(¯x2) ̸= c1 ⇔ (1 - k)(p1(¯x2) - c1) ̸= 0 and since p(¯x2) ̸= c1 this is true for all k ̸= 1. In the same way, we see that ¯xk ∈ D2 when k ̸= 0.

For i ̸= 1, 2, we note that if pi(¯x1) = d1 ̸= ci and pi(¯x2) = d2 ̸= ci, then pi(¯xk ) = k(d1-d2)+d2. If d1 = d2, then the disequation is always true; otherwise, there is at most one value for k such that pi(¯xk ) = ci. Hence, each disequation is not satisfied by ¯xk for at most one value of k, and we conclude that there is some k′ such that ¯xk′ ∈ Di for all i. It follows that IΓ ∪ IΔ is satisfiable for any size of IΔ.

By Theorem 11, it is now sufficient to prove that CSPΔ≤1(Γ∪ Δ) is tractable. Let I be an instance of CSPΔ≤1(Γ ∪ Δ). We view I as an equation system A¯x = ¯b together with a disequation p(¯x) ̸= c. We start by finding a satisfying integer point ¯x to A¯x = ¯b; this is tractable by [Kannan and Bachem, 1979]. If no such point exists, then I is not satisfiable. If the found solution ¯x also satisfies p(¯x) ̸= c, then we have found a solution to I, too. Otherwise, note that if ¯ y ̸= ¯x and A¯ y = ¯b, then A(¯ y - ¯x) = ¯b - ¯b = ¯0. By letting ¯xh = ¯ y - ¯x, we see that any satisfying point ¯ z can be written as ¯ z = ¯x + ¯xh for some ¯xh such that A¯xh = ¯0. Since p(¯x) = c, we note that p(¯ z) ̸= c ⇔ p(¯x) + p(¯xh) ̸= c ⇔ p(¯xh) ̸= 0. From this we conclude that we can find a solution to I if and only if we can find a point ¯xh such that A¯xh = ¯0 and p(¯xh) ̸= 0.

Now we solve the system A¯x = ¯0 ∧ p(¯x) = 1 over the rational numbers. If this system has no solution, then there is no point ¯xh since some rational multiple of ¯xh would have been a solution. If we find a solution ¯xq to this system, then there exists an integer k ̸= 0 such that k¯xq is an integer point satisfying Ak¯xq = ¯0 and p(k¯xq) = k ̸= 0. We see that we can let ¯xh = k¯xq and conclude that I is satisfiable. As this only requires solving two linear systems, one over the integers and one over the rational numbers, this is a polynomial-time algorithm for solving CSPΔ≤1(Γ∪Δ). □

Theorem 13 Γ×∨Δ∗ is maximally tractable in HZ.

Proof: The relations in HZ \ (Γ×∨Δ∗ ) are of the form R ≡ p(¯x) ≤ c ∨ ∨ni=1 (qi(¯x) ̸= ai). Note that we do not have to consider relations with < separately since those are always equivalent to a relation using ≤. We assume without loss of generality that the definition of R is reduced.

We will now show how to pp-define Tz0,z1 for some z0 ̸= z1 in Z. By reasoning as in the proof of Theorem 8, we see that we can pp-define a unary relation S(z) that is a subset of {z ∈ Z | z ≤ c} by S(z) ≡ ∃¯x.(z = p(¯x)) ∧ (p(¯x) ≤ c ∨ ∨ni=1 (qi(¯x) ̸= ai)) ∧ (∧ni=1 (qi(¯x) = ai)).

We first prove that |S| > 1. If |S| = 0, then (∧ni=1 (qi(¯x) = ai)) ⇒ p(¯x) > c but since the definition of R is reduced, we know that there exists an integral vector ¯x satisfying p(¯x) ≤ c. If |S| = 1, then ∧ni=1 (qi(¯x) = ai)) ⇒ p(¯x) = d for some d ≤ c but then R = Zn and we have a contradiction since R ∈ Γ×∨Δ∗ . To see this, let ¯x be an arbitrary vector in Zn . If it satisfies one of the disequations, then we are done. Otherwise, p(¯x) = d and it clearly satisfies the inequality p(¯x) ≤ c. Consequently, |S| > 1.

Define z0 = max{z | S(z)} and z1 = max{z | S(z), z ̸= z0} and note that these constants are pp-definable in Γ∪{R}. Now, Tz0,z1 (x, y, z) ≡ S(x) ∧ S(y) ∧ S(z) ∧ x + y + z = (2z0 + z1) and NP-hardness follows from Theorem 2. □

Corollary 14 Let Γ be a constraint language over Z such that the relations x = y + z and x = 1 are in 〈Γ〉. Then, Γ ∪ {R} is NP-hard whenever R ∈ HZ \ (Γ×∨Δ∗ ).

4 Constraints that are k-valid

We will now demonstrate that there are an infinite number of distinct maximally tractable fragments within HZ. This fact makes complexity classifications harder since a description of the tractable cases must be more elaborate than just listing the maximally tractable fragments.

A relation R is said to be k-valid, k ∈ Z, if (k, . . . , k) ∈ R. A constraint language Γ is k-valid if every relation in Γ is kvalid. Let Γk, k ∈ Z, denote the set of k-valid relations in HZ together with the empty relation. Clearly, Γi ̸= Γj whenever i ̸= j; Γi contains the relation (x = i) but does not contain (x = j) and vice versa. Solving instances of CSP(Γk) is obviously trivial (simply check whether some constraint is based on the empty relation) but such classes have to be considered, too, in order to obtain full complexity classifications. The maximality proof for k-valid constraints differs slightly from the proofs in the preceeding sections. There, we managed to construct explicit NP-hard constraint languages. This proof is slightly non-constructive since we obtain a sequence of constraint languages and prove that (at least) one of them is NP-hard. However, we do not know which one.

For distinct a, b, c ∈ Z, define T ′a,b,c (x, y) ≡ {a, b, c}2 \ {(a, a), (b, b), (c, c)}. CSP({T ′a,b,c }) is an NP-hard problem since it corresponds to the 3-COLOURABILITY problem.

Theorem 15 For each k ∈ Z, Γk is a maximally tractable language in HZ.

Proof: The problem CSP(Γk) is obviously globally tractable. To prove maximality, arbitrarily choose a relation R ∈ HZ that is not k-valid. Let m denote the arity of R and consider the following relations:

The relations U1, . . . ,Um+1 are pp-definable in Γk ∪ {R} since the relation y = k is k-valid. We claim that there exists an index 1 ≤ j ≤ m such that Uj ̸= ∅ and k ̸∈ Uj. Since R is not k-valid, it follows that Um+1 = ∅ so there exists a smallest index 2 ≤ j ′ ≤ m+ 1 such that Uj ′ = ∅. Let j = j ′ - 1. Clearly, Uj is non-empty and if k ∈ Uj, then Uj+1 = Uj ′ is non-empty which leads to a contradiction.

We now let ca(z) ≡ (z = a) and pp-define the relation ck′(z) for some k′ ̸= k. Assume without loss of generality that there is some element in Uj that is larger than k; if not, then there is some element in Uj that is smaller than k and the reasoning is symmetric. Let k′ = min{x ∈ Uj | x > k} and note that z = k′ ⇔ Uj(z) ∧ (z ≥ k) ∧ (z ≤ k′ ). The relations (z ≥ k) and (z ≤ k′ ) are both k-valid so (z = k) is pp-definable in Γk ∪ {R}. Using the relation z = k′ , we conclude the proof by the following pp-definition: T ′k-1,k,k+1 (x, y) ≡ ∃z, w.(z = w∨x ̸= y)∧ck(z)∧ck′ (w)∧ ∧(k - 1 ≤ x) ∧ (x ≤ k + 1) ∧ (k - 1 ≤ y) ∧ (y ≤ k + 1). NP-hardness of CSP({T ′k-1,k,k+1 }) implies NP-hardness of CSP(Γk ∪ {R}) via Theorem 2. □

5 Discussion

The results reported in this paper constitute a step towards a better understanding of the complexity of temporal reasoning in discrete time structures. Below, we discuss how this work can be continued.

5.1 Horn DLRs

Completely classifying the complexity of CSP(HZ) appears to be a quite hard problem. Consider the NP-complete integer feasibility problem: given a system of inequalities Ax ≥ b, decide whether there exists a satisfying integer vector x or not. Note that each row of the system can be viewed as a relation in HZ. Thus, a complete classification of CSP(HZ) would give us a classification of the integer feasibility problem (parameterised by allowed row vectors). Such a classification is not currently known and, in fact, there are no classifications even if we restrict ourselves to finite domains or if we consider the closely related integer optimisation problem.

One obvious difficulty when classifying CSP(HZ) is that we do not know what algorithmic techniques will be needed. The results in this paper are based on either solving linear equations or solving linear programming problems over the real numbers. Completely different methods may be needed in other cases, though. As a concrete example, consider the constraint language Γ containing all relations of the type ax+ by = c, x ≤ c, and x ≥ c (where a, b, c ∈ Z) and note that Γ ⊆ HZ. Bodirsky et al. [2009] have shown that CSP(Γ) is tractable by using a graph-theoretic approach; it is not clear how (or if) this algorithm can be recast in more familiar terms.

Another difficulty is that there are tractable cases where we have not been able to prove maximality. One example is the previously mentioned class by Bodirsky et al. Another example is constraints of the types ax - by ≤ c and ax - by = c where a, b ∈ {0, 1} and c ∈ Z. Let ΣZ denote the corresponding constraint language. The tractability of CSP(ΣZ) problem follows from combining Theorem 19.1 and Theorem 19.3(iv) in [Schrijver, 1986] with the fact that linear programs can be solved in polynomial time. This result is interesting since it implies tractability of the discrete-time analogue of Dechter et. al's [1991] well-known simple temporal networks.

Deciding maximality for ΣZ and similar classes appear to be non-trivial. Apparently, ΣZ may be difficult to extend with disequality relations p(¯x) ̸= a. It is, for instance, straightforward to prove that CSP(ΣZ ∪{x ̸= y}) is NP-hard. It may be the case that ΣZ can be extended in other ways, though.

5.2 Semilinear relations and DLRs

If we turn our attention to semilinear relations and DLRs, then we immediately note that they give rise to a much richer class of CSPs than Horn DLRs. The following is an interesting consequence: for every finite constraint language Γ over a finite domain D, there exists a finite set Γ′ ⊆ SZ such that CSP(Γ) and CSP(Γ′ ) are polynomial-time equivalent. This can be demonstrated as follows: given a relation R ⊆ Dk where D = {d1, . . . , dm} is finite, define R′ (x1, . . . , xk) ≡ ∧ki=1 (xi = d1 ∨ . . . ∨ xi = dm) ∧ ∧(t1,...,tk)∈Dk ,(t1,...,tk)̸∈R(x1 ̸= t1 ∨ . . . ∨ xk ̸= tk). It is now straightforward to see that R′ is a semilinear relation and that CSP({R}) is polynomial-time equivalent to CSP({R′ }). This idea is straightforward to extend to constraint languages, so a complete classification of CSP(SZ) would also constitute a complete classification of finite-domain CSPs. Such a classification has for many years been a major open question within the CSP community. We can also observe that the resulting constraint language Γ′ is typically not a subset of DZ. The simpler structure of DZ may very well simplify the classification task. We note that the finite-domain CSP problem for so-called clausal relations is completely classified [Creignou et al., 2008], and this kind of relations are defined by single clauses satisfying certain properties.

When studying the complexity of CSP(SZ) and CSP(DZ), it appears that the known sources of tractable fragments increase drastically. An obvious example are the relations that are first-order definable over (Q; <). Every tractable subclass has been identified by Bodirsky and Kara [2010] so we let Γ denote one of their tractable classes. The structure (Q;<) admits quantifier elimination and Γ ⊆ SZ. By combining this fact with Lemma 4, it can be shown that an instance I of CSP(Γ) has a solution if and only if I|Z has a solution. Thus, CSP(Γ|Z) is tractable, too. Note that there is no a priori reason to believe that Γ|Z is maximally tractable within DZ or SZ (even though Γ is maximal within the relations that are first-order definable within (Q,<)). It may be the case that there are many different tractable classes that contains Γ|Z.