SWI-Prolog中大于/不等数独求解器实现故障排查求助

核心错误点分析 #

1. 变量重复绑定冲突
   在greatersudoku/3谓词中，你将Horizontals和Verticals的扁平化元素都绑定到了同一个变量Ws：

   append(Horizontals, Ws),
   Ws ins 0..1,
   ...
   append(Verticals, Ws),
   

   这会强制要求Horizontals和Verticals的扁平化列表完全一致，显然不符合逻辑，直接导致约束冲突返回false。需改为使用两个独立变量分别存储：

   append(Horizontals, Ws1),
   Ws1 ins 0..1,
   length(Verticals, 9), maplist(same_length([0,1,2,3,4,5]), Verticals),
   append(Verticals, Ws2),
   Ws2 ins 0..1,
   

2. comp谓词递归调用问题
   你的comp/3谓词通过递归实现反向约束，可能引发CLP(FD)约束处理异常：

   comp(X,1,Y) :- comp(Y,0,X). % 递归调用
   

   应直接声明约束，避免递归：

   comp(X,0,Y) :- X #> Y.
   comp(X,1,Y) :- X #< Y.
   

3. 无初始值的搜索空间问题
   提供的problem/4中数独Rows全为占位符_，即使修复上述错误，也会因搜索空间过大导致求解缓慢，甚至无法在合理时间内找到解。建议先给Rows设置部分初始值进行测试。

修复后的完整代码 #

:- use_module(library(clpfd)).

greatersudoku(Rows, Horizontals, Verticals) :- 
        length(Rows, 9), maplist(same_length(Rows), Rows),
        append(Rows, Vs),
        Vs ins 1..9,
        length(Horizontals, 9), maplist(same_length([0,1,2,3,4,5]), Horizontals),
        append(Horizontals, Ws1),
        Ws1 ins 0..1,
        length(Verticals, 9), maplist(same_length([0,1,2,3,4,5]), Verticals),
        append(Verticals, Ws2),
        Ws2 ins 0..1,
        maplist(all_distinct, Rows),
        transpose(Rows, Columns),
        maplist(all_distinct, Columns),
        Rows = [As,Bs,Cs,Ds,Es,Fs,Gs,Hs,Is],
        Horizontals = [H1,H2,H3,H4,H5,H6,H7,H8,H9],
        Verticals = [V1,V2,V3,V4,V5,V6,V7,V8,V9],
        blocks(As, Bs, Cs, [H1,H2,H3], [V1,V2,V3]),
        blocks(Ds, Es, Fs, [H4,H5,H6], [V4,V5,V6]),
        blocks(Gs, Hs, Is, [H7,H8,H9], [V7,V8,V9]).

blocks([], [], [], _, _).
blocks([N1,N2,N3|Ns1], [N4,N5,N6|Ns2], [N7,N8,N9|Ns3], [Ha|HOR], [Va|VER]) :- 
        all_distinct([N1,N2,N3,N4,N5,N6,N7,N8,N9]),
        Ha = [C1,C2,C3,C4,C5,C6],
        Va = [D1,D2,D3,D4,D5,D6],
        comp(N1,C1,N2), comp(N2,C2,N3), comp(N4,C3,N5), comp(N5,C4,N6), comp(N7,C5,N8), comp(N8,C6,N9),
        comp(N1,D1,N4), comp(N4,D2,N7), comp(N2,D3,N5), comp(N5,D4,N8), comp(N3,D5,N6), comp(N6,D6,N9),
        blocks(Ns1, Ns2, Ns3, HOR, VER).

comp(X,0,Y) :- X #> Y.
comp(X,1,Y) :- X #< Y.

% 带部分初始值的测试问题
problem(1, [[5,_,_,_,_,_,_,_,_],[_,_,_,_,_,_,_,_,_],[_,_,_,_,_,_,_,_,_],[_,_,_,_,_,_,_,_,_],[_,_,_,_,_,_,_,_,_],[_,_,_,_,_,_,_,_,_],[_,_,_,_,_,_,_,_,_],[_,_,_,_,_,_,_,_,_],[_,_,_,_,_,_,_,_,_]], 
        [[0,1,0,0,0,0],[0,0,0,1,0,1],[1,1,1,0,1,0],[1,1,1,0,0,1],[1,0,1,0,0,1],[0,1,1,1,1,0],[0,1,1,0,0,1],[1,1,1,0,0,0],[0,1,0,0,0,1]],
        [[1,0,0,0,0,0],[1,1,1,0,1,1],[0,1,0,1,1,1],[1,0,0,1,0,0],[1,1,1,0,0,1],[0,1,0,1,1,1],[1,1,1,0,0,1],[0,1,1,1,1,0],[0,0,0,1,0,1]]).

测试方式 #

通过以下查询验证修复效果：

problem(1, Rows, H, V), greatersudoku(Rows, H, V), maplist(label, Rows), maplist(writeln, Rows).

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