Enforcing inequality of lists?

Question

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?

Answer 1

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.