CLP - missing variable binding

I’m using: SWI-Prolog version 8.0.2-1

Why do I get no bindings for X and Y in the third query, although I get bindings in the first two queries?

?- 2X+Y #= 5 , 2Y +X #= 7 , [Y,X] ins -1000000…sup.
X = 1,
Y = 3.

?- 2X+Y #= 5 , 2Y +X #= 7 , [Y,X] ins inf…100000.
X = 1,
Y = 3.

?- 2X+Y #= 5 , 2Y +X #= 7 , [Y,X] ins inf…sup.
X+2Y#=7,
2
X+Y#=5.

I would appreciate any comment or pointer to further reading.

Thanks,

Stefan

The FD in CLPFD means “finite domain” and inf…sup is not finite, so it returns the relation instead.

Sorry, but -1000000…sup is also not finite, but yields a solution, i.e. can be solved. Why that?

Iam,

-1000000…sup has a finite beginning, which alows the engine to have a starting point.

Why is the engine limited in this aspect? I mean:
The engine could take any number (e.g. 0) as starting point, start two processes (either in parallel or alternate between the two processes), such that 1 process regards inf…0 and the other 0…sup. As the current engine terminates for both semi-open intervals, inf…0 and 0…sup, correctly, a new engine using two processes should be able to come up with the correct result.

1 Like

Usually CLP(FD) doesn’t do Gauss elimination. That it gives a solution in the first two cases is an artefact of interval propagation. Interval propagation might also decide inequalities like here:

?- X #=< Y, Y #< X.
Y#=<X+ -1,
Y#>=X.

?- X #=< Y, Y #< X, [X,Y] ins -1000..1000.
false.

But in some CLP(FD) systems, interval propagation might be implemented with a loop, computing some fixpoint, and might slow down things. You can try:

?- time((X #=< Y, Y #< X, [X,Y] ins -100..100)).
% 23,217 inferences, 0.004 CPU in 0.005 seconds (94% CPU, 5281392 Lips)
false.

?- time((X #=< Y, Y #< X, [X,Y] ins -1000..1000)).
% 226,617 inferences, 0.064 CPU in 0.065 seconds (99% CPU, 3517914 Lips)
false.

?- time((X #=< Y, Y #< X, [X,Y] ins -10000..10000)).
% 2,260,617 inferences, 3.822 CPU in 3.875 seconds (99% CPU, 591508 Lips)
false.

Quite drastic difference for the same problem.

1 Like