Always true for a nonempty finite constraint domain, as conventionally assumed. Write and identify its values with . For each satisfying assignment , simultaneously replace every value by
This permutation of the common constraint domain preserves every equality and inequality, hence every all-different constraint. The resulting assignments are distinct: equality of even one coordinate before and after a shift forces . There is at least one variable, since and .
The cyclic group of shifts therefore partitions the solution set into disjoint orbits of size . It follows that
The conclusion includes an unsatisfiable instance, whose solution count is zero. Full permutation group orbits need not have size , 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 ” 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.

Articles by others on the same topic (0)

There are currently no matching articles.