performance - 序言程序: clp(fd) too slow无输出

Question

我是 Prolog 编程的新手，我写了一个代码来解决 4 x 4 幻方，但是当我运行程序时，程序没有给出任何输出；它只是继续执行(忙)，最终我不得不退出 SWI-Prolog。请指导我解决这个问题。

代码:

:- use_module(library(clpfd)).

magic_square(Puzzle,Sum) :-
    Puzzle = [S11,S12,S13,S14,
              S21,S22,S23,S24,
              S31,S32,S33,S34,
              S41,S42,S43,S44],

    Puzzle ins 1..16,
    all_different(Puzzle),
    labeling([],Puzzle),

    R1 = [S11,S12,S13,S14],           % rows
    R2 = [S21,S22,S23,S24],
    R3 = [S31,S32,S33,S34],
    R4 = [S41,S42,S43,S44],

    C1 = [S11,S21,S31,S41],           % columns
    C2 = [S12,S22,S32,S42],
    C3 = [S13,S23,S33,S43],
    C4 = [S14,S24,S34,S44],

    Diag1 = [S11,S22,S33,S44],        % diagonals
    Diag2 = [S14,S23,S32,S41],

    S11 + S12 + S13 + S14 #= Sum,     % rows
    S21 + S22 + S23 + S24 #= Sum,
    S31 + S32 + S33 + S34 #= Sum,
    S41 + S42 + S43 + S44 #= Sum,

    S11 + S21 + S31 + S41 #= Sum,     % columns
    S12 + S22 + S32 + S42 #= Sum,
    S13 + S23 + S33 + S43 #= Sum,
    S14 + S24 + S34 + S44 #= Sum,

    S11 + S22 + S33 + S44 #= Sum,     % diagonals
    S14 + S23 + S32 + S41 #= Sum.

我尝试将 sum 变量更改为 64，但仍然没有任何 react 。我为此使用了 SWI-Prolog。

Answer 1

第一件事!

与 clp(fd), 总是 推迟枚举目标，如 labeling/2直到所有的限制都被声明。一般是良好做法 进行如下操作:

声明所有使用的变量的初始域

陈述所有应该通过约束保持的关系

通过 labeling/2 触发对解决方案的搜索或其他有限域枚举目标

在评论中，您注意到同样适用于 3x3 幻方；同意，但有效 不是因为 标签和约束张贴的相反顺序——它有效 尽管如此 .

您在合理的时间内获得解决方案的原因是找到大小为 3x3 的幻方比找到 4x4 的幻方要容易几个数量级。

因此，重新排序谓词中的目标 magicSquare4x4_withSum/2像这样:

:- use_module(library(clpfd)).

magicSquare4x4_withSum(Zs,Sum) :-
    Zs = [S11,S12,S13,S14,
          S21,S22,S23,S24,
          S31,S32,S33,S34,
          S41,S42,S43,S44], 
    Zs ins 1..16,                   % state the initial finite domain
    S11 + S12 + S13 + S14 #= Sum,   % rows
    S21 + S22 + S23 + S24 #= Sum,
    S31 + S32 + S33 + S34 #= Sum,
    S41 + S42 + S43 + S44 #= Sum,    
    S11 + S21 + S31 + S41 #= Sum,   % columns
    S12 + S22 + S32 + S42 #= Sum,
    S13 + S23 + S33 + S43 #= Sum,
    S14 + S24 + S34 + S44 #= Sum,
    S11 + S22 + S33 + S44 #= Sum,   % diagonals
    S14 + S23 + S32 + S41 #= Sum,   
    all_different(Zs).              % no two variables shall have the same value

magicSquare4x4_withSum/2最通用的查询立即确定性地成功；但是，给出的答案并未显示某些 4x4 幻方的具体值；相反，它提出了解决方案必须遵守才能存在的待决约束。

?- time(magicSquare4x4_withSum(Zs,Sum)).
% 7,780 inferences, 0.001 CPU in 0.001 seconds (99% CPU, 8396967 Lips)
Zs = [_G9481, _G9484, _G9487, _G9490, _G9493, _G9496, _G9499, _G9502|...],
_G9481 in 1..16,
all_different([_G9481, _G9484, _G9487, _G9490, _G9493, _G9496, _G9499|...]),
_G9481+_G9496+_G9511+_G9526#=Sum,
_G9481+_G9493+_G9505+_G9517#=Sum,
_G9481+_G9484+_G9487+_G9490#=Sum,
_G9484 in 1..16,
_G9484+_G9496+_G9508+_G9520#=Sum,
_G9487 in 1..16,
_G9487+_G9499+_G9511+_G9523#=Sum,
_G9490 in 1..16,
_G9490+_G9499+_G9508+_G9517#=Sum,
_G9490+_G9502+_G9514+_G9526#=Sum,
_G9493 in 1..16,
_G9493+_G9496+_G9499+_G9502#=Sum,
_G9496 in 1..16,
_G9499 in 1..16,
_G9502 in 1..16,
_G9505 in 1..16,
_G9505+_G9508+_G9511+_G9514#=Sum,
_G9508 in 1..16,
_G9511 in 1..16,
_G9514 in 1..16,
_G9517 in 1..16,
_G9517+_G9520+_G9523+_G9526#=Sum,
_G9520 in 1..16,
_G9523 in 1..16,
_G9526 in 1..16,
Sum in 4..64.

