MiniZinc五联骨牌regular约束示例工作原理及技术问询

首先先把示例数据和求解代码整理如下：

示例数据 #

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,]

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)];

1. 该示例的目标是什么？为何看似需要骨牌重叠或排除？ #

这个示例的核心目标是在5×4的棋盘上，用编号1-5的5个五联骨牌（每个占5个格子）完全覆盖棋盘的前4列区域，同时骨牌之间不能重叠。而棋盘的最后一列被预先标记为排除区域（不能放置任何骨牌）。

你觉得“需要重叠或排除”的原因是：代码里明确约束了最后一列的所有格子必须等于ntiles+1（也就是6），这部分是强制排除的不可用区域；同时通过regular约束确保每个骨牌的形状符合要求，而骨牌的编号在棋盘里是互斥的（每个格子只能属于一个骨牌或排除区域），所以不存在重叠——只是排除区域的存在让可用空间看起来和骨牌总格子数有差异，实际是DFA约束会自动筛选出符合空间要求的骨牌放置方式。

2. MiniZinc中五联骨牌的tile和dfa表示如何工作？ #

这是用确定性有限自动机（DFA）编码骨牌形状的经典方法，具体逻辑如下：

• tile（骨牌参数）：每个tile是一个五元素数组，对应DFA的核心参数：
  • Q：DFA的状态总数；
  • S：输入符号的数量（对应棋盘的可能取值：1-5是骨牌编号，6是排除区域）；
  • Fstart到Fend：DFA的接受状态范围（骨牌形状放置完成时的状态）；
  • Dstart：该骨牌的DFA转移表在全局dfa数组中的起始索引。
• dfa（转移表）：全局dfa数组是所有骨牌DFA转移表的集合，每个骨牌的转移表是一个Q×S的二维数组，其中每个元素表示“当前状态下，输入某个符号（棋盘格子的值）后转移到的下一个状态”。
• regular约束：对每个骨牌t，regular(board, q, s, d, 1, f)会检查按行优先遍历的棋盘序列中，所有标记为t的格子组成的模式是否符合该骨牌的DFA规则——确保这些格子是连通的、符合五联骨牌的形状，最终进入接受状态。

3. 该表示中五联骨牌的旋转与镜像如何实现？ #

旋转和镜像的变体是直接编码在DFA的转移逻辑里的：在构建DFA的时候，已经把该骨牌所有可能的旋转（0°、90°、180°、270°）和镜像（左右/上下翻转）后的有效形状都包含进去了。这样regular约束就能自动接受任何这些变体的放置方式，不需要额外编写旋转/镜像的处理代码，DFA会负责识别所有合法的形状变体。

4. 求解结果中的数字6代表什么含义？ #

数字6代表预先定义的排除区域——也就是棋盘的最后一列（宽度为5，第5列）的所有格子，这些格子不允许放置任何骨牌，是强制留空的区域，对应代码里的约束：

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

这里ntiles=5，所以ntiles+1=6，直接把最后一列的所有格子设为6。

内容的提问来源于stack exchange，提问作者makeyourownmaker