时间戳

首页 > 解决方案 > minizinc pentominoes 常规约束示例如何工作？

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

问题描述

minizinc基准存储库包含几个pentomino 示例。

这是第一个示例的数据：

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 溶液：

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 挑战的一部分，但现在不再是了。

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

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

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

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

minizinc pentomino 瓷砖和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。它们代表什么？

请参阅此网页以获取完整的 50、5 x 4无重叠、排除或孔洞的五联拼板。

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

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

标签： regexdfaminizincsattiling

解决方案

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

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

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

_ _ _ _
_ _ XX
XX _ _
_ _ _ _

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

如果您觉得这很有趣，我还有其他 几篇使用类似的放置部件结构的论文以及原始出版物。

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

推荐阅读