

![0_image_0.png](0_image_0.png)

Note that the length of the interval [b, max(Xj ) + 1) equals the sum of Bi1,max(Xj )
and Db,max(Xj ) due to the invariant. This means that the interval [b, max(Xj ) + 1)
violates conditions (5)–(7), as the sum Bi1,max(Xj ) + Db,max(Xj ) has to be less than or equal to the length of the interval [b, max(Xj ) + 1) minus 1.

Soundness. Suppose we pruned an interval [b − 1, max(Xj )] from D(Xi) after the processing of the variable Xj . This pruning is sound because the interval [b, max(Xj )+
1) violates conditions (5)–(7).

Completeness. Suppose there exists an interval [*l, u*] that violates conditions (5)–
(7), so that Bi1,u + Di l,u > u − l. However, the algorithm does not prune the upper bound of Xito l − 1. Suppose that l ∈ L, u ∈ U. As the pointer b preserves the invariant, there are exactly Bi1,u available values between [*l, u* + 1). Hence b points to l and max(Xi) ≤ l − 1.

Suppose that l /∈ L, u ∈ U. We consider the step when the last pruning of the variable Xi occurs. Suppose we processed the variable Xj at this step. The pointer b stores max(Xi) + 1. As b does not move backward in the following steps, we conclude that neither successors nor non-successors with domains that are contained inside the interval [*b, d*] occur. Hence, Bi1,u + Di l,u = Bi1,u + Dimax(Xi)+1,u
, max(Xj ) ≤ u, u ∈ U, l < max(Xi). Hence [*l, u*] is not a violated interval.

Complexity. At each iteration of the loop (line 2) the pointer b moves O(d)
times forward and O(n) times backward. Due to a disjoint set data structure the total cost of the operations is O(d), the functions Union(v1, v2, T) and F ind(v1, T) take O(1) [22]. The total time complexity is O(nd). ut We can construct a similar algorithm to Algorithm 1 to enforce conditions (8)–(10)
and prune lower bounds.

Example 4 *Consider* ALLDIFFPREC([X1, X2, X3, X4, X5], {(1, 2),(1, 3)}) for Example 3. We show how our algorithm works on this example.

We represent values in the disjoint set data structure T with circles. We use rectangles to denote sets of joint values. Initially, all values are in disjoint sets. If a variable