Re: [eclipse-clp-users] Simple problem - strange effect

Philipp Marcus schrieb:
> Hi,
> 
> thanks for your hints. I've changed to IC and added the constraint 
> X#=2. But now I still have too less propagation in my example:
> 
>    :-lib(ic).
>    :-lib(propia).
> 
>    con1(1,1,0).
>    con1(1,2,0).
>    con1(1,3,0).
> 
>    cons(X,Y,B) :-
>         con1(X,Y,B) infers most.
> 
>    execute(X) :-
>         X#::[1,2,3],    cons(1,X)    or    X#=1 or X#=2.
> 
> Why is it not possible for IC to infer that the domain of X only
> consists of the elements [1,2]? Instead I get the output:
> 
>    ?- execute(X).
>    X = X{1 .. 3}
>    There are 4 delayed goals.
>    Yes (0.00s cpu)
> 
> Best regards,
> Philipp

What happens is that "under the hood", the 'or'/2 constraint is replaced
by more simple constraints similar to those that Wit gave in his reply, i.e.

cons(1,X) or X #= 1

gets replaced by

cons(1,X,B1), #=(X,1,B2), B1+B2 #>= 1

In this case, since B1 == 0, B2 must be 1, so X is immediately bound to 1.


Now consider this case:

X #= 1 or X #= 2

gets replaced by

#=(X,1,B1), #=(X,2,B2), B1+B2 #>= 1

(btw, you can see the delayed goals by selecting Tools->Delayed Goals in
tkeclipse)

Now either B1 or B2 can be 1, or both. But unless one is bound, no
propagation happens, since the equality constraints remain passive. No
information is propagated that would change X's domain.

In general, each constraint has its own triggers, which ensure
propagation whenever something "interesting" happens to the variables on
which the constraint is posted. But the constraint solver is usually not
sentient enough to determine on its own when two constraints can be
combined to allow the extraction of additional information. (which btw
is always a difficult point to explain to customers, I had to learn
since working in industry...) Therefore, the logical operation
constraints like and/2, or/2, etc will only become active when one of
the boolean variables of the reified constraints on which they are
posted is bound.

Cheers,
Thorsten