CLP(FD) hangs on enigma problem

[ghost]

This here works:

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.6)

?- use_module(library(clpfd)).

?- [X,Y] ins 1..100, X*(X-1)+46 #= (X+Y)*(X+Y-1), 
    label([X,Y]), write(X-Y), nl, fail; true.
11-2
23-1
true.

But this here seems to hang:

?- [X,Y] ins -100..100, X*(X-1)+46 #= (X+Y)*(X+Y-1), 
    label([X,Y]), write(X-Y), nl, fail; true.

[JanWielemaker]

This issue has been mentioned on SWI-Prolog. There might be relevant details there:

https://swi-prolog.discourse.group/t/enigma-for-thought/2860/23

[ghost]

I tested on mac and windows, it just runs and
runs using one core at 100%. Here from a 4 core machine:

[ridgeworks]

Came across this (again) recently while doing my own testing and just wanted to confirm that it's a problem.

Summarizing:

1. clpfd on Jekejeke Prolog 4 works (see discourse thread).
2. Same answers using clpBNR on SWIP (Mac version):

?- [X,Y]::integer(-100,100), {X*(X-1)+46 == (X+Y)*(X+Y-1)}, enumerate([X,Y]), write(X-Y), nl, fail; true.
-22- -1
-22-46
-10- -2
-10-23
11- -23
11-2
23- -46
23-1
true.

3. clpfd on SWIP (8.3.7) is fine if initial values are positive or include smallish negative values, but execution times becomes excessively long for large negative values. Using:

?- [X,Y] ins 0..100, X*(X-1)+46 #= (X+Y)*(X+Y-1), 
    time((label([X,Y]), write(X-Y), nl, fail)); true.
11-2
23-1
% 367,772 inferences, 0.057 CPU in 0.082 seconds (70% CPU, 6407736 Lips)

For:

 -1..100   % 429,591 inferences, 0.067 CPU in 0.101 seconds (66% CPU, 6376308 Lips)
 -5..100   % 694,083 inferences, 0.107 CPU in 0.176 seconds (61% CPU, 6491611 Lips)
-10..100   % 108,426,163 inferences, 14.624 CPU in 14.760 seconds (99% CPU, 7414493 Lips)
-11..100   % 874,706,000 inferences, 118.978 CPU in 119.419 seconds (100% CPU, 7351802 Lips)

(Last two produce additional solutions at -10- -2 and -10-23.)

Need to confirm that the versions of clpfd are the same for SWIP and Jekejeke runs, but something definitely seems to be broken.

[ghost]

Hi, I think it works in my system, a different implementation
from the SWI-Prolog implementation, not simply a rip-off, since
I am using weaker propagation. I am using asymetric propagation,

usually for an equation:

     A #= B

I only do propagate from B to A. And similarly this is also used
when replacing subexpression. Interestingly you cannot make
it oscillate or consume a lot of resources, if you play this one:

     A #= B,
     B #= A

You can try, still works:

?- [X,Y] ins -100..100, X*(X-1)+46 #= (X+Y)*(X+Y-1), 
      (X+Y)*(X+Y-1) #= X*(X-1)+46, 
    label([X,Y]), write(X-Y), nl, fail; true.
-22- -1
-22-46
-10- -2
-10-23
11- -23
11-2
23- -46
23-1
Yes

But maybe who knows, someday there is a case where things
go wrong, after all this is handcrafted and not machine verified
termination condition software. The weaker propagation has also

advantage that time consumption is more predictable.

[ridgeworks]

Thanks for clarifying that. So it looks quite likely it's an issue with the CLP(FD) implementation on SWIP rather than anything in SWIP itself. (Perhaps that was already obvious.)