Prolog - jigoku 求解器 - 运行时

Question

我是 Prolog 的新手(例如:我在 7 周内只用 7 种语言完成了 Prolog 章节)，因此非常欢迎对以下任何代码提出一般性评论。

首先:什么是 hell ？这就像一个数独游戏，除了你得到一个空的网格，并且在每个 3x3 block 内，给出相邻插槽之间的不等式。此处示例:http://krazydad.com/jigoku/books/KD_Jigoku_CH_8_v18.pdf .您仍然需要填充网格，使每一行、每一列和每一 block 都包含数字 1-9。

我尝试基于这个数独解算器实现一个解算器:http://programmablelife.blogspot.co.uk/2012/07/prolog-sudoku-solver-explained.html .出于调试原因，我从一个运行良好的 4x4 示例开始:

:- use_module(library(clpfd)).

small_jidoku(Rows, RowIneqs, ColIneqs) :-
  Rows = [A,B,C,D], 
  append(Rows, Vs), Vs ins 1..4,
  maplist(all_distinct, Rows),
  transpose(Rows, Columns),     
  maplist(all_distinct, Columns),
  blocks(A, B), blocks(C,D), 
  maplist(label, Rows),
  fake_check_ineqs(Rows, RowIneqs),
  fake_check_ineqs(Columns, ColIneqs),
  pretty_print([A,B,C,D]).      

blocks([], []).       
blocks([A,B|Bs1], [D,E|Bs2]) :-     
  all_distinct([A,B,D,E]),      
  blocks(Bs1, Bs2).

fake_check_ineqs([],[]).
fake_check_ineqs([Head|Tail], [Ineq1|TailIneqs]) :- 
    Head = [A,B,C,D],
    atom_chars(Ineq1, [X1,X2]),
    call(X1, A, B),
    call(X2, C, D),
    fake_check_ineqs(Tail, TailIneqs).

pretty_print([]).
pretty_print([Head | Tail]) :-
 print(Head),
 print('\n'),
 pretty_print(Tail).

然后我解决了下面的例子:

time(small_jidoku([[A1,A2,A3,A4],[B1,B2,B3,B4],[C1,C2,C3,C4],[D1,D2,D3,D4]],[><,<>,<<,<<],[><,<<,<>,>>])).

这会在大约 0.5 秒内运行。但是，我也尝试用

解决它

time(small_jidoku([A,B,C,D],[><,<>,<<,<<],[><,<<,<>,>>])).

这似乎需要很长时间。谁能解释为什么当我没有指定每行有 4 个元素时求解器需要更长的时间？对此我天真的回答是 Prolog，如果没有告诉我行的实际格式，将也尝试探索更小/更大的行，因此浪费时间在例如行长度为 5，但这真的是真的吗？

我的第二个问题是关于 9x9 版本，它与 4x4 非常相似，只是 block 当然更大，而且在检查不等式时需要进行更多测试。代码如下:

:- use_module(library(clpfd)).

jidoku(Rows, RowIneqs, ColIneqs) :-  
  Rows = [A,B,C,D,E,F,G,H,I],   
  append(Rows, Vs), Vs ins 1..9,
  maplist(all_distinct, Rows),
  transpose(Rows, Columns),     
  maplist(all_distinct, Columns),         
  blocks(A, B, C), blocks(D, E, F), blocks(G, H, I),     
  maplist(label, Rows),
  check_ineqs(Rows, RowIneqs),
  check_ineqs(Columns, ColIneqs),
  pretty_print([A,B,C,D,E,F,G,H,I]).      

blocks([], [], []).       
blocks([A,B,C|Bs1], [D,E,F|Bs2], [G,H,I|Bs3]) :-     
  all_distinct([A,B,C,D,E,F,G,H,I]),      
  blocks(Bs1, Bs2, Bs3).