现在，让我们开始吧!

?- time((magicSquare4x4_withSum(Zs,Sum), labeling([],Zs))).
% 8,936,459 inferences, 1.025 CPU in 1.025 seconds (100% CPU, 8720473 Lips)
Zs = [1, 2, 15, 16, 12, 14, 3, 5, 13|...],
Sum = 34 ;
% 37,098 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 6073990 Lips)
Zs = [1, 2, 15, 16, 13, 14, 3, 4, 12|...],
Sum = 34                                    % and the search goes on...

我们可以做些什么来加快搜索速度？首先，我们尝试不同的标签启发式/选项。

?- time((magicSquare4x4_withSum(Zs,Sum), labeling([ff],Zs))).
% 5,056,298 inferences, 0.578 CPU in 0.578 seconds (100% CPU, 8749040 Lips)
Zs = [1, 2, 15, 16, 12, 14, 3, 5, 13|...],
Sum = 34 ;
% 36,783 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 5733914 Lips)
Zs = [1, 2, 15, 16, 13, 14, 3, 4, 12|...],
Sum = 34                                    % and the search goes on...

我们还能做什么？通过提供总和作为常数来帮助搜索。

?- time((magicSquare4x4_withSum(Zs,34), labeling([],Zs))).
% 106,296 inferences, 0.017 CPU in 0.017 seconds (100% CPU, 6242045 Lips)
Zs = [1, 2, 15, 16, 12, 14, 3, 5, 13|...] ;
% 36,858 inferences, 0.009 CPU in 0.009 seconds (100% CPU, 4076658 Lips)
Zs = [1, 2, 15, 16, 13, 14, 3, 4, 12|...] ;
% 209,206 inferences, 0.028 CPU in 0.028 seconds (100% CPU, 7430044 Lips)
Zs = [1, 2, 16, 15, 13, 14, 4, 3, 12|...]   % and the search goes on...

在性能方面，先验地将总和限制为值 34 会产生巨大的影响!

编辑 2015-04-24

我们还能做什么？

我们可以通过排除仅仅是彼此“翻转”或“旋转”的解决方案来添加限制搜索和解决方案空间的附加约束。

让我们考虑大小为 3x3 的幻方:有 8 个不同的幻方，但实际上它们都是同一个幻方的“翻转”/“旋转”。
在这 8 个中，我们可以安全地消除 7 个，知道如何构建它们，当给定剩余的一个时。

打破对称限制了大小
搜索空间和解空间，我们可以通过使用幻方四个角之间的排序约束来表达它:

magicSquare4x4withRestrictedSymmetries(Zs) :-
    Zs = [S11,_,_,S14,
            _,_,_,_,
            _,_,_,_,
          S41,_,_,S44], 
    S11 #< S14,
    S11 #< S44,
    S11 #< S41,
    S14 #< S41.

这些额外的约束可能会也可能不会帮助我们更快地找到第一个解决方案，但在搜索所有解决方案时它们肯定会有所帮助。

首先，让我们在没有打破对称性的额外约束的情况下进行:

?- time((findall(t,(magicSquare4x4_withSum(Zs,34),
                    labeling([ff],Zs)),Ts),
         length(Ts,N_Sols))).
% 1,526,766,108 inferences, 152.1 CPU in 152.1 seconds (100% CPU, 10033768 Lips)
Ts = [t, t, t, t, t, t, t, t, t|...],
N_Sols = 7040.

现在，有了额外的约束:

?- time((findall(t,(magicSquare4x4_withSum(Zs,34),
                    magicSquare4x4withRestrictedSymmetries(Zs),
                    labeling([ff],Zs)),Ts),
         length(Ts,N_Sols))).
% 129,527,384 inferences, 12.580 CPU in 12.578 seconds (100% CPU, 10295893 Lips)
Ts = [t, t, t, t, t, t, t, t, t|...],
N_Sols = 880.

大赢! 搜索所有解决方案的速度提高了 10 倍以上。正如预期的那样，当打破对称性 (880 * 8 = 7040) 时，解的数量正好除以 8。哼!