Prolog CLP(FD)实现GCD的不同查询终止性差异原因求解

现有如下GCD的Prolog实现：

:- use_module(library(clpfd)).
:- use_module(library(reif)).

gcd(A, B, C) :-
  C #> 0, A #>= C, B #>= C,
  R #= A mod B,
  A mod C #= 0,
  B mod C #= 0,
  if_(R = 0, C = B, gcd(B, R, C)).

执行如下查询可以正常终止：

A in 2..10, gcd(A, 14, 7), indomain(A).

但结构相似的如下查询无法终止：

A in 2..10, gcd(A, 16, 4), indomain(A).

两个查询行为差异的核心来自这段GCD实现的逻辑缺陷，以及clpfd约束传播、reif库分支判断的特性：

• 首先看if_(R = 0, C = B, gcd(B, R, C))的分支逻辑：当R没有被完全实例化为具体值时，reif库的if_会生成两个分支分别探索：先尝试R=0的分支，失败后回溯尝试R≠0的分支触发递归。
• 第一个查询中，C=7、B=14，结合A mod 7 #= 0和A in 2..10的约束，约束传播会直接把A的取值缩小到唯一值7，R被实例化为14 mod 7 = 0，直接走R=0的分支验证C=B（7=7）成立，返回解A=7。后续indomain枚举下一个解时回溯，R≠0的分支和R=0的事实冲突，直接失败，程序正常终止。
• 第二个查询中，C=4、B=16，结合约束A的取值缩小到4和8：
  1. 当A=4时，R=16 mod 4=0，走R=0分支验证C=B（4=4）成立，返回第一个解A=4。
  2. indomain继续枚举下一个解，回溯到A=8的分支，此时R=16 mod 8=0，走R=0分支验证C=B会得到4=8的矛盾，触发回溯进入R≠0的分支。
  3. 此时clpfd没有立刻检测到R=16 mod 8=0和R≠0的约束矛盾，而是继续执行递归调用gcd(8, R, 4)，递归调用又会触发新的约束检查和分支判断，无限生成新的递归路径，最终导致程序无法终止。

调整约束顺序，把分支判断和终止逻辑提前，同时先保证欧几里得算法的参数顺序要求，就可以避免无限递归：

gcd(A, B, C) :-
  C #> 0,
  A #> 0, B #> 0,
  R #= A mod B,
  if_(R = 0, 
      (C = B, A mod C #= 0, B mod C #= 0), 
      (A #>= B, gcd(B, R, C))).

内容的提问来源于stack exchange，提问作者vasily