Let Y = {Xp1**, . . . , X**pk
} be a maximum cardinality subset of variables of X whose ranges are pairwise disjoint (i.e., range(Xpi) ∩ range(Xpj) = ∅, ∀i, j ∈ 1**..k, i** 6= j). Let IY = {[bi, ci] | bi = min(Xpi), ci = max(Xpi), Xpi ∈ Y } be the corresponding ordered set of disjoint ranges of the variables in Y . It has been shown in [9] that |Y | =
card↓(X).

Consider the interval [bi, ci] ∈ IY . Constraints (5) ensure that the variables Mbici i = [1**, . . . , k**] are greater than or equal to 1 and constraints (6) ensure that the variable M1d is greater than or equal to the sum of lower bounds of variables Mbici
,
i = [1**, . . . , k**], because intervals [bi, ci] are disjoint. Therefore, the variable N is greater than or equal to **card**↓(X) and it is bound consistent.

We show that when N is BC and dom(N) 6= {**card**↓(X)}, all X variables are BC.

Take any assignment S ∈ ΠXi∈X**range**(Xi) such that card(S) = **card**↓(X). Let S[Xi ← b] be the assignment S where the value of Xiin S has been replaced by b, one of the bounds of Xi. We know that card(S[Xi ← b]) ∈ [card(S) − 1, card(S**) + 1] =**
[card↓(X) − 1, card↓(X**) + 1]** because only one variable has been flipped. Hence, any assignment (**S, p**) with p ≥ card↓(X**) + 1** is a bound support. dom(N) necessarily contains such a value p by assumption.

The only case when pruning might occur is if the variable N is ground and card↓(X) = N. Constraints (6) imply that M1d equals the sum of variables M1,b1−1 +
Mb1,c1 +Mc1+1,b2−1 **. . .**+MbN,cN +McN+1,d. The lower bound of the variable Mci,bi is greater than one and there are |Y | = card↓(X) = N of these intervals. Therefore, by constraint (7), the upper bound of variables Mci−1+1,bi−1 that correspond to intervals outside the set IY are forced to zero.

There are O(nd2) constraints (4) and constraints (5) that can be woken O(d) times down the branch of the search tree. Each requires O(1) time for a total of O(nd3) down the branch. There are O(d 2) constraints (6) which can be woken O(n) times down the branch and each invocation takes O(1) time. This gives a total of O(nd2). The final complexity down the branch of the search tree is therefore O(nd3). ✷
The proof of theorem 3 also provides the corollary that enforcing range on consistency on constraints 4 enforces range consistency on ATMOSTNVALUE. Note that theorem 3 shows that the BC propagator of ATMOSTNVALUE [12] is not algorithmically global with respect to time, as BC can be achieved with a decomposition with comparable time complexity. On the other hand, the O(nd2) space complexity of this decomposition suggests that it is algorithmically global with respect to space. Of course, we only provide upper bounds here, so it may be that ATMOSTNVALUE is not algorithmically global with respect to either time or space.

## 5 Faster Decompositions

We can improve how the solver handles this decomposition of the ATMOSTNVALUE constraint by adding implied constraints and by implementing specialized propagators. Our first improvement is to add an implied constraint and enforce BC on it:

$$M_{1d}=\sum_{i=1}^{d}M_{i i}$$
Mii (8)