Constraint Programming on Infinite Data Streams

1 Introduction

The standard domains of classical Constraint Satisfaction Problems (CSPs) [Dechter, 2003] are of simple types, such as integers, reals, and sets, which are inadequate in describing problems with values that change over time. Discrete simulation of a person juggling indefinitely is an example of constrained time-varying problems with discrete time points. Changing continuously, the loci of the balls are governed by the juggler's throws, juggling rules, and laws of physics. In addition, an experienced juggler should be able to exhibit non-repetitive patterns so long as all the rules and laws are obeyed. Modeling such a problem as a CSP would require an infinite number of variables and constraints.

We propose Constraint Programming on infinite data streams, which are difficult to manipulate due to the lack of finite representation, especially for non-periodic ones. The domains of stream variables are represented compactly using ω-regular languages which are recognizable by B¨uchi automata [B¨uchi, 1962]. Different from model checking, the automata are modified during search and synthesized into different stream values. We define stream operators (a la Lucid

Y. C. Law, J. H. M. Lee, and C. F. K. Siu Department of Computer Science and Engineering The Chinese University of Hong Kong Shatin, N.T., Hong Kong

{yclaw,jlee,fksiu}@cse.cuhk.edu.hk

[Wadge and Ashcroft, 1985]) and constraints. The searching approach used in classical CSP is no longer practical due to infinite domain size. We propose a search scheme which limits our attention to a window of time points. Consistency enforcement is integrated to the search procedure to eliminate infeasible search space. We have implemented a prototype solver, which is used to model and solve the simulation of juggling and jazzy harmonization of music as proof of concept.

2 Infinite Data Streams

Streams are infinite sequences of data items, called datons, over natural number time points. A stream α is an ordered sequence 〈α(0), α(1), α(2), . . .〉, where α(i) is a daton of α at time point i ≥ 0. We use α(i, j), 0 ≤ i ≤ j, to denote the finite string 〈α(i), α(i + 1), . . . , α(j)〉. In particular, α(i,∞) is the stream 〈α(i), α(i + 1), . . .〉. We overload these notations to apply on a set of stream values similarly. Given a set of streams S, S(i) = {α(i) | α ∈ S} and S(i, j) = {α(i, j) | α ∈ S}.

Without loss of generality, we assume that datons are of the same type. In particular, we focus on integer (Z) streams in this paper. For example α = 〈1, 2, 3, 2, 4, 5, . . .〉 is an integer stream, in which α(2) = 3, α(1, 3) = 〈2, 3, 2〉, and α(3,∞) = 〈2, 4, 5, . . .〉.

An ω-regular language generalizes a regular language to a set of infinite strings (a la streams), and can be expressed as a finite union ∪ni=0UiV ω i where Ui and Vi are regular languages and the empty string ϵ /∈ Vi. The ω operator in V ω i indicates the infinite concatenation of the regular language Vi. In this paper, we are interested only in problems whose solution sets are ω-regular languages.

A B¨uchi automaton over an alphabet Σ is a 4-tuple A = (Q, q0,△, F) where Q is a finite set of states, q0 ∈ Q is an initial state, △ ⊆ Q × Σ × Q is a transition relation, and F ⊆ Q is the set of final states. The automaton A accepts an infinite string if and only if there exists a run of the automaton which visits at least one of the final states infinitely often. An ω-regular language is recognizable by a B¨uchi automaton. We use L(A) to denote the ω-regular language recognized by A.

Temporal operators are defined over streams. The unary first operator gives the stream formed by repeating the first daton of the stream. Formally, first α = β, where

∀i ≥ 0, β(i) = α(0). The unary next operator gives the stream formed by removing the first daton of the stream. Formally, next α = α(1,∞). The binary fby operator takes two streams and gives the resulting stream by concatenating the first daton in the first stream and the second stream. Formally, α fby β = γ where γ(0) = α(0) and ∀i ≥ 1, γ(i) = β(i - 1).

In addition to temporal operators, pointwise operators are extensions to functions defined over integers. Given an n-ary function f : Zn ↦→ Z, an extension of f to a corresponding pointwise operator f is defined by f(α1, α2, . . . , αn) = β where ∀i ≥ 0, β(i) = f(α1(i), α2(i), . . . , αn(i)). In particular, we highlight some useful pointwise operators, which will be used in infix notation as usual. Arithmetic operators, including +, -, ×, and / (integer division) on numbers are the extension of the usual operators over integers. When the streams are pseudo-Boolean streams, containing only datons 0 (false) and 1 (true), there are logical operators and, or, and not. Relational operators determine the truth of relation on the stream values pointwisely and return a pseudo-Boolean stream. The operators include ==, <>, <=, and >= on numbers.

