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

Question

我尝试在swi-prolog中编写二进制数独求解器.(这里解释了二元数独)

问题是我现在正在耗尽全局堆栈.我给它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/1s数使用sum-constraints,对no-three-1s条件使用sequence/4约束,使用lex_ne/2来强制行之间的差异.解决方案搜索由最后的标记/ 1调用完成.此外,使用Matrix-notation,这比这些设置中的列表更方便.

:- 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)