prolog - swi prolog 中的二进制数独

Question

作为 prolog 新手，我想尝试实现一个二进制数独求解器。(代码如下，swi-prolog)。二进制数独在这里解释:https://cstheory.stackexchange.com/questions/16982/how-hard-is-binary-sudoku-puzzle

但是，在执行以下查询时:

binarySudoku([[1,0],[0,1]]). I get "true."
binarySudoku([[1,_],[_,_]]). I get "false."

现在显然它不应该返回 false 因为有一个解决方案......为什么会发生这种情况/我该如何解决这个问题？

:-use_module(library(clpfd)).

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

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

allDifferent([]).
allDifferent([X|Y]) :-
    not(member(X,Y)),
    allDifferent(Y).


invalid(Rows,X,Y) :-
    AboveY is Y-1,
    BelowY is Y+1,
    matrixNth(Rows,X,Y,1),
    matrixNth(Rows,X,AboveY,1),
    matrixNth(Rows,X,BelowY,1).
invalid(Rows,X,Y) :-
    LeftX is X-1,
    RightX is X+1,
    matrixNth(Rows,X,Y,1),
    matrixNth(Rows,LeftX,Y,1),
    matrixNth(Rows,RightX,Y,1).

binarySudoku(Rows) :-
    length(Rows,Height),
    transpose(Rows,Cols),
    length(Cols,Height),
    maplist(validRow,Rows),
    foreach(between(1,Height,X),foreach(between(1,Height,Y),not(invalid(Rows,X,Y)))),
    allDifferent(Rows).

Answer 1

而不是 (\+)/1 ，在这种情况下逻辑上不合理，请使用纯约束 dif/2 :您的代码按预期工作，因为您更改了行 not(member(X,Y))到:
maplist(dif(X), Y)
示例查询(请注意，我还使用了 a_more_readable_naming_convention 而不是 OfMixingTheCases):

?- binary_sudoku([[1,A],[B,C]]), label([A,B,C]).
A = B, B = 0,
C = 1 ;
false.

+1 用于使用 CLP(FD)，非常适合此任务。