prolog 数独求解器耗尽全局堆栈

Question

我尝试在 swi-prolog 中编写二进制数独求解器。 (二进制数独解释here)

问题是我现在已经用完了全局堆栈。我给了它 2 GB，这应该足够了。我使用的算法有缺陷吗？有什么我可以做得更好的事情来避免遇到这样的小谜题缺少全局堆栈错误吗？

更多信息:我已经用完 4X4 谜题的堆栈了，这些谜题的第一个约束仅应用了 6^4 种可能性。您可以通过以下方式查询此问题:

problems(2,Field),binary_sudoku(Field).

代码在这里:

:-use_module(library(clpfd)).

valid_row(Row) :-
    Row ins 0..1,
    length(Row,L),
    sum(Row,#=,L/2).

matrixNth1(Matr,X,Y,El) :-
    nth1(Y,Matr,CurRow),
    nth1(X,CurRow,El).

all_diff([]).
all_diff([X|Y]) :-
    maplist(dif(X),Y),
    all_diff(Y).


valid(_,1,1).
valid(Rows,1,Y) :-
    length(Rows,Y).
valid(Rows,X,1) :-
    length(Rows,X).
valid(Rows,X,X) :-
    length(Rows,X).

valid(Rows,X,Y) :-
    matrixNth1(Rows,X,Y,0).
valid(Rows,X,Y):-
    AboveY is Y-1,
    matrixNth1(Rows,X,AboveY,0).
valid(Rows,X,Y):-
    BelowY is Y+1,
    matrixNth1(Rows,X,BelowY,0).
valid(Rows,X,Y):-
    LeftX is X-1,
    matrixNth1(Rows,LeftX,Y,0).
valid(Rows,X,Y):-
    RightX is X+1,
    matrixNth1(Rows,RightX,Y,0).

binary_sudoku(Rows) :-
    length(Rows,Height),
    transpose(Rows,Cols),
    length(Cols,Height),
    maplist(valid_row,Rows),
    foreach(between(1,Height,X),foreach(between(1,Height,Y),valid(Rows,X,Y))),
    all_diff(Rows),all_diff(Cols).


problems(1,[[_,_],[_,_]]).

problems(2,[[_,_,_,_],[_,_,_,_],[_,_,_,_],[_,_,_,_]]).

Answer 1

这是 ECLiPSe 中的一个紧凑解决方案(带有约束和建模扩展的 Prolog， http://eclipseclp.org )。它对每行/列的 0/1 数量使用 sum-constraints，对 no-two-1 条件使用 sequence/4 约束，并使用 lex_ne/2 来强制行之间的差异。解决方案搜索是通过最后的 labels/1 调用完成的。另外，使用了矩阵表示法，在此类设置中比列表更方便。

:- lib(gfd).

solve(Name, Mat) :-
    problem(Name, Mat),
    dim(Mat, [N,N]),
    Mat #:: 0..1,
    N #= 2*K,
    ( for(I,1,N), param(Mat,K,N) do
        sum(Mat[I,1..N]) #= K,
        sum(Mat[1..N,I]) #= K,
        sequence(1, 2, 3, Mat[I,1..N]),
        sequence(1, 2, 3, Mat[1..N,I]),
        ( for(J,I+1,N), param(Mat,I,N) do
            lex_ne(Mat[I,1..N], Mat[J,1..N]),
            lex_ne(Mat[1..N,I], Mat[1..N,J])
        )
    ),
    labeling(Mat).

problem(2, [](
    [](_,1,0,_,_,_,_,0,_,_,0,_),
    [](_,1,1,_,_,1,_,_,_,_,_,_),
    [](_,_,_,_,_,_,_,_,1,_,_,0),
    [](_,_,0,0,_,_,_,_,_,_,_,0),
    [](_,_,_,_,_,_,1,1,_,0,_,_),
    [](_,1,_,0,_,1,1,_,_,_,1,_),
    [](_,_,_,_,_,_,_,_,1,_,_,_),
    [](1,_,_,1,_,_,_,_,_,_,0,_),
    [](_,1,_,_,_,_,_,_,0,_,_,_),
    [](_,_,_,_,_,_,_,0,_,_,_,_),
    [](1,_,_,_,_,_,_,_,_,_,_,1),
    [](_,1,_,1,_,_,_,_,_,0,0,_))).

这会快速提出(独特的)解决方案:

?- solve(2, M).
M = []([](1, 1, 0, 0, 1, 0, 1, 0, 1, 1, 0, 0),
       [](0, 1, 1, 0, 0, 1, 0, 1, 0, 0, 1, 1),
       [](1, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 0),
       [](1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0),
       [](0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1),
       [](0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0),
       [](1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1),
       [](1, 0, 1, 1, 0, 0, 1, 0, 0, 1, 0, 1),
       [](0, 1, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0),
       [](0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 0),
       [](1, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 1),
       [](0, 1, 0, 1, 0, 1, 0, 1, 1, 0, 0, 1))
Yes (0.03s cpu, solution 1, maybe more)