如何在Prolog中获取Z₁₂方程解集中绝对值最小的解？

问题背景 #

我们需要处理Z₁₂域内的线性同余方程 (x + y) mod 12 = z，变量约束为：

• x ∈ [0, 11]
• y ∈ [-11, 11]
• z ∈ [0, 11]

已基于CLPFD库实现求解谓词，例如求解(11 + y) mod 12 = 1时，得到解集{-10, 2}。现在需要实现筛选逻辑：

• 从解集中提取绝对值最小的解
• 若两个解的绝对值相等（如{-6, 6}），则同时保留两者
• 若绝对值不等，仅保留绝对值更小的那个

实现代码 #

:- use_module(library(clpfd)).

% 计算列表中元素的最小绝对值
min_abs_value([X|Xs], MinAbs) :-
    abs(X, AbsX),
    min_abs_value(Xs, AbsX, MinAbs).

min_abs_value([], CurrentMin, CurrentMin).
min_abs_value([X|Xs], CurrentMin, MinAbs) :-
    abs(X, AbsX),
    (AbsX < CurrentMin ->
        min_abs_value(Xs, AbsX, MinAbs)
    ;
        min_abs_value(Xs, CurrentMin, MinAbs)
    ).

% 筛选出绝对值等于最小绝对值的所有元素
filter_by_min_abs(Solutions, MinAbsSolutions) :-
    min_abs_value(Solutions, MinAbs),
    include(abs_equals(MinAbs), Solutions, MinAbsSolutions).

abs_equals(TargetAbs, X) :-
    abs(X, AbsX),
    AbsX #= TargetAbs.

% 求解给定x和z对应的所有y解
solve_y(X, Z, Ys) :-
    Y in -11..11,
    (X + Y) mod 12 #= Z,
    findall(Y, label([Y]), Ys).

% 整合求解+筛选的完整流程
solve_and_get_min_abs(X, Z, MinAbsYs) :-
    solve_y(X, Z, Ys),
    filter_by_min_abs(Ys, MinAbsYs).

测试示例 #

示例1：解集{-10, 2}的筛选 #

?- solve_and_get_min_abs(11, 1, MinAbsYs).
MinAbsYs = [2].

abs(-10)=10，abs(2)=2，2的绝对值更小，因此仅保留2。

示例2：绝对值相等的解集{-6, 6} #

?- solve_and_get_min_abs(0, 6, MinAbsYs).
MinAbsYs = [-6, 6].

两个解的绝对值都是6，符合“绝对值相等则保留两者”的规则。

示例3：多解场景 #

求解(3 + y) mod 12 = 5，解集为{2, -10}：

?- solve_and_get_min_abs(3, 5, MinAbsYs).
MinAbsYs = [2].

代码说明 #

1. min_abs_value/2：遍历解集列表，计算出所有元素绝对值的最小值，作为筛选阈值。
2. filter_by_min_abs/2：利用CLPFD的include/3谓词，筛选出所有绝对值等于阈值的元素。
3. solve_y/3：基于CLPFD的约束求解，生成给定x和z下所有符合范围的y解。
4. solve_and_get_min_abs/3：一步完成求解和筛选，直接得到最终结果。

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