A stream expression can involve different operators as in "α + β - (γ fby (next α))".

3 StreamConstraint Satisfaction

A Constraint Satisfaction Problem (CSP) P is a tuple (X,D, C) where X is a finite set of variables, D is a finite set of (variable) domains, and C is a finite set of constraints. A variable X ∈ X can only take a value from its corresponding variable domain D(X) ∈ D. Each constraint C ∈ C has scope(C) corresponding to the list of variables involved in C. A constraint C limits the combinations of values that can be taken by the variables in scope(C). A solution to a CSP is an assignment of values from the variable domains to all variables such that all constraints in P are satisfied simultaneously. We denote the set of solutions to CSP P as sol(P).

3.1 StreamConstraints

Stream constraints are relations on stream expressions, which are composed of stream variables, stream constants, and stream operators. Stream constants have the same daton over all the time points which are denoted with the daton in bold, such as 2 = 〈2, 2, 2, . . .〉. The relations can be =, ̸=, ≥, ≤, and → (implication), which are all enforced pointwisely. An example constraint is "X + 3 = Y fby Z". When the constraints involve ≥ or ≤, the set of datons, such as Z in this paper, is assumed to have some ordering.

A stream constraint C ∈ C with scope(C) = (X1,X2, . . . ,Xn) is a subset of (Zω )n , i.e. C ⊆ (Zω )n . Relational operators are different from stream relations. The former are functions returning pseudo-Boolean streams, while the latter are constraints to be enforced.

In a Stream CSP (St-CSP), variables take on stream values so that domains are possibly infinite sets of streams. Expressions and constraints involving streams are those defined earlier. We require stream variable domains to be ω-regular languages. For simplicity, initial domains are specified in the form of Σω where Σ is the set of possible datons at each time point.

The following shows an example St-CSP having variables X, Y , and Z, with domains D(X) = D(Y ) = D(Z) = (0|1|2)ω , where " | " denotes choice. The two constraints are:

X = next Y +1 and Y =X fby Z This problem has infinitely many solutions. Three such solutions are: (a) {X = (1)ω , Y = 1(0)ω , Z = (0)ω }, (b) {X = 121(2)ω , Y = 1010(1)ω , Z = 010(1)ω }, and (c) {X = 211(212)ω , Y = 2100(101)ω , Z = 100(101)ω }. For example, solution (b) satisfies all constraints since "next Y " gives 010(1)ω and "010(1)ω + 1" is 121(2)ω which is equal to X's value. Furthermore, "X fby Z" takes the first daton of X, i.e., 1, followed by the stream Z = 010(1)ω , which gives 1010(1)ω and is equal to Y 's value.

An St-CSP can be viewed as a classical CSP with an infinite number of variables and constraints. A stream variable X corresponds to an infinite sequence of daton variables 〈X(0),X(1), . . .〉 in which D(X(i)) = D(X)(i). Similarly, a stream constraint C corresponds to an infinite sequence of daton constraints C(0), C(1), . . .. Each daton constraint C(i) of C can be obtained by applying translation operation Ti with the rules listed in Table 1 such that Ti(C) gives C(i). Thus, each stream constraint C is translated to the set {Ti(C) | i ≥ 0}. For example, the stream constraint "X = Y fby Z" at time point 0 is translated by Rule 3 from "T0(X = Y fby Z)" to "T0(X) = T0(Y fby Z)", and then by Rules 6 and 1 to "X(0) = Y (0)". For time point i > 0, "Ti(X) = Ti(Y fby Z)" is translated by Rule 7 to "Ti(X) = Ti-1(Z)", and then by Rule 1 to "X(i) = Z(i - 1)". Therefore, the stream constraint is equivalent to the conjunction of daton constraints: X(0) = Y (0),X(1) = Z(0),X(2) = Z(1), . . .. An St-CSP P = (X,D, C) can be viewed as a classical CSP P ′ = (X ′ ,D′ , C ′ ) where X′ = {X(i) | i ≥ 0 ∧ X ∈ X}, ∀X(i) ∈ X ′ ,D′ (X(i)) = D(X)(i), and C ′ = {Ti(C) | i ≥ 0 ∧ C ∈ C}.

3.2 Characterizing the Solution Space

We consider a variable assignment as a tuple. The solution set of an St-CSP contains possibly infinite number of tuples of streams. We introduce the ⊗ operator on streams such that α1 ⊗ α2 ⊗ . . . ⊗ αn = 〈(α1(0), α2(0), . . . , αn(0)), (α1(1), α2(1), . . . , αn(1)), . . .〉. The operator turns a sequence of streams into a stream of tuples of corresponding datons. Then, given a set of tuples of streams S, we define L(S) = {α1 ⊗ α2 ⊗ . . . ⊗ αn | (α1, α2, . . . , αn) ∈ S}.

