From: Joachim Schimpf <joachim.schimpf_at_infotech.monash.edu.au>

Date: Wed, 14 Jan 2009 12:15:15 +1100

Date: Wed, 14 Jan 2009 12:15:15 +1100

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. -- JoachimReceived on Wed Jan 14 2009 - 04:15:32 CET

*
This archive was generated by hypermail 2.2.0
: Thu Feb 02 2012 - 02:31:58 CET
*