= Solution
\b[Always true.] Replace every <all-different constraint> by the pairwise inequalities on its scope. Then solutions are precisely the <proper graph colourings> of the <primal graph> using values from $D$ as colours. Put $t=\operatorname{tw}(P)$.
A <graph> of <treewidth> $t$ has a <proper graph colouring> with at most $t+1$ colours. Here is a constructive proof. In a width-$t$ <tree decomposition>, remove any leaf bag contained in its neighbor. If more than one bag remains, a leaf bag has a <vertex> absent from its neighbor. The running-intersection property means that <vertex> occurs only in the leaf bag, so every neighbor of the <vertex> belongs to that bag. It has at most $t$ neighbors. If only one bag remains, it has at most $t+1$ <vertices> and the same degree bound holds.
Remove the chosen <vertex> and repeat; deleting <vertices> cannot increase the width of the restricted <tree decomposition>. Now colour in reverse removal order. At most $t$ already coloured neighbors forbid colours, so one of $t+1$ colours is always available. Since the <integer> inequality $|D|>t$ gives $|D|\ge t+1$, this produces a satisfying assignment:
$$
\boxed{|D|>\operatorname{tw}(P)\ \Longrightarrow\ \operatorname{Sol}(P)\ne\varnothing.}
$$
The common unrestricted <constraint domain> and the exclusively <all-different constraints> are essential: arbitrary constraint relations do not reduce to <graph colouring> in this way.
Back to article page