Lemma 1. L(sol(P)) is isomorphic to sol(P).

Lemma 2. Given a stream constraint C, L(C) is an ωregular language.

The solution set of an St-CSP is, mathematically, the conjunction of constraints and the Cartesian product of variable domains. Since stream domains and stream constraints are ωregular languages, by the closure of operations for ω-regular languages [Thomas, 1990], we have the following theorem.

Theorem 1. Given an St-CSP P, L(sol(P)) is an ω-regular language.

Proof. We prove it by induction. When there is one stream variable in the problem P, the set of solutions L(sol(P)) is the conjunction of the initial domain and the set of constraints. Since domains and constraints are ω-regular languages, by the closure of ω-regular languages over conjunction, the resulting set is also an ω-regular language. Given two ω-regular languages L1 and L2, we let S = {(α1, α2) | α1 ∈ L1, α2 ∈ L2}. Since S is an ω-regular language, the induction applies.

Thus we can solve an St-CSP by constructing a B¨uchi automaton for L(sol(P)). In addition, by the nature of ωregular languages, solution streams of an St-CSP can be nonperiodic.

4 Solving StreamCSPs

An St-CSP has infinite domains. The tree search method [Dechter, 2003] widely applied in solving traditional finite domain CSPs is not applicable in this case as stream variable domains can never be enumerated exhaustively. We propose a depth-first search approach which determines the datons in the stream variables in the order of time points. We define a dominance relation among the search states or nodes so that when a search state is dominated by an ancestor node in the search tree, the search down that branch can terminate.

4.1 Search Tree

A search state is an St-CSP P. Given P1 = (X1,D1, C1) and P2 = (X2,D2, C2), P1 is a sub-problem of P2, denoted P1 ⊆ P2, when X1 = X2, D1 ⊆ D2, and C1 = C2. In a search tree, a parent search state P has a finite set of child states P ′ i such that ∀i,P ′ i ⊆ P ∧ ∪isol(P ′ i ) = sol(P).

Figure 1 shows the first 7 nodes of the search tree for an St-CSP P, having variables X and Y with the initial domains D(X) = D(Y ) = (1 | 2)ω and a constraint X = first Y . The search procedure attempts to determine the daton assignment in the order of increasing time points. We define the current time point of a variable X as t(X) which is the maximum time point before which all the daton variables of X can be fixed according to D(X). Formally, t(X) = min{i | i ≥ 0 s.t. |D(X)(i)| > 1}. The current time point of an St-CSP P, t(P) is the minimum current time point among all the variables in P, i.e. t(P) = min{t(X) |X ∈ X}. Thus, there exists at least one variable whose daton variable at time point t(P) is unbound in a given P. When t(P) = ∞, all the daton variables are bound. For example, in P2 of the search tree in Figure 1, the datons in both domains D2(X) and D2(Y ) are fixed up to time point 0; therefore t(P2) is 1.

In each search state P, a variable X with t(X) = t(P) is selected. With each d ∈ D(X)(t(P)), P is branched with the assignment X(t(P)) = d. In Figure 1, upon completion of assignment to datons in time point 0 at P2, the search selects a variable with current time point as t(P2) for daton assignment. The search tree here first selects X(1) and branches for X(1) = 1 and X(1) = 2 respectively.

Note that t(P0) = t(P1) = 0, but t(P2) = t(P1) + 1. We say that there is an advancement of current time point from P1 to P2 but not from P0 to P1. We define the set of search states with advancement of current time point from their parent search states plus P0 to be Φ = {Pi | t(parent(Pi)) < t(Pi)}∪{P0}, where parent(P) gives the parent search state of P and P0 is the root node of the search tree. Each search state in Φ corresponds to a complete assignment to all daton variables at and before a time point. In the search tree in Figure 1, Φ includes P0, P2, P4, and P5 among the first 7 nodes.

Since the streams are defined on infinite time points, the search procedure will advance the time point forever. To avoid infinite search, we define the notion of dominance of one search state over another. A search state Pi = (X,Di, C) is dominated by Pj = (X,Dj, C), denoted as Pi ≺ Pj, if and only if Pi,Pj ∈ Φ, Pj is an ancestor of Pi, and ti = t(Pi), tj = t(Pj), ∀X ∈ X,Di(X)(ti,∞) = Dj (X)(tj , ∞)∧∀C ∈ C, ∏X∈scope(C) Di(X)(ti, ∞)∩C = ∏X∈scope(C) Dj(X)(tj,∞) ∩ C. The conditions for dominance ensure the solution space of both Pi and Pj , when only considering the time points after t(Pi) and t(Pj) respectively, is the same, since the domains are the same and each constraint represents the same set of tuples of streams.

