Q: Is the fixed point of constraint propagation unique?

The answer is yes (with thanks to Rina Dechter).

First imagine there were multiple fixed points with different domain sets. Each of these domain sets would be arc-consistent by definition. Now simply take the union of all these domains and you can easily verify that that is still arc-consistent (for each value in a source domain there must be a possible value in the target domain, but this is guaranteed by the fact that each sub-solution admits a possible value in the target; therefore you can simply pick that). We call the union the maximal arc-consistent set.

Now let's see if constraint propagation will converge to that maximal set. First we establish it converges. This follows because at each iteration we remove values form domains and we stop when there are no more changes. Clearly, since the domains are finite this must stop at some point.

To prove that we will converge on the maximal set, we need to recall if a particular domain is consistent for all its incoming messages, then a strictly larger domain will also be consistent for all its incoming messages. Let's assume that some message from Di to domain Dj is going to remove a value from the maximal set (at Di) for the first time. This means that the target, Dj, must have had a domain smaller than the one in the maximal set to the begin with. If not, by the definition of the maximal set, the arc was consistent and no value would have been removed from source Di using constraint propagation. This leads to a contradiction because we assumed that this was the first message that was going to remove the first value from a domain in the maximal set. Thus, constraint programming will not remove values which are in the maximal set, but on the other hand it will not stop before every arc is consistent either. Therefore, irrespective of the order in which we send messages, it will always converge on the same unique maximal set.