在clpfd中制定二次方程

Question

CLPFD系统主要不是为了有效处理二次方程,但是,是否有更好的方法来制定如下问题？

似乎问题归结为如下的方程式.SWI library(clpfd)给了:

?- time( ((L+7)^2#=L^2+189, L in 0..10000000) ).
% 252,169,718 inferences, 87208.554 CPU in 87445.038 seconds (100% CPU, 2892 Lips)
ERROR: Out of local stack

但现在SWI的最新版本给出了

?- time( ((L+7)^2#=L^2+189, L in 0..10000000) ).
% 3,805,545,940 inferences, 868.635 CPU in 870.311 seconds (100% CPU, 4381063 Lips)
L = 10.

在SICStus 4.3beta7中,我得到:

| ?- statistics(runtime,_).
yes
| ?- (L+7)*(L+7)#=L*L+189, L in 0..10000000.
L = 10 ? ;
no
| ?- statistics(runtime,[_,T_ms]).
T_ms = 2550 ? ;
no

Answer 1

为了快速解决这个问题，已经具有原始 X #= Y^2 约束的约束求解器还可以实现以下规则：

规则1：

X #= (Y+C)^2 --> H #= Y^2, X #= H + 2*C*Y + C^2
% where C is an integer and X,Y variables

规则#2：

X #= Z^2, Y #= Z^2 --> X #= Z^2, X #= Y.
% where X,Y,Z are variables

上述规则将把方程简化为线性方程，无论如何，它都可以由一个像样的 CLP(FD) 系统直接求解。在这里您可以看到有和没有规则 #2 的系统之间的区别：

没有规则#2：

?- (L+7)*(L+7) #= L*L+189, stored.
_C #= 140+_B-14*L.
_B #>= 0.
_C #>= 0.
_B #= L*L.
_C #= L*L.
Yes

根据规则#2：

?- (L+7)*(L+7) #= L*L+189, stored.
L = 10
?- statistics(time, S), (L+7)*(L+7) #= L*L+189, statistics(time, T), U is T-S.
U = 3

但第二条规则对我来说似乎有点特别。还不确定是否应该保留它。

再见