The search states P4 and P5 in Figure 1 are dominated by P2. Since D4(X)(2,∞) = D2(X)(1,∞), D4(Y )(2,∞) = D2(Y )(1,∞) and ((D4(X) × D4(Y )) ∩ C)(2,∞) = ((D2(X) × D2(Y )) ∩ C)(1,∞) = ((1, 1) | (1, 2))ω . This is similar for P5.

Suppose Pi is dominated by Pj , where Pi, Pj ∈ Φ. There is a path from Pj to Pi in the search tree. The path corresponds to a sequence of daton assignments, denoted as s, between time points t(Pj) and t(Pi) - 1. Therefore, for all α ∈ L(sol(Pi)), sα ∈ L(sol(Pj)), where sα is s appended with α. As Pi and Pj share the same solution space after a certain time point, such operation can be done infinitely many times and sω is one of the solutions to Pi and Pj. For example, in Figure 1, the path fromP2 to P4 corresponds to the assignment {X(1) = 1, Y (1) = 1}. Since P4 is dominated by P2, the solution space of P2 is the same as that of P4 after 1 time point. Therefore, the assignment {X(i) = 1, Y (i) = 1} can always be satisfied and {X = (1)ω , Y = (1)ω } is one of the solutions.

As the domains can be infinite, the computation of conjunction of constraints and domains is infeasible. We propose simple and sufficient conditions for dominance detection. Given an St-CSP P = (X,D, C). As all the datons are fixed before time point t(P), we limit our attention to time point t(P) and onwards. We define a limited view of P to be ˆ P = (X, ˆD, ˆ C), which can be obtained from P by removing the time points from 0 to t(P) - 1 such that ∀X ∈ X, ˆD(X) = D(X)(t(P),∞) and ˆ C = { ˆ C(i) | ∀i ≥ 0,C ∈ C } where ˆ C(i) is C(i) with all the occurrences of X(i), i < t(P), replaced by the assigned values to X(i)'s.

Theorem 2. Given Pi,Pj ∈ Φ. If ˆ Pi = ˆ Pj and Pj is an ancestor of Pi, then Pi ≺ Pj .

Proof. Suppose Pi = (X,Di, C), Pj = (X,Dj, C), ti = t(Pi), and tj = t(Pj). Since Pi,Pj ∈ Φ and, Pj is an ancestor of Pi, we only have to show that when ˆ Pi = ˆ Pj, (1) ∀X ∈ X,Di(X)(ti,∞) = Dj(X)(tj,∞) and (2) ∀C ∈ C, ∏X∈scope(C) Di(X)(ti,∞) ∩ C = ∏X∈scope(C) Dj (X)(tj , ∞) ∩ C are true.

ˆ

ˆ

When Pi = Pj, condition (1) is satisfied by the definition of limited view, as ∀X ∈ X, ˆ Di(X) = ˆ Dj(X). Since ∀C ∈ C, ˆ Ci = ˆ Cj and by condition (1), condition (2) is also satisfied.

Next, we analyze the termination and complexity of this search approach. From Table 1, we observe that different translation rules are applied to the fby operator depending on the time point i. A stream constraint C, in which the maximum nested applications of fby is n, for all time points i ≥ n, Ti(C) is translated with the same set of rules. Therefore, we have the following property.

Property 1. Given a stream constraint C with n nested applications of fby. ∀i > n, Ti(C) share the same structure as Tn(C).

Two daton constraints C(i) and C(j) share the same structure when C(i) becomes C(j) after replacing i by j. Take the above stream constraint "X = Y fby Z" as an example, since there is only one fby operator, for all time points i ≥ 1, the daton constraint is X(i) = Z(i - 1).

ˆ

ˆ

When Pi = Pj, Pi and Pj share the same search space after t(Pi) and t(Pj) respectively. The order of variable assignment in the search strategy divides the time line into three parts: (1) all daton variables are fixed, (2) some daton variables are fixed, and (3) no daton variables can be fixed. For example, the search state P3 in Figure 1, the window of part (1) is [0, 0], that of part (2) is [1, 1], and that of part (3) is [2,∞] which is depicted in Figure 2.

Theorem 3. The time complexity for dominance detection on a pair of search states is O(w(d|X| + a|C|)), where w is the width of part (2), d is the maximum number of possible daton at any time point, and a is the maximum arity of stream constraints.

