如何在MiniZinc中建模Hitori谜题的连通性约束？

Hitori谜题是n×n网格，填充1到n的数字，部分数字在行/列重复。目标是覆盖部分重复数字，需满足三个核心条件：

• 任意行、列无重复数字；
• 被覆盖单元格不能垂直或水平相邻；
• 未覆盖单元格需通过垂直/水平方向连通（无孤立区域）。

现有MiniZinc模型运行给定数据集时，会生成未覆盖单元格不连通的错误解。当前仅实现了避免单单元格孤岛的初步连通性约束，移除该约束会生成33个含孤立单元格的解。曾考虑用n²×n²马尔可夫转移矩阵建模，但认为这种方式低效且不优雅，现寻求在MiniZinc中正确建模未覆盖单元格连通性约束的方法。

现有MiniZinc模型代码（hitori.mzn） #

% hitori.mzn  

% Given square a grid of sidelength n
% The grid is filled with numbers 1..n, some of them repeated in rows and/or columns
% Goal: Cover some of the repeated numbers so that
% i)    there are no duplicates in any row of column
% ii)   no covered square is vertically of horizontally adjacent to another coverde square
% iii)  the uncovered blocks are connected 

% data instance defined in *.dzn 
int: nsize ;
array[SDX,SDX] of SDX: hitoritabl ;

set of int: SDX = 1..nsize ;
set of int: SDX0 = 0..nsize ;  
set of int: SDX2 = 2..nsize ;

% primary unknowns, 0 or 1 whether whether a square is covered or open
array[SDX,SDX] of var 0..1 : hitorimask ;

% modelling variable to display the solution, 0 is used to indicate a covered cell, ie a blacked cell
array[SDX,SDX] of var SDX0: hitorisoln ;
constraint forall( ir in SDX, jc in SDX ) ( hitorisoln[ir,jc] = hitorimask[ir,jc] * hitoritabl[ir,jc] ) ;

% model constraints

% use primary variables to construct quantity on which nonrepeat constraint can be imposed
include "alldifferent_except_0.mzn" ; 
constraint forall ( ir in SDX) ( alldifferent_except_0 ( [ hitorisoln[ir,jc]| jc in SDX ] ) ) ;  % no repeats in a row
constraint forall ( jc in SDX) ( alldifferent_except_0 ( [ hitorisoln[ir,jc]| ir in SDX ] ) ) ;  % no repeats in a column

% impose condition on non-adjacent masked cells
% no black square directly below anothe black square
constraint forall (ir in SDX2, jc in SDX) ( 0 < hitorimask[ir-1,jc] + hitorimask[ir,jc] ) ;
% no black square directly to the right of anothe black square
constraint forall (ir in SDX, jc in SDX2) ( 0 < hitorimask[ir,jc-1] + hitorimask[ir,jc] ) ;

% this constraint simply excludes islands of singleton open cells
constraint forall (ir in SDX, jc in SDX) 
           ( if hitorimask[ir,jc]=1 then 
                ( if ir > 1     then hitorimask[ir-1,jc  ] else 0 endif 
                + if jc < nsize then hitorimask[ir  ,jc+1] else 0 endif
                + if ir < nsize then hitorimask[ir+1,jc  ] else 0 endif
                + if jc > 1     then hitorimask[ir  ,jc-1] else 0 endif
                 > 0 
                )
             endif ) ;

%
% still need a condition of connectedness of open squares
%

solve satisfy ;

output ["\nhitorimask           hitorisoln \n" ] ;
output [ 
         if jc <= nsize then "" ++ show_int(3, hitorimask[ir,jc] ) else "" endif
      ++ if jc = nsize then "   " else "" endif 
      ++ if nsize < jc /\ jc <= 2*nsize 
         then if fix(hitorisoln[ir,jc-nsize])>0 
              then show_int(3, hitorisoln[ir,jc-nsize] )  
              else "  ." 
              endif  
         else "" 
         endif 
      ++ if jc = 2*nsize then "\n" else "" endif
      | ir in SDX, jc in 1..2*nsize ] ;

数据集代码（hitori.dzn） #

% hitori.dzn
nsize = 5 ;   % size of square grid

hitoritabl = [|
4, 5, 4, 4, 3 |
4, 2, 5, 1, 3 |
5, 1, 1, 3, 4 |
5, 4, 2, 5, 2 |
2, 1, 4, 3, 1 |] ;

解决方案：建模未覆盖单元格的全局连通性 #

在MiniZinc中实现全局连通性，最实用且高效的方式是基于可达性的传递闭包建模，具体实现步骤如下：

1. 添加可达性变量与根节点约束 #

引入二维布尔数组reachable表示单元格是否从某个未覆盖的根节点可达，同时定义根节点变量确保存在起始连通点：

array[SDX, SDX] of var bool: reachable;
var SDX: root_i;
var SDX: root_j;

% 选择一个未覆盖单元格作为连通起点
constraint hitorimask[root_i, root_j] = 1;
constraint reachable[root_i, root_j] = true;

2. 约束可达性的传递关系 #

如果某个单元格可达且未被覆盖，那么它的相邻未覆盖单元格也必须可达：

constraint forall(i in SDX, j in SDX) (
    if reachable[i,j] then
        % 上邻单元格连通传递
        (i > 1 /\ hitorimask[i-1,j] = 1) -> reachable[i-1,j]
        /\
        % 下邻单元格连通传递
        (i < nsize /\ hitorimask[i+1,j] = 1) -> reachable[i+1,j]
        /\
        % 左邻单元格连通传递
        (j > 1 /\ hitorimask[i,j-1] = 1) -> reachable[i,j-1]
        /\
        % 右邻单元格连通传递
        (j < nsize /\ hitorimask[i,j+1] = 1) -> reachable[i,j+1]
    endif
);

3. 强制所有未覆盖单元格可达 #

确保所有未被覆盖的单元格都能从根节点到达：

constraint forall(i in SDX, j in SDX) (
    hitorimask[i,j] = 1 -> reachable[i,j]
);

修改后的完整模型 #

将上述代码添加到原模型中% still need a condition of connectedness of open squares注释的位置即可。原有的单单元格孤岛约束可以保留，作为前置剪枝条件提升求解效率。

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