Prolog - jigoku 求解器 - 运行 时间

Prolog - jigoku solver - run time

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

首先:什么是地狱?这就像一个数独游戏,除了你得到一个空的网格,并且在每个 3x3 块内,给出相邻插槽之间的不等式。此处示例:http://krazydad.com/jigoku/books/KD_Jigoku_CH_8_v18.pdf。您仍然需要填充网格,使每一行、每一列和每一块都包含数字 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,如果没有告诉我的实际格式行,还将尝试探索 smaller/bigger 行,因此会浪费时间,例如行长度为 5,但这是真的吗?

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

:- 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]], 
        [<>>><>,<<<>><,<<<><>,<><<><,>>><><,><>><>,<>>><>,<>><><,><<>>>], 
        [<<<><>,><<>>>,<><<><,><<<>>,><><<<,<><><>,<>>>><,><><><,<>><>>])).

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

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

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

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.

中所述