minizinc pentominoes 常规约束示例如何工作？

Question

minizinc benchmarks 存储库包含多个 pentomino examples。

这里是data for the first example：

width = 5;
height = 4;
filled = 1;
ntiles = 5;
size = 864;
tiles =  [|63,6,1,2,0,
   |9,6,1,2,378,
   |54,6,1,2,432,
   |4,6,1,2,756,
   |14,6,1,2,780,
   |];
dfa = [7,5,5,5,5,3,0,2,2,2,2,2,7,5,5,5,5,3,19,4,4,4,4,3,30,4,4,4,4,3,0,10,10,10,10,10,46,8,8,8,8,0,0,12,12,12,12,13,0,15,15,15,15,14,0,16,16,16,16,16,0,18,18,18,18,17,0,20,20,20,20,20,0,21,21,21,21,21,0,22,22,22,22,22,0,23,23,23,23,23,0,28,28,28,28,0,47,22,22,22,22,22,47,23,23,23,23,23,46,11,11,11,11,24,0,26,26,26,26,26,0,25,25,25,25,25,0,27,27,27,27,25,0,29,29,29,29,26,0,31,31,31,31,31,32,0,0,0,0,0,33,0,0,0,0,0,34,0,0,0,0,0,35,0,0,0,0,0,36,0,0,0,0,0,46,9,9,9,9,6,47,16,16,16,16,16,0,35,35,35,35,0,60,35,35,35,35,0,0,37,37,37,37,39,0,39,39,39,39,39,60,37,37,37,37,39,0,40,40,40,40,40,0,41,41,41,41,41,0,42,42,42,42,42,0,43,43,43,43,43,0,45,45,45,45,45,0,47,47,47,47,47,60,47,47,47,47,47,48,0,0,0,0,0,49,44,44,44,44,0,53,38,38,38,38,38,60,0,0,0,0,0,0,50,50,50,50,50,0,51,51,51,51,0,0,52,52,52,52,52,0,54,54,54,54,54,0,55,55,55,55,55,0,56,56,56,56,56,0,57,57,57,57,57,0,60,60,60,60,0,0,58,58,58,58,58,0,59,59,59,59,59,61,55,55,55,55,0,62,0,0,0,0,0,63,0,0,0,0,0,0,62,62,62,62,0,0,63,63,63,63,0,0,2,2,2,2,2,3,4,3,3,3,3,2,0,2,2,2,2,3,4,3,3,3,3,5,9,5,5,5,5,6,0,6,6,6,6,7,0,7,7,7,7,8,0,8,8,8,8,0,9,0,0,0,0,2,0,2,2,2,2,4,4,14,4,4,5,2,2,0,2,2,2,3,3,10,3,3,5,3,3,12,3,3,5,4,4,14,4,4,5,8,8,0,8,8,0,9,9,0,9,9,13,11,11,0,11,11,11,11,11,22,11,11,11,7,7,15,7,7,11,13,13,0,13,13,13,6,6,15,6,6,0,0,0,22,0,0,0,6,6,25,6,6,0,17,17,29,17,17,16,19,19,0,19,19,19,20,20,0,20,20,20,21,21,0,21,21,21,22,22,0,22,22,0,23,23,0,23,23,24,24,24,0,24,24,24,26,26,0,26,26,0,26,26,27,26,26,0,0,0,27,0,0,0,18,18,29,18,18,0,0,0,30,0,0,0,28,28,0,28,28,0,30,30,0,30,30,0,32,32,0,32,32,32,33,33,0,33,33,33,34,34,0,34,34,0,35,35,0,35,35,35,36,36,0,36,36,36,0,0,37,0,0,0,31,31,40,31,31,0,0,0,45,0,0,0,39,39,0,39,39,39,41,41,0,41,41,41,42,42,0,42,42,42,43,43,0,43,43,0,44,44,0,44,44,44,45,45,0,45,45,0,38,38,46,38,38,0,0,0,50,0,0,0,0,0,51,0,0,0,47,47,0,47,47,47,49,49,0,49,49,49,51,51,0,51,51,0,48,48,52,48,48,0,0,0,53,0,0,0,0,0,54,0,0,0,53,53,0,53,53,0,54,54,0,54,54,0,2,2,0,2,2,2,3,3,3,4,3,3,2,2,2,0,2,2,3,3,3,4,3,3,2,2,2,0,2,2,3,3,3,3,8,3,2,2,2,2,0,2,3,3,3,3,8,3,5,5,5,5,0,5,6,6,6,6,0,6,7,7,7,7,0,7,0,0,0,0,9,0,4,4,4,4,13,4,10,10,10,10,0,10,11,11,11,11,0,11,12,12,12,12,0,12,13,13,13,13,0,13,0,0,0,0,14,0,2,2,2,2,0,2,]

据我了解，目标是用 5 pentominoes 填充 5 x 4 板。似乎需要一些重叠和/或排除图块，这并不常见。

这里是minizinc solution：

include "globals.mzn";

int: Q = 1;
int: S = 2;
int: Fstart = 3;
int: Fend = 4;
int: Dstart = 5;

