如何调试Prolog CLPZ中n_factors/2谓词的非终止问题

问题表现 #

实现的支持双向调用的n_factors/2质因数分解谓词，在执行带范围约束的定长因子列表查询时，输出全部合法解后无法自动终止，会持续探索大数值搜索空间。
原核心实现代码：

:- use_module(library(clpz)).

n_factors(N, Fs) :-
    integer(N),
    N > 1,
    primes(Ps),
    n_factors0(N, Fs, Ps),
    !.

n_factors(N, Fs) :-
    var(N),
    primes(Ps),
    N #> 1,
    above(2, N),
    n_factors0(N, Fs, Ps).

above(I, I).
above(I, N) :- I1 is I + 1, above(I1, N).

n_factors0(N, [F|Fs], [P|Ps]) :-
    N #> 1,
    F #=< N,
    P #=< N,
    (   P * P #> N ->
        F = N, Fs = []
        ;   (   N #= N1 * P ->
                F #= P, n_factors0(N1, Fs, [P|Ps])
            ;   F #> P, n_factors0(N, [F|Fs], Ps)
        )
    ).

测试查询与输出：

?- C #> 6, C #< 12, n_factors(A, [B,C]).
   C = 7, A = 14, B = 2
;  C = 7, A = 21, B = 3
;  C = 11, A = 22, B = 2
;  C = 11, A = 33, B = 3
;  C = 7, A = 35, B = 5
;  C = 7, A = 49, B = 7
;  C = 11, A = 55, B = 5
;  C = 11, A = 77, B = 7
;  C = 11, A = 121, B = 11
;
% 此处程序持续运行不终止

附依赖的无限素数列表实现（该部分无逻辑问题）：

primes(Ps) :-
    Ps = [2,3|T],
    primes0(5, Ps, Ps, T),
    !.

primes0(C, [D|Ds], Ps, T) :-
    (   D * D > C ->
        T = [C|T1], C1 is C + 2, freeze(T1, primes0(C1, Ps, Ps, T1))
        ;   (   C mod D =:= 0 ->
                C1 is C + 2, primes0(C1, Ps, Ps, T)
            ;   primes0(C, Ds, Ps, T)
        )
    ).

根因定位 #

不需要逐处试加不变量，问题集中在三个违反CLP(Z)谓词编写原则的点：

• 冗余的无界枚举：手动实现的above(2, N)是无上限的整数生成器，放在约束前会强制从2开始逐一枚举N，哪怕约束已经限定N的最大可能值，生成器也不会停止。CLP(Z)本身可以通过约束自动确定变量范围，不需要手动编写这类裸枚举谓词。
• 缺失核心不变量约束：质因数分解的结果是非递减素数序列，原代码仅在跳过素数的分支约束了F #> P，没有在全局约束因子列表的有序性，导致递归时会无限跳过更大的素数，哪怕这些素数已经超过查询中限定的因子上限（比如C<12，素数大于11后不可能成为解，但程序仍会持续遍历素数列表）。
• 硬编码剪枝破坏约束传播：原代码中手动写的P*P #> N分支强制要求此时Fs必须为空，没有把因子长度的约束传递进去，导致当因子列表长度固定时，该分支的匹配逻辑无法正确触发剪枝。

修复方案 #

去掉冗余的分支判断和无界枚举，把核心不变量放在递归入口，修复后的代码如下：

:- use_module(library(clpz)).

n_factors(N, Fs) :-
    N #> 1,
    primes(Ps),
    n_factors0(N, Fs, Ps).

% 递归边界：最后一个因子就是N本身，无后续因子
n_factors0(N, [N], _) :-
    N #> 1.
n_factors0(N, [F|Fs], [P|Ps]) :-
    N #> 1,
    F #>= P,
    F #=< N,
    (   F #= P
    ->  N #= N1 * F,
        n_factors0(N1, Fs, [P|Ps])
    ;   F #> P,
        n_factors0(N, [F|Fs], Ps)
    ).

修复后执行相同查询，会输出全部9个合法解后自动返回false终止，不会进入无限搜索。

通用排查思路 #

CLP系列谓词出现不终止问题时，按以下优先级排查即可，不需要盲目试加约束：

1. 检查是否存在无界生成器放在约束前的情况：所有手动编写的枚举逻辑必须放在所有约束之后，且必须有明确的终止边界，优先依赖CLP求解器自身的枚举能力，不要裸写递归枚举整数。
2. 检查递归分支的参数收敛性：每一次递归调用，必须至少有一个参数向边界收敛（比如待分解的N变小、待遍历的素数列表向前移动、因子列表长度变短），不能出现所有参数都无界变化的分支。
3. 检查核心不变量是否前置：问题本身的数学不变量（比如质因数非递减、乘积等于原数、因子范围）必须放在递归入口，不要分散在各个分支里，避免分支绕过约束传播。

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