Proof. (Sketch) The starting point of part (2) for an St-CSP P is t(P). To check domain equivalence, we can consider only part (2) of the time line since there is no difference for part (3). This takes time O(wd|X |). We then check constraint equivalence. Every constraint can involve only a finite number of fby operators. By Property 1, after a finite number of time points, all the daton constraints share the same structure. As the constraint may involve a finite number of daton variables before time point t(Pj) or t(Pi), we have to check the equivalence of the values which are assigned to those daton variables. This checking takes O(wa|C|).

The sufficient condition (Theorem 2) depends on the number of datons, width of part (2), and the number of variables. As all are finite, there must be two search states in each branch matching the condition for dominance detection.

Lemma 3. Each branch in a search tree is finite and must either (a) end in failure or (b) contain search states Pi and Pj such that Pi ≺ Pj and the branch terminates at Pi.

Proof. The search procedure branches for each possible daton for a selected variable at a time point. Since the daton domain is finite, there is a finite number of branches. The branch ends in failure once there is no consistent daton to be assigned; otherwise, the branch continues. At every advancement of time point, the search performs dominance detection.

As there are finite possible datons and finite number of stream constraints in the problems, there must be two search states along a branch of the search tree that satisfy the dominance relation.

Theorem 4. The search procedure terminates.

Proof. The theorem follows directly from Lemma 3.

Among the first seven search states shown in Figure 1, the search states P4 and P5 are dominated by P2. In search state P6, the assignment X(1) = 2 cannot satisfy the constraint X = first Y and the search fails.

4.2 Construction of Solution Set

When solving solutions of St-CSP P through the search procedure, we are actually building the corresponding B¨uchi automaton A, which can recognize and thus also generate the solution set. We want L(A) = L(sol(P)).

The automaton A = (Q, q0, △, F ) is built according to the search tree. For each search state Pi ∈ Φ, Pi is associated to a state state(Pi) in A, thus Q = {state(Pi) | Pi ∈ Φ}. The root node of the search tree, P0, is associated with the starting state of A where q0 = state(P0). For every non-root search state Pi ∈ Φ\{P0}, there is an edge pointing from state(Pj) to state(Pi) where Pj is the nearest ancestor of Pi in Φ. The edge is labelled with the assignment tuple made from the search state Pj to Pi. For each leaf node Pi associated with state state(Pi), if Pi ≺ Pj, there is an edge pointing from state(Pi) to state(Pj) labelled with an empty string ϵ. Since the automaton is generated from the search tree, all the possible runs correspond to solutions. The set of final states contains all the states in the automaton, thus F = Q. The final automaton can be simplified. When a path in search tree leads to failure, there are some states in A cannot be included in any accepting runs. These states can be removed. When Pi ≺ Pj , state(Pi) can be merged with state(Pj) such that the edge labelled with ϵ can be eliminated.

Figure 3 shows the subset of solutions corresponding to the first seven search states in Figure 1. The associated search states are labelled on the states in the automaton. From the automaton, the subset of solutions is (1, 1)((1, 1) | (1, 2))ω .

The solution automaton A corresponds to the structure of search tree, where every search state Pi ∈ Φ is a state and every complete daton assignment is an edge.

Theorem 5. The solution automaton takes O(wa|C| + d|X| ) space, where w is the width of part (2), a is the maximum arity of constraint, and d is the maximum number of possible datons at any time point.

P = ({X, Y }, {D(X) = D(Y ) = (1 | 2)ω }, {C : X = first Y })

Proof. Each advancement of current time point in the search corresponds to a state in the automata. The number of nodes Pi, where Pi ∈ Φ along the search path, is O(wa|C|), which is the number of different patterns in part (2). Each state contributes at most d|X| edges for every possible daton assignment.

The following theorem shows that the constructed automaton recognizes all solutions and only solutions of P.

Theorem 6. (Soundness and Completeness) Given a B¨uchi automaton A constructed from the search procedure for an St-CSP P, (α1, α2, . . . , αn) ∈ sol(P) ↔ α1 ⊗ α2 ⊗ . . . ⊗ αn ∈ L(A).

5 Consistency Algorithm

Enforcing consistency helps reduce search space, by identifying and avoiding infeasible search branches. In St-CSP, due to the infinite domain size, it is expensive to enforce generalized arc consistency (GAC) [Bessi`ere and R´egin, 1997]. According to the search strategy introduced in the previous section, we define a weaker notion of consistency, namely prefix-k consistency, which enforces GAC on the daton variables in a size k window of time points.

In the search tree, the current time point t(P) of a search state P contains the first unbound daton variable. We limit our attention to the width k window of time points starting from t(P), which is R = [t(P), t(P)+k-1]. Among the daton variables in this window of time points, we enforce GAC.

By the definition of GAC [Bessi`ere and R´egin, 1997], a daton variable Xv(i) in an St-CSP P is GAC with respect to daton constraint C(j) if and only if D(Xv(i)) = (∏Xu(m)∈scope(C(j)) D(Xu(m)) ∩ C(j)) ↓Xv(i) where ↓Xv(i) projects the tuples to Xv(i).

