For a given CSP I used a variety of viewpoints, one of which is a somewhat more exotic boolean model which uses a variable array of size NxNxN. Then I enforce unequality of various subarrays with this snippet :
(foreach(X, List1),
foreach(Y, List2),
foreach((X #\= Y), Constraints)
do true),
1 #=< sum(Constraints).
The performance of the model is bad, so I was curious to know more about what happens behind the scenes. Is this a proper way to ensure that two given lists are different? Do I understand it correctly that every constraint (X #\= Y) in the Constraints list needs to be instantiated before the sum is calculated, meaning that all the corresponding variables need to be instantiated too?
The constraint library library(ic_global) is indeed missing a constraint here; it should provide lex_ne/2, analogous to lex_lt/2. This would have the same logical and operational behaviour as the code you have written, i.e. propagate when there is only a single variable left in its argument lists:
?- B#::0..1, lex_ne([1,0,1], [1,B,1]).
B = 1
For comparison, you can try the sound difference operator ~=/2 (called dif/2 in some Prologs). This is efficiently implemented, but it doesn't know about domains and will thererefore not propagate; it simply waits until both sides are instantiated and then fails or succeeds:
?- B#::0..1, [1,0,1] ~= [1,B,1].
B = B{[0, 1]}
There is 1 delayed goal.
?- B#::0..1, [1,0,1] ~= [1,B,1], B = 0.
No (0.00s cpu)
Whether this is overall faster will depend on your application.