check_ineqs([],[]).
check_ineqs([Head|Tail], [Ineq1|TailIneqs]) :- 
    Head = [A,B,C,D,E,F,G,H,I],
    atom_chars(Ineq1, [X1, X2, X3, X4, X5, X6]),
    call(X1, A, B),
    call(X2, B, C),
    call(X3, D, E),
    call(X4, E, F),
    call(X5, G, H),
    call(X6, H, I),
    check_ineqs(Tail, TailIneqs).

测试示例:

    time(jidoku([[A1,A2,A3,A4,A5,A6,A7,A8,A9],
        [B1,B2,B3,B4,B5,B6,B7,B8,B9],
        [C1,C2,C3,C4,C5,C6,C7,C8,C9],
        [D1,D2,D3,D4,D5,D6,D7,D8,D9],
        [E1,E2,E3,E4,E5,E6,E7,E8,E9],
        [F1,F2,F3,F4,F5,F6,F7,F8,F9],
        [G1,G2,G3,G4,G5,G6,G7,G8,G9],
        [H1,H2,H3,H4,H5,H6,H7,H8,H9],
        [I1,I2,I3,I4,I5,I6,I7,I8,I9]], 
        [<>>><>,<<<>><,<<<><>,<><<><,>>><><,><>><>,<>>><>,<>><><,><<>>>], 
        [<<<><>,><<>>>,<><<><,><<<>>,><><<<,<><><>,<>>>><,><><><,<>><>>])).

并且这个已经运行了一夜没有得出任何结论，在这一点上，我完全不知道出了什么问题。我预计会出现一些缩放问题，但不是这个比例!

如果真正知道自己在做什么的人能够对此有所启发，那就太好了!已经谢谢了!

Answer 1

这是我想到的您的代码版本(其他谓词保持不变):

ineqs(Cells, Ineq) :-
        atom_chars(Ineq, Cs),
        maplist(primitive_declarative, Cs, Ds),
        ineqs_(Ds, Cells).

ineqs_([], _).
ineqs_([Op1,Op2|Ops], [A,B,C|Cells]) :-
        call(Op1, A, B),
        call(Op2, B, C),
        ineqs_(Ops, Cells).

primitive_declarative(<, #<).
primitive_declarative(>, #>).

请注意，调用谓词“check_...”并不符合代码的一般性，因为谓词说明了持有什么并且可以使用在几个方向:是的，它可以用来检查约束是否成立，但它可以也用来声明约束必须保持一些变量。因此，我避免命令式并使用更多声明性名称。

您在 jidoku/3 中使用 ineqs/2 与:maplist(ineqs, Rows, RowsIneqs) 等

您的示例和新版本的结果，使用 SWI 7.3.2:

?- length(Rows, 9), maplist(same_length(Rows), Rows),
   time(jidoku(Rows,
   [<>>><>,<<<>><,<<<><>,<><<><,>>><><,><>><>,<>>><>,<>><><,><<>>>],
   [<<<><>,><<>>>,<><<><,><<<>>,><><<<,<><><>,<>>>><,><><><,<>><>>])),
   maplist(writeln, Rows).
% 2,745,471 inferences, 0.426 CPU in 0.432 seconds (99% CPU, 6442046 Lips)
[1,5,4,8,7,2,6,9,3]
[2,3,9,1,6,5,7,4,8]
[6,7,8,3,9,4,2,5,1]
[3,4,1,2,5,6,8,7,9]
[9,6,5,7,1,8,3,2,4]
[8,2,7,9,4,3,1,6,5]
[4,9,3,6,2,1,5,8,7]
[7,8,2,5,3,9,4,1,6]
[5,1,6,4,8,7,9,3,2]
Rows = [[1, 5, 4, 8, 7, 2, 6, 9|...], ...].

事实上，请注意，在这种特殊情况下，根本不需要标记来计算唯一的解决方案，因为约束求解器足够强大，可以将所有域简化为单例集。

在您之前的版本中，所有的时间都被不必要地浪费在天真地生成最终被认为是不一致的排列上。在新版本中，约束求解器有机会更早地应用这些知识。

因此建议首先声明所有约束，然后才调用labeling/2 来搜索具体的解决方案，如CLP(FD) manual 中所述。 .