gives bound consistent domains for the original NVALUE *constraint:*

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

To show that decomposing the NVALUE constraint into these two parts does not hinder propagation in general, we will use the following lemma. Given an assignment S of values, **card**(S) denotes the number of distinct values in S. Given a vector of variables X = X1 . . . Xn, card↑(X) = max{card(S) | S ∈ ΠXi∈X**range**(Xi)} and card↓(X) = min{card(S) | S ∈ ΠXi∈X**range**(Xi)}.

Lemma 1 (adapted from [5]) *Consider* NVALUE([X1, . . . , Xn], N)*. If* D(N) ⊆
[card↓(X)**, card**↑(X)], then N *is BC.*
Proof: Let Smin be an assignment of X in ΠXi∈X**range**(Xi) with card(Smin) =
card↓(X) and Smax be an assignment of X in ΠXi∈X**range**(Xi) with card(Smax) =
card↑(X). Consider the sequence Smin = S0, S1, . . . , Sn = Smax where Sk+1 is the same as Sk except that Xk+1 has been assigned its value in Smax instead of its value in Smin. |card(Sk+1)− card(Sk)| ≤ 1 because they only differ on Xk+1. Hence, for any p ∈ [card↓(X)**, card**↑(X)], there exists k ∈ 1..n with card(Sk) = p. Thus, (Sk, p) is a bound support for p on NVALUE([X1, . . . , Xn], N). Therefore, min(N) and max(N)
have a bound support. ✷
We now prove that decomposing the NVALUE constraint into ATMOSTNVALUE
and ATLEASTNVALUE constraints does not hinder pruning when enforcing BC.

Theorem 2 *BC on* NVALUE([X1, . . . , Xn], N) *is equivalent to BC on* ATMOSTNVALUE([X1, . . . , Xn], N) *and on* ATLEASTNVALUE([X1, . . . , Xn], N).

Proof: Suppose the ATMOSTNVALUE and ATLEASTNVALUE constraints are BC.

The ATMOSTNVALUE constraint guarantees that card↓(X) ≤ min(N) and the ATLEASTNVALUE constraint guarantees that card↑(X) ≥ max(N). Therefore, D(N) ∈ [card↓(X)**, card**↑(X)]. By Lemma 1, the variable N is bound consistent.

Consider a variable/bound value pair Xi = b. Let (S
b least, p1) be a bound support of Xi = b in the ATLEASTNVALUE constraint and (S
b most, p2) be a bound support of Xi = b in the ATMOSTNVALUE constraint. We have **card**(S
b least ) ≥ p1 and **card**(S
b most) ≤ p2 by definition of ATLEASTNVALUE and ATMOSTNVALUE.

Consider the sequence S
b least = S
b 0
, Sb 1
, . . . , Sbn = S
b most where S
b k+1 is the same as S
b k except that Xk+1 has been assigned its value in S
b most instead of its value in S
b least. |**card**(S
b k+1) − **card**(S
b k
)| ≤ 1 because they only differ on Xk+1. Hence, there exists k ∈ 1..n with min(p1, p2) ≤ **card**(S
b k
) ≤ max(p1, p2). We know that p1 and p2 belong to **range**(N) because they belong to bound supports. Thus, card(S
b k
) ∈ **range**(N) and (S
b k
, card(S
b k
)) is a bound support for Xi = b on NVALUE([X1, . . . , Xn], N). ✷
When enforcing domain consistency, Bessiere *et al.* [5] noted that decomposing the NVALUE constraint into ATMOSTNVALUE and ATLEASTNVALUE constraints does