= Solution
\b[Always true for a nonempty finite <constraint domain>, as conventionally assumed.] Write $q=|D|$ and identify its values with $\{0,\ldots,q-1\}$. For each satisfying assignment $(x_1,\ldots,x_n)$, simultaneously replace every value by
$$
x_i\longmapsto x_i+a\pmod q,\qquad a\in\{0,\ldots,q-1\}.
$$
This <permutation> of the common <constraint domain> preserves every equality and inequality, hence every <all-different constraint>. The resulting $q$ assignments are distinct: equality of even one coordinate before and after a shift forces $a=0\pmod q$. There is at least one <variable>, since $m>0$ and $k\ge2$.
The <cyclic group> of shifts therefore partitions the solution <set> into disjoint <orbits> of size $q$. It follows that
$$
\boxed{q\mid\#\operatorname{Sol}(P).}
$$
The conclusion includes an unsatisfiable instance, whose solution count is zero. Full <permutation group> orbits need not have size $q!$, because unused values can be permuted without changing an assignment; the cyclic-shift argument avoids that mistake.
If an empty <constraint domain> is permitted, there are zero assignments here, but the wording “divisible by $|D|$” then asks about divisibility by zero, which is ordinarily left undefined. The asserted divisibility uses the standard nonempty-domain convention, and the no-solution conclusion still holds for that degenerate input.
Back to article page