int: width;
int: height;
int: filled;
int: ntiles;
int: size;
array[1..ntiles,1..Dstart] of int: tiles;
array[1..size] of int: dfa;

array[1..width*height] of var filled..ntiles+1: board;

constraint forall (h in 1..height, w in 1..width-1) (
    board[(h-1)*width+w] != ntiles+1);

constraint forall (h in 1..height) (
    board[(h-1)*width+width] = ntiles+1);

constraint
  forall (t in 1..ntiles)(
    let {
      int: q = tiles[t,Q],
      int: s = tiles[t,S],
      set of int: f = tiles[t,Fstart]..tiles[t,Fend],
      array[1..q,1..s] of int: d =
        array2d(1..q,1..s,
                [ dfa[i] | i in tiles[t,Dstart]+1..tiles[t,Dstart]+q*s] )
    }
    in
      regular(board,q,s,d,1,f)
  );

solve :: int_search(board, input_order, indomain_min, complete) satisfy;

output [show(board)];

我无法找到有关 minizinc 基准测试的大量文档。他们在minizinc challenge 中加入了几年，但不再是了。

Mikael Lagerkvist's thesis 的第 3 章可能部分相关。它描述了使用regular 约束在gecode 工具包中放置五联骨牌。 第 3.2 节说明了使用 0 和 1s 的正则表达式字符串放置 L pentomino 的字符串表示形式：其中棋盘的每个正方形与 L pentomino 的正方形重叠。 3.3 节使用正则表达式的析取来处理片段旋转。一般来说，每个 pentomino 有 8 个对称性需要考虑（2 个镜像和 4 个旋转）。

上面的 minizinc 数据不使用 8 个二进制字符串的析取来表示 pentomino 拼贴，但 minizinc 代码确实使用了regular 约束。

我意识到 gecode 和 minizinc 的工作方式不同，在这种情况下 minizinc 选择了一种替代方法来替代难以读写的二进制字符串正则表达式析取。 dfa 变量中的 864 长数字串可能是我缺少的 minizinc 解决方案的核心部分。解决方案的其余部分（消除板对称性）我可能会在那之后弄清楚。

我不知道如何在没有重叠和/或排除的情况下用 5 个五联板填充 5 x 4 板。这个例子的目的是什么？

minizinc pentomino tile 和dfa 表示如何工作？

pentomino 旋转和镜像在这个 minizinc 表示中是如何工作的？

这是上面代码中唯一的板子解决方案：

[1, 1, 1, 2, 6, 3, 3, 1, 2, 6, 3, 5, 5, 5, 6, 3, 3, 3, 4, 6]

这是重新格式化为 5 x 4 板的解决方案：

[1, 1, 1, 2, 6, 
 3, 3, 1, 2, 6, 
 3, 5, 5, 5, 6, 
 3, 3, 3, 4, 6]

注意 6s。它们代表什么？

---

参见this web page for the complete set of 50, 5 x 4 pentomino tilings，没有重叠、排除或漏洞。

使用 minizinc 解决此类问题还有其他方法。 geost 谓词是一种可能性。这些替代方案都与此问题无关。

除 minizinc 和 gecode 之外的替代软件建议或讨论再次无关紧要。

Answer 1

原始 MiniZinc 模型和评论中存储库中的模型都是我写的。虽然我的执照论文和链接的存储库使用正则表达式来表达约束，但最初的 MiniZinc 挑战模型是在 MiniZinc 仅支持 DFA 输入时编写的，因为这是求解器内部的正则约束实际使用的 (§)。 DFA 实际上是通过采用 Gecode 模型并编写一个小程序（丢失时间）生成的，该程序使用 Gecode 正则表达式到 DFA 的转换打印出 Gecode 示例文件中正则表达式的 DFA。翻译的一个好处是，对于具有一定对称性的片段，DFA 最小化将消除对称性。链接的实例生成器是今年编写的，它使用了接受正则表达式的现代 MiniZinc 功能。这样写更容易。

因此，为了理解一长串数字，您必须将其视为 DFA。该列表表示一个矩阵，其中索引是状态和下一个输入，值是要进入的下一个状态。正则约束的其他参数表示状态数、字母表中的符号数以及 DFA 的起始和接受状态。

至于矩阵末尾的 6，这些是行尾标记。他们在那里确保一块不会分开。考虑 4 x 4 棋盘上的简单棋子 XXX，没有其他棋子（因此 X 为 1，空为 0）。使用表达式0*1110*，该作品的所有位置都被建模，但是像

这样的位置也是如此 _ _ _ _ _ _ X X X X _ _ _ _ _ _

为了避免这种情况，在板中添加了一个额外的行尾列。在这种特殊情况下，行尾标记是它自己的唯一值，这意味着模型甚至可以处理不相交的片段。如果所有棋子都已连接且棋盘未满，则行尾标记可能与空方格相同。

我有几个otherpapers，如果您觉得这很有趣，它们使用类似的放置部件结构，还有original publication。

脚注：(§) 从技术上讲，Pesant 算法的大多数直接实现也可以处理 NFA（忽略 epsilon 转换），这可用于优化表示。然而，DFA 最小化是一种已知且快速的方法，而 NFA 最小化要困难得多。 FA 中的状态越少，传播速度就越快。