JCumin/Brachylog

Prime factorisation uses low level arithmetic

Closed this issue · 4 comments

Change that to CLP(FD) arithmetic. Low level arithmetic makes it fail for big numbers (float_overflow).

I have a solution for it but it is significatively slower than the low-level version for big numbers it can still process, so I am unsure I should actually change it (Finding the "ceiled" square root is the long part for CLPFD, even using min when labeling).

Does this help?

ceiled_square_root(0, 0).
ceiled_square_root(N0, Root) :-
        N1 #= N0 - 1,
        Max in 0..N1,
        R0^2 #= Max,
        Root #= Root0 + 1,
        fd_sup(R0, Root0).

Usage example:

?- time(ceiled_square_root(10^99, R)).
8,425 inferences, 0.002 CPU in 0.002 seconds (100% CPU, 3436000 Lips)
R = 31622776601683793319988935444327185337195551393253.

Tested with:

?- length(_, L), ceiled_square_root(L, R), S is ceil(sqrt(L)), R #\= S.

(No counterexample found so far ...)

The key is to set up the constraints in such a way that CLP(FD) propagation helps us find the square root. I hope the speed is satisfactory. If you need more such CLP(FD) propagations in the future, please let me know!

Speed seems now "acceptable" for 2^1000 (about 5 times faster than my solution), thanks.

Please try it with the latest git version: I have installed a patch that makes propagation in this case faster by orders of magnitude with larger numbers.