A stream variable X is prefix-k consistent with respect to a stream constraint C if and only if ∀i ∈ R, X(i) is GAC with respect to all the daton constraint C(j) ∈ C such that X(i) ∈ scope(C(j)). An St-CSP P is prefix-k consistent if and only if all the stream variables in P are prefix-k consistent with respect to all C ∈ C.

For example, in Figure 1, the search state P1 is not prefix1 consistent with respect to the constraint because there are no datons d ∈ D(X(0)) such that X(0) = Y (0) when Y (0) = 2. Figure 4 shows the search tree of the problem with prefix-1 consistency enforced. After the assignment X(0) = 1 from search state P0, prefix-1 consistency is enforced at time point 0 and removes 2 from D(Y (0)). As both X(0) and Y (0) are bound, the search advances the current time point and enforces prefix-1 consistency at time point 1, which gives the search state P1. We can see that the search tree becomes smaller and some nodes leading to failure, such as P6 in Figure 1, are pruned earlier.

The notion of prefix-k consistency is enforced on the daton variables and daton constraints. The enforcement algorithm in Algorithm 1 is based on the classical GAC enforcement, but we are only interested in the daton variables X(i) whose time point i falls in R. In the procedure PrefixK, only daton variables with time points in the width R will be considered. The Revise procedure checks if each of the values in the daton variable domain can be extended to a tuple which is consistent to the daton constraint. When there are changes made to the domain, all the constraints with variables inside the range of time points will be enqueued.

1 Procedure Revise(P, xi, c) 2 //xi and c are daton variable and daton constraint respectively. 3 change := false; 4 for dj ∈ D(xi) do 5 support := false; 6 for (d0, d1, . . . , dj , . . . , dn) ∈ D(x0) × D(x1) × . . . × {dj} × . . . × D(xn) do 7 if (d0, d1, . . . , dj, . . . , dn) ∈ c then 8 support := true; 9 if support = false then 10 D(xi) := D(xi) \ {dj}; 11 change := true; 12 return change; 13 Procedure PrefixK(P, k) 14 R := [t(P), t(P) + k - 1]; 15 Q := {(Xm(i), Cn(j)) | Xm(i) ∈ scope(Cn(j)) ∧ i ∈ R }; 16 while Q ̸= ∅ do 17 take and remove (Xm(i), Cn(j)) from Q; 18 if Revise(P, Xm(i), Cn(j)) then 19 for Cn′ (j ′ ) ∈ C s.t. Xm(i) ∈ scope(Cn′ (j ′ )) do 20 for Xm′ (i′ ) ∈ Cn′ (j ′ ) do 21 if Xm′ (i′ ) ̸= Xm(i) ∧ i′ ∈ R then 22 Q := Q ∪ (Xm′ (i′ ), Cn′ (j ′ ));

Theorem 7. (Correctness) If St-CSP P ′ is obtained from P by applying Algorithm 1, then P ′ is equivalent to P and P ′ is prefix-k consistent.

Proof. Given i ∈ R. Suppose ∃d ∈ D(X(i)) such that ∃C(j),X(i) ∈ scope(C(j)), d /∈ C(j) ↓X(i) and d remains in D(X(i)) after executing Algorithm 1. In line 18 of the algorithm, C(j) will be selected. In procedure Revise, the condition in line 7 will never be satisfied. Thus d is removed from the domain of D(X(i)) and this contradicts the assumption.

Theorem 8. The algorithm to enforce prefix-k consistency takes O(adak|C|) time, where a is the maximum arity of daton constraints, and d is the maximum possible datons at any time point.

Proof. The complexity of Revise isO(da ) to check for support for each of the possible daton in the daton domain. The procedure PrefixK enforces prefix-k consistency. There are O(ak|C|) tuples in the queue Q, each of them will be put into queue again for at most O(da ) time.

6 Examples and Experiments

To verify the feasibility of our framework, we have modelled the periodic still life problem, traffic light scheduling, 15puzzle, simulation of juggling, and jazzy harmony generation as St-CSPs. The periodic still life problem looks for initial patterns that lead to oscillating patterns after a finite number of steps. The traffic light scheduling problem arranges traffic light signals in a road junction such that the vehicles will never crash. Though optimal solutions to a valid 15puzzle always involves finite number of moves, the problem looks for all possible solutions so that the number of moves is not known in advance. Due to space limitation, we describe only the juggling problem and harmony generation in details. These problems have non-UP-stream solutions. We implement a prototype St-CSP solver enforcing prefix-k consistency. Comparison among different k values is conducted. The solution automata are constructed automatically on-thefly during search and translation time is included in our results. Experiments are conducted on a Sun Blade 2500 machine with 2GB memory.

