Prolog类数独求解器遇分支问题，求单一完整解实现方案

我用Prolog实现了一款遵循同一分组内值不重复规则的类数独求解器，现有代码可运行，但会生成分支结果，无法返回所有值填充完成的单一解。

现有代码及问题复现 #

:- use_module(library(clpfd)).

solve(Input) :- 
    append(Input, Items),
    bagof(V, member(G-V, Items), Group),
    length(Group, Len),
    Group ins 1..Len,
    all_distinct(Group).

input(I) :- I = [
    [a-1, b-_],
    [a-_, b-1]
].

执行查询：

?- input(I), solve(I).

得到分支结果：

I = [[a-1, b-_], [a-2, b-1]] ;
I = [[a-1, b-2], [a-_, b-1]].

我期望返回所有占位符_都被填充完成的单一I值，但不清楚分支产生的原因，也不知道如何修改代码避免分支。

补充说明（更复杂的期望示例） #

已将所有值统一为分组-值格式，以下是期望的完整求解效果：

input(I) :- I = [[a-1, b-_, b-2],
                 [a-_, c-_, b-1],
                 [a-2, a-4, b-3]].

执行查询后期望得到：

?- input(I), solve(I).
I = [[a-1, b-4, b-2],
     [a-3, c-1, b-1],
     [a-2, a-4, b-3]].

当前算法能正确求解每个分组，但每个分组的解处于不同分支中。

问题原因与修复方案 #

分支产生的原因 #

• bagof/3的特性：bagof/3会为每个不同的分组G生成独立的求解分支，导致每个分组的解分开返回，无法合并成一个完整的填充结果。
• 未触发完整变量绑定：当前代码仅对每个分组的变量设置约束，但没有强制CLP(FD)求解器完成所有变量的绑定，导致部分变量仍为未绑定的占位符，形成多个不完整的分支。

修改后的代码 #

:- use_module(library(clpfd)).

solve(Input) :-
    % 展开所有项并提取唯一分组
    append(Input, Items),
    findall(G, member(G-_, Items), Groups),
    sort(Groups, UniqueGroups),
    % 为每个分组应用约束
    maplist(enforce_group_constraint(Items), UniqueGroups),
    % 强制所有变量绑定到具体值
    append(Input, AllItems),
    maplist(bind_value, AllItems),
    % 确保输入结构完全实例化
    ground(Input).

% 对单个分组应用约束：值范围为1到分组大小，且全不重复
enforce_group_constraint(Items, Group) :-
    findall(V, member(Group-V, Items), GroupValues),
    length(GroupValues, Len),
    GroupValues ins 1..Len,
    all_distinct(GroupValues).

% 触发CLP(FD)求解，绑定变量到具体值
bind_value(_-V) :-
    label([V]).

代码说明 #

• 统一处理所有分组：通过findall/3和sort/2获取唯一分组列表，再用maplist/2对每个分组批量应用约束，避免bagof/3产生分支。
• 强制完整绑定：用label/1触发CLP(FD)求解器为所有变量生成具体值，再通过ground/1确保整个输入结构的所有变量都被实例化，最终返回单一完整解。

测试补充示例的查询：

?- input(I), solve(I).
I = [[a-1, b-4, b-2], [a-3, c-1, b-1], [a-2, a-4, b-3]].

此时会直接返回完全填充的单一结果，无分支。

内容的提问来源于stack exchange，提问作者João Haas