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

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.

One is defining some finite domain (large but finite) for the variables, 
as in:

infinite_loop1 :-
     integers([V1,V2]),
     V2 :: 1..1000000,
     V1 :: -1000000..1000000,
     ic:(V2 >= 1),
     ic:(V1 > V2),
     ic:(V1 $= V2).

Notice that the computing time can be high, as the solver tries to 
remove one value in each iteration, and fails only when there are no 
more values in the domain of one variable.

Another solution is defining a new constraint, for example in CHR, and 
tell the solver that two numbers cannot be equal and one greater of the 
other at the same time, as in:

constraints greater_than/2, equal/2.

greater_than(X,X) <=> false.
greater_than(X,Y), greater_than(Y,Z) ==> greater_than(X,Z).
% ... other rules for defining the behaviour of greater_than

%if finite domain, post ic constraint
greater_than(X,Y) ==> get_bounds(X,Lx,Hx), get_bounds(Y,Ly,Hy), 
integer(Lx), integer(Ly), integer(Hx), integer(Hy) | ic:(X>Y).

% ... various rules for defining the behaviour of equal

% if X>Y and X=Y, then fail
greater_than(X,Y), equal(X,Y) <=> false.

chr_solution:-
     integers([V1,V2]),
     ic:(V2 >= 1),
     greater_than(V1,V2),
     equal(V1,V2).

(of course, you can use library ECH instead of CHR).

Cheers,
Marco

-- 
Marco Gavanelli, Ph.D. in Computer Science
Dept of Engineering
University of Ferrara
Via Saragat 1 - 44100 Ferrara (Italy)
Tel  +39-0532-97-4833
Fax  +39-0532-97-4870
http://www.ing.unife.it/docenti/MarcoGavanelli/