6.1 Simulation of Juggling

The task is to simulate basic juggling [Apt and Brand, 2006] involving n balls. For simplicity, the patterns ensure that there is at most one ball in hand at any time, and every ball is thrown for maximum m time points after which the ball is caught. Each problem is characterized by (n,m). We aim to find all possible sequences of juggling patterns which may change over time.

The n variables X1,X2,X3, . . . ,Xn represent the time interval after which the ball is caught. For example, if X1 has daton 5 at time point 3, ball 1 will be in the air for 5 time points and be caught at time point 7. The variable A indicates the force to throw the ball, which reflects the time interval for the ball in the air. A ball thrown with odd (even) units of force will be caught by different (same) hand. The domain of the variables are: ∀1 ≤ i ≤ n, D(Xi) = (1|2|3| . . . |m)ω and D(A) = (0|1|2| . . . |m)ω . The variable A has daton 0 at the time when no ball is at hand.

A ball falls down by 1 unit at a time, unless it is being thrown with force A again. The constraints are: ∀1 ≤ i ≤ n, (Xi == 1) → (next Xi == A) and (Xi ̸= 1) → (next Xi = Xi - 1). Also, no two balls are being caught simultaneously: ∀1 ≤ i < j ≤ n, Xi ̸= Xj .

One solution of instance (3, 5): X1 = (3, 2, 1, 4)ω ,X2 = (2, 1, 4, 3)ω , X3 = (1, 3, 2, 1)ω , A = (3, 4, 4, 1)ω which is a UP solution, is shown in Figure 5 by a space-time diagram. The automaton in Figure 6 recognizes a subset of solutions to the problem. The solution can be obtained in a run starts at state 0 and followed by sequence of states 1, 2, 3, 4 repeatedly. Other solutions can also be obtained by transversing different edges, including non-UP solutions, such as: X1 = 〈3, 2, 1, 3, 2, 1, 4, 3 . . .〉,X2 = 〈2, 1, 3, 1, 4, 3, 2 . . .〉,X3 = 〈1, 3, 2, 3, 2, 1, 1 . . .〉, A = 〈3, 3, 3, 4, 4, 1, 4 . . .〉 which is the run of states 0, 1, 5, 0, 1, 2, 3, 4, . . ..

We conduct experiments on instances of (n,m) with prefix-k consistency where k ∈ {1, 2, 3} and the results are listed in Table 2. When n = m, there are only repetitive juggling patterns as solutions. After enforcing consistency, the solutions can be easily obtained and thus the number of fails is small in those cases. When k is larger, the consistencies become stronger and thus more infeasible search space is pruned. As the time complexity of prefix-k consistency increases with k, the overall runtime cannot be compensated by the extra pruning when k is large.

In the problem, all constraints relate daton variables across only two time points, e.g. Xi(t) and Xi(t + 1) in the constraint (Xi == 1) → (next Xi == A). We conjecture that the optimal solving performance is obtained when k is chosen as the maximum difference of time points of all constraints involving the "next" and "fby" operators. The long solving time for instances (3, 4) and (6, 6) is due to the enumeration of many solutions and large problem size respectively.

6.2 Towards Generating Jazzy Harmonization

This problem is to generate the harmonization of four-part choral music. A choral music contains soprano, alto, tenor, and bass. Given the soprano notes which are repeated indefinitely, we have to determine the notes for alto, tenor, and bass so that the music is pleasant to listen for human beings.

We use variables X1,X2,X3,X4 to represent the sequences of notes for soprano, alto, tenor, and bass respectively. A music note is encoded as a number. For example, 60 is middle C (C4). We limit the range of notes to two octaves from 48 (C3) to 72 (C5). The domains are D(X1) = D(X2) = D(X3) = D(X4) = (48 | . . . | 72)ω . Auxiliary variables help in modeling. For example, we have a set of pseudo-Boolean variables indicating the notes of each part, such as CInX1 , CsharpInX1 , and DInX1 which represent whether X1 takes the note C, C♯, and D respectively.

In this problem, we use the first four bars of the melody from "Twinkle Twinkle Little Star" (CCGGAAG, FFEEDDC) as a sentence and repeat it indefinitely: melody = (60, 60, 67, 67, 69, 69, 67, 65, 65, 64, 64, 62, 62, 60)ω . The end of the sentence is indicated by a pseudo-Boolean stream: end = (0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1)ω .

