Re: Propagation in ECLiPSe

Michael Thielscher wrote:
> ...
> The problem seems a bit more complicated, actually: I would like
> 
> ((X#=1 #/\ Y#=2) #\/ (X#=3 #/\ Y#=4)) #/\ (X#\=1 #\/ Y#\=2).
> 
> to propagate! Notice the rightmost disjunction. If X isn't 1 or Y isn't 2,
> then X,Y cannot be 1,2; hence, X,Y must be 3,4. This seems not to
> propagate even if I add domains for X,Y. Any idea what I could do?

[I'm copying this answer to the eclipse-users mailing list because
I believe it is of general interest - I hope you don't mind!]


This is a rather fundamental problem: it is much more difficult
to extract information from disjunctions than from conjunctions.
>From the conjunction X#\=1 #/\ Y#\=2 the system can infer reduced
domains:

?- [X,Y]::0..5,  X#\=1 #/\ Y#\=2.
X = X{[0, 2..5]}
Y = Y{[0, 1, 3..5]}
Yes (0.00s cpu)

But from the disjunction this is of course not possible:

?- [X,Y]::0..5,  X#\=1 #\/ Y#\=2.
X = X{[0..5]}
Y = Y{[0..5]}
Delayed goals:
...
Yes (0.00s cpu)

Since nothing can be inferred from X#\=1 #\/ Y#\=2 alone,
nothing can be inferred from your larger expression either.
The individual #= and #\= constraints reason only locally,
and are simply connected via their reification-booleans.


What you need to make the strong inference you want is some
form of "global reasoning" on the whole expression.
The easiest way to do that in Eclipse is to use lib(propia):

?- lib(propia).
?- ((X#=1,Y#=2 ; X#=3,Y#=4),(X#\=1;Y#\=2)) infers most.
X = 3
Y = 4
Yes (0.00s cpu)

There was no need here to use reified constraints: I have just
used the normal constraints and combined them with ',' and ';'.
The result is a nondeterministic goal, which then gets annotated
with 'infers most'. This turns it into a (deterministic) constraint.


You could also have kept your original constraints and added
some (local) labeling to achieve a similar effect:

?- lib(propia).
?- [X,Y]::0..5,
   (
	((X#=1 #/\ Y#=2) #\/ (X#=3 #/\ Y#=4)) #/\ (X#\=1 #\/ Y#\=2),
	labeling([X,Y])
   ) infers most.

X = 3
Y = 4
Yes (0.01s cpu)

You see that you basically solve a small sub-problem (with
constraints and search) and the infers-mechanism extracts
deterministic information from this sub-problem and uses it
for propagation.


For more information, see the chapter on Propia in the "Constraint
Library Manual". The Eclipse web site has papers on the
"generalised propagation" technique which lib(propia) implements.


-- 
 Joachim Schimpf              /             phone: +44 20 7594 8187
 IC-Parc, Imperial College   /            mailto:J.Schimpf@ic.ac.uk
 London SW7 2AZ, UK         /    http://www.icparc.ic.ac.uk/eclipse