1 2 3 4 5 X1 ∗ ∗ X2 ∗ ∗ ∗ Y1 ∗ ∗ ∗ Y2 ∗ ∗ If we have Oi ∈ [0, 1] for 1 ≤ i ≤ 5 then both EGCC([X1, X2], [O1, O2, O3, O4, O5]) and EGCC([Y1, Y2], [O1, O2, O3, O4, O5]) are BC. However, enforcing BC on the decomposition of
SAME([X1, X2], [Y1, Y2]) removes 3 *from the domain*
of X2 and Y1.
In fact, we conjecture that enforcing BC on this decomposition achieves BC on the SAME constraint itself. Similar
decompositions can be given for other global constraints like
NVALUE and COMMON.

## 6 Experimental Results

To test these decompositions, we ran experiments on pseudo-Boolean encodings (PB) of CSPs containing ALL-DIFFERENT and PERMUTATION constraints. We used the MiniSat+ 1.13 solver on an Intel Xeon 4 CPU, 2.0 Ghz, 4G RAM with a timeout of 600 seconds for each experiment.

Our decompositions contain two types of constraints: SUM constraints like (2) and MEMBER constraints like (1). The SUM constraints is posted directly to the MiniSat+ solver.

To encode MEMBER constraints, we use literals Bij for the truth of Xi ≤ j [Ohrimenko *et al.*, 2007], and clauses of the form (Ailu = 1) ⇔ (Bi(l−1) = 0 ∧ Biu = 1). This achieves bound consistency (Theorem 2). To increase propagation, we use a direct encoding with literals Zij for the truth of Xi = j and clauses (Ailu = 0) ⇒ (Zij = 0), j ∈ [l, u]. The overall consistency achieved is therefore between BC and RC. We denote this encoding HI. To explore the impact of small Hall intervals, we also tried HIk, a PB encoding with only those constraints (2) for which u − l + 1 ≤ k. This detects Hall intervals of size at most k. Finally, we decomposed ALL-DIFFERENT into a clique of binary inequalities, and used a direct encoding to convert this into SAT (denoted BI).

Pigeon Hole Problems. Table 1 gives results on pigeon hole problems (PHP) with n pigeons and n − 1 holes. Our decomposition is both faster and gives a smaller search tree compared to the BI decomposition. On such problems, detecting large Hall intervals is essential.

Double-Wheel Graceful Graphs. The second set of experiments uses double-wheel graceful graphs [Petrie and Smith, 2003]. We converted the CSP model in [Petrie and Smith, 2003] into a PB formula. This model has an ALL-DIFFERENT constraint on node labels and a PERMUTATION constraint on edge labels. For the PERMUTATION constraint we use (5). We strengthen the BI decomposition with clauses to ensure that every value appears at least once. Table 2 show that our decomposition outperforms the augmented BI decomposition on many instances. Whilst detecting large Hall intervals can greatly

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

Table 1: PHP problems. t is time and bt is the number of backtracks to solve the problem.

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

reduce search, in some cases the branching heuristics appear to be fooled by the extra variables introduced in the encodings.

Overall these experiments suggest that detecting Hall intervals reduces search significantly, and focusing on small Hall intervals may be best except on problems where large Hall intervals occur frequently.

## 7 Other Related Work

The ALL-DIFFERENT constraint first appeared in the ALICE constraint programming language [Lauriere, 1978]. Regin proposed a DC propagator that runs in O(n 2.5) time
[R´egin, 1994]. Leconte gave a RC propagator based on Hall intervals that runs in O(n 2) time [Leconte, 1996]. Puget then developed a BC propagator also based on Hall intervals that runs in O(n log(n)) time [Puget, 1998]. This was later improved by Melhorn and Thiel [Mehlhorn and Thiel, 2000] and then Lopez-Ortiz *et al.* [Lopez-Ortiz *et al.*, 2003].

The global cardinality constraint, GCC was introduced in the CHARME language [Oplobedu *et al.*, 1989]. Regin proposed a DC propagator based on network flow that runs in O(n 2) time [R´egin, 1996]. Katriel and Thiel proposed a BC propagator for the EGCC constraint [Katriel and Thiel, 2003]. Quimper *et al.* proved that enforcing DC on the EGCC constraint is NP-hard
[Quimper *et al.*, 2004]. They also improved the time complexity to enforce DC and gave the first propagator for enforcing RC on GCC.

Many decompositions have been given for a wide range of global constraint. However, decomposition in general tends to hinder propagation. For instance,
[Stergiou and Walsh, 1999] shows that the decomposition of ALL-DIFFERENT constraints into binary inequalities hinders