We implement a number of rules for harmonization [Tsang and Aitken, 1991]. For example, the parallel fifth rule is specified as ∀i < j, Xi -Xj == 7 → next(Xi -Xj) <> 7. The rule requiring that voices should never cross each other is expressed by ∀2 ≤ i ≤ 4, Xi > Xi-1.

The auxiliary variables can be constrained by CInXi = (Xi/12 == 0), CsharpInXi = (Xi/12 == 1), DInXi = (Xi/12 == 2), etc. The existence of a note in a chord can be defined in terms of these auxiliary variables: existC = CInX1 or CInX2 or CInX3 or CInX4 . Then, each of the seven chord types can be given by constraints, e.g., chordI = (existC and existE and existG) for Chord I. Now, we can require that each chord must be one of the seven standard types: chordI + . . . + chordVII = 1

By changing pitch, tempo, and delay of harmony, we can introduce jazzy feeling to the music.

When we decide to change the pitch of the song up to five intervals, we have to change it for every note in a sentence. Therefore, D(offset) = (-5 | . . . | 5)ω and not end → (next offset = offset ) and thus X1 = melody + offset .

The change of tempo is also applied to a sentence for up to three times slower. D(tempo) = (1 | 2 | 3)ω which represents the multiples of tempo of the original note: not end → (next tempo = tempo).

The last feature is delay of harmony. When this style is applied to a chord, the harmony will be silent in the first half of the time. However, this style cannot be applied frequently to maintain pleasant feeling. Among any three consecutive chords, at most one chord can apply this style. Moreover, by the convention of music composition, the last note of each melody should keep long, and thus the style cannot be applied to the last note. We use a pseudo-Boolean variable delay to indicate the application of this style with initial domain (0 | 1)ω . The style is implied by imposing the following constraints: delay + next delay + next next delay ≤ 1 and end → not delay .

With the remaining constraints, we generate harmony for a given soprano which contains a repeated melody. The harmony can vary as the soprano repeats over time based on the solution automaton, which can serve as a basis for musical improvisation. Sample MIDI files generated from our solver can be downloaded online 1 .

7 Concluding Remarks

Streams are related to coinduction [Rutten, 2005]. Fages and Rizk [2009] specify the problem using a formula in LTL which is the first approach to softness and optimization by quantifying the satisfaction degree of the formula. Pralet and Verfaillie [2008] use different techniques to solve problems in which variables have temporal dimension. Work on classical temporal constraints are too numerous to be mentioned [Dechter, 2003]. Our work also has some loose connections with online constraint solving [Verfaillie and Jussien, 2005]. The work by Gavanelli et al. [2005] is related but different from ours. It is the variable domains that are changing with possible values coming in incrementally, but variables still take just a scalar value from the evolving but always finite variable domains. In our case, each variable takes an infinite data stream as value from a possibly infinite variable domain of streams. Planning problems have been solved by constraint programming [van Beek and Chen, 1999]. While the number of steps is not known prior to solving, the problem is modelled for a fixed number of steps. The problem is re-modelled with increased number of steps until there is a solution found.

We consider data streams as a new domain for constrained variables. The constraint language allows us to use any classical constraint interpreted pointwisely and temporal operators inspired by the data-flow language Lucid [Wadge and Ashcroft, 1985]. The modelling examples show that the St-CSP framework makes it possible to give a declarative statement, such as the juggling specification, of the problem, which separates problem formulation and solution methods. This brings us one step towards the Holy Grail of programming [Freuder, 1997]: the user states the problem, the computer solves it. We have implemented a prototype solver for the framework to find all solutions. By using B¨uchi automata, the solver can give solutions including non-UP ones.

Optimization in St-CSP is an important future direction. For example, in musical generation, some rules can be more preferable to others. The framework opens a new direction of research. We have described the application to simulate the juggling and generate music harmonization in this paper. Other real life applications, such as controller synthesis, are worth for exploration. Interaction with live data streams is another possible venue for future work. Studying the effect of variable and value orderings is also worthwhile. Enhancement on the search strategies, such as applying more accurate heuristics for dominance detection, and introducing new consistency notions to the St-CSP, can improve the search performance. Improvement to the prototype solver in terms of implementation techniques and the use of data structures is also imminent.

1 http://www.cse.cuhk.edu.hk/˜jlee/stcsp.mid

Acknowledgments

We thank the anonymous referees for constructive comments and Jasper Lee for the advice on music harmonization. The work described in this paper was substantially supported by grants (CUHK413808 and CUHK413710) from the Research Grants Council of Hong Kong SAR.