ple superscripts, in the following, we will assume dom(v) =
[1, d] for all v ∈ V .

Direct Encoding A straightforward encoding is the direct
encoding in which an atom e(**v, i**) is introduced for each constraint variable v and each value i from their domain, representing v = i. Intuitively, e(**v, i**) is in an answer set if v takes
the value i, and it is not if v takes a value different from i. For
each v, possible assignments are encoded by a choice rule (1). Furthermore, we specify that v takes at least one value (2) and that it takes at most one value (3).
$$\{e(v,1),\ldots,e(v,d)\}\gets\tag{1}$$ $$\perp\gets not\ e(v,1),\ldots,not\ e(v,d)$$ (2) $$\perp\gets2\ \{e(v,1),\ldots,e(v,d)\}\tag{3}$$  constraint $c$ is encoded as forbidden combination of values.  
A constraint c is encoded as forbidden combination of values,
i.e., if v1 = d1, v2 = d2, **. . .** , vn = dn is such a forbidden
combination then we encode
violate(c) ← e(v1, d1), e(v2, d2), . . . , e(vn, dn).
Unfortunately, the direct encoding hinders propagation:
Theorem 1 *Enforcing arc consistency on the binary decomposition of a constraint prunes more values from the variables*
domain than unit-propagation on its direct encoding.
The support encoding has been proposed in the domain of
SAT to tackle this weakness [Gent, 2002].

Support Encoding We now encode support information for assignments rather than the encoding of conflicts. For each possible assignment to a variable one of its supports must hold, that is, the set of values for the other variable which allow this assignment. Formally, a *support* for a constraint variable v to take the value i across a constraint c is the set of values {i1, . . . , im} ⊆ dom(v
′
) of another variable in v
′ ∈ **scope**(c)\{v} which allow v = i, and can be encoded in the following rule, based on (1–3):
violate(c) ← e(v, i)**, not e**(v
′
, i1)**, . . . , not e**(v
′
, im).

It can be read as whenever v = i, then at least one of its supports must hold, otherwise the constraint is violated. In the support encoding, for each constraint c there is one support for each pair of distinct variables v, v′ ∈ **scope**(c), and for each value i.

Theorem 2 *Unit-propagation on the support encoding enforces arc consistency on the binary decomposition of the* original constraint.

We have used program transformation [Simons *et al.*, 2002]
in [Drescher and Walsh, 2010] to reformulate ALL-DIFFERENT straightforwardly according to our support encoding into O(d) cardinality rules:
violate(c) ← 2 {e(v1, i), . . . , e(vn, i)} (4)
Corollary 1 *Unit-propagation on (1–4) enforces arc consistency on the binary decomposition of* ALL-DIFFERENT in O(nd2) *down any branch of the search tree.*
Range Encoding In the *range encoding*, we represent that a variable can take values from an interval v ∈ [**l, u**], i.e.,
a value between l and u (inclusive). An atom r(**v, l, u**) is introduced for each v and [l, u] ⊆ [1, d]. For each range [**l, u**],
the following O(nd2) rules encode v ∈ [**l, u**] whenever v 6∈
[1, l − 1] and v 6∈ [u + 1, d], and enforce a consistent set of ranges, i.e., v ∈ [**l, u**] implies v ∈ [l −1, u] and v ∈ [**l, u**+ 1]:
r(v, l, u) ← not r(v, 1, l − 1), not r(**v, u** + 1, d) (5)
⊥ ← r(v, l − 1, u), not r(**v, l, u**) (6)
⊥ ← r(**v, l, u** + 1), not r(**v, l, u**) (7)
Constraints are encoded into integrity constraints representing conflict regions v1 ∈ [l1, u1], . . . , vn ∈ [ln, un]:
violate(c) ← r(v1, l1, u1), . . . , r(vn, ln, un)
Theorem 3 *Unit-propagation on the range encoding enforces range consistency on the original constraint.*
An efficient propagator for ALL-DIFFERENT enforces range consistency by pruning Hall intervals [Leconte, 1996]. A
Hall interval of size k completely contains the domains of k variables, formally, |{v | dom(v) ⊆ [**l, u**]}| = u−l+1. Observe that in any bound support, the variables whose domains are contained in the Hall interval consume all values within the Hall interval, whilst any other variable must find their support outside the Hall interval (cf. [Bessi`ere *et al.*, 2009a]).

We encode ALL-DIFFERENT such that no interval [**l, u**] can contain more variables than its size:
violate(c) ← u − l + 2 {r(v1, l, u), . . . , r(vn**, l, u**)}. (8)
This simple reformulation can simulate a complex propagation algorithm like the one in [Leconte, 1996] with a similar overall complexity.

Corollary 2 *Unit-propagation on (5–8) enforces range consistency on* ALL-DIFFERENT in O(nd3) down any branch of the search tree.

Bound Encoding In our *bound encoding*, similar to the *order encoding* [Tamura *et al.*, 2006], an atom b(**v, i**) is introduced for each variable v and value i to represent that v is
bounded by i, i.e., v ≤ i. For each v, possible assignments
are encoded by a choice rule (9). To ensure a consistent set of
bounds, (10) encodes that v ≤ i implies v ≤ i + 1. Finally, (11) encodes v ≤ d, i.e., some value must be assigned to v.
$$\{b(v,1),\ldots,b(v,d)\}\gets\tag{9}$$ $$\perp\gets b(v,i),not\ b(v,i+1)$$ (10) $$\perp\gets not\ b(v,d)\tag{11}$$  Similar to the range encoding, we represent conflict regions
l1 < v1 ≤ u1, . . . , ln < vn ≤ un as below
violate(c) ← b(v1, u1), . . . , b(vn, un),
not b(v1, l1), . . . , not b(vn, ln).
$\mathbf{a}\cdot\mathbf{b}=\mathbf{a}\cdot\mathbf{b}$. 
Theorem 4 *Unit-propagation on the bound encoding enforces bound consistency on the original constraint.*
In order to achieve a reformulation of ALL-DIFFERENT that can only prune bounds, the bound encoding for variables is