Re: [eclipse-clp-users] posting ic constraints does not terminate

Marco Gavanelli wrote:
> Ulrich Scholz wrote:
>> Dear Kish and all,
>>
>> the following clause does not terminate.  The current version and 5.10 #145
>> show the same result.
>>
>> :- lib(ic). 
>>
>> infinite_loop :-
>>
>>     integers([V1,V2]),
>>     ic:(V2 >= 1),
>>     ic:(V1 > V2),
>>     ic:(V1 $= V2).
>>
>> I've also file a bug report (#629).  Sorry for my impatience but the bug
>> blocks me.
> 
> Dear Ulrich,
> 
> I believe this is not a bug as we usually mean it: it is a well-known 
> problem of CLP(FD) in general. Many CLP(FD) systems terminate with an 
> integer overflow error in this situation.
> 
> There are various solutions proposed in the literature.
> 
> ...
> 

Marco is of course right.  To generally detect this kind of inconsistency
efficiently, you need a solver that looks at several constraints at once.
Marco's solution is one way, another would be to use a simplex solver,
i.e. lib(eplex).

However, the particular case that Ulrich brought up happens to be a bit
simpler than the general case.  Look at the trace:

   (5) 4 RESUME<3>  -(_974{2 .. 1.0Inf}) + _974 $> 0
   (5) 4 EXIT<3>  -(_974{3 .. 1.0Inf}) + _974 $> 0
   (5) 4 RESUME<3>  -(_974{3 .. 1.0Inf}) + _974 $> 0
   (5) 4 EXIT<3>  -(_974{4 .. 1.0Inf}) + _974 $> 0
   (5) 4 RESUME<3>  -(_974{4 .. 1.0Inf}) + _974 $> 0
   (5) 4 EXIT<3>  -(_974{5 .. 1.0Inf}) + _974 $> 0
   ...

What happened is that we originally had 2 constraints, V1 $> V2 and V1 $= V2.
The second constraint was simplified to V1=V2, and we ended up with V1 $> V1
remaining, which is what you see repeatedly waking up, shaving one unit from
the lower bound of V1 every time.

So, if we could only simplify  V1 $> V1  to  V1-V1 $> 0  then to  0 $> 0,
the failure would be obvious.   So the problem is that the constraint keeps
treating the two occurrences of V1 as two different variables, instead of
combining them into one.  This is because in most solvers, this kind of
normalisation (grouping identical variables together) is only done _once_
when the constraint is set up (i.e. if you call X1$>X1 directly, it will
fail as expected), but not when two variables become equal during the course
of computation.

The reason this is not done is that it would add overhead that only pays off
under special circumstances.  But of course ECLiPSe has the facilities to add
this.  The following will do it:

no_longer_infinite_loop :-
       integers([V1,V2]),
       V2 $>= 1,
       V1 $> V2,
       suspend(V1 $> V2, 0, [V1,V2]->bound),
       V1 $= V2.

What happens is that another copy of V1$>V2 gets posted (and simplified,
and found to be inconsistent) as soon as V1 and V2 are being unified.
The Key is the Vars->bound waking condition which will wake on any unification
among the variables occurring in Vars.

Here is more generic code for the same idea:

simplifiable(Constraint) :-
       call(Constraint),       % post for the first time
       suspend(repost_simplified(Constraint), 0, Constraint->bound).

:- demon repost_simplified/2.
repost_simplified(Constraint, Susp) :-
       call(Constraint),       % post again
       ( ground(Constraint) -> kill_suspension(Susp) ; true ).


This can be used as follows:

no_longer_infinite_loop :-
       integers([V1,V2]),
       V2 $>= 1,
       simplifiable(V1 $> V2),
       V1 $= V2.


-- Joachim