如何在MiniZinc中创建网格连通性约束（Nurikabe求解器场景）

需求说明 #

给定N×N网格，每个单元格为「水域」或「陆地」，需要完成两个核心功能：

• 为每个陆地单元格统计其所在连通块的陆地总数
• 判断任意两个陆地单元格是否连通（用于Nurikabe求解器）

示例 #

输入网格（0=陆地，1=水域）：

0 0 0 0 1
1 0 0 1 1
1 0 0 0 0
0 0 1 1 0

期望输出（每个陆地单元格对应其所在连通块的大小，水域单元格为0）：

0 0 0 0 3
2 0 0 3 3
2 0 0 0 0
0 0 2 2 0

现有代码问题 #

你提供的代码中，is_connected函数仅判断两个单元格是否为陆地，未考虑实际连通性；岛屿大小的计算逻辑也仅统计所有陆地单元格数量，无法区分不同连通块。

正确实现方案 #

MiniZinc作为约束编程语言，不适合用普通递归函数遍历连通块，需通过等价类约束（给同一连通块分配相同ID）来表达连通关系，以下是完整实现：

完整代码 #

int: L = 4; % 列数
int: H = 5; % 行数

% 输入网格：0=陆地，1=水域
array[1..L, 1..H] of int: puzzle = [
    [0,0,0,0,1],
    [1,0,0,1,1],
    [1,0,0,0,0],
    [0,0,1,1,0]
];

% 存储每个单元格的岛屿大小
array[1..L, 1..H] of var 0..L*H: island_sizes;

% 标记所有陆地单元格
set of pair: land_cells = {(i,j) | i in 1..L, j in 1..H where puzzle[i,j] == 0};

% 给每个单元格分配连通块ID：水域为-1，陆地为非负整数，同一连通块ID相同
array[1..L, 1..H] of var -1..card(land_cells): component_id;

% 水域单元格的约束：ID为-1，岛屿大小为0
constraint forall(i in 1..L, j in 1..H where puzzle[i,j] == 1) (
    component_id[i,j] == -1 /\ island_sizes[i,j] == 0
);

% 陆地单元格的连通性约束：四连通的陆地必须属于同一连通块
constraint forall(i in 1..L, j in 1..H where puzzle[i,j] == 0) (
    component_id[i,j] >= 0
    % 上方相邻
    /\ (i > 1 /\ puzzle[i-1,j] == 0) -> component_id[i,j] == component_id[i-1,j]
    % 下方相邻
    /\ (i < L /\ puzzle[i+1,j] == 0) -> component_id[i,j] == component_id[i+1,j]
    % 左方相邻
    /\ (j > 1 /\ puzzle[i,j-1] == 0) -> component_id[i,j] == component_id[i,j-1]
    % 右方相邻
    /\ (j < H /\ puzzle[i,j+1] == 0) -> component_id[i,j] == component_id[i,j+1]
);

% 根据连通块ID计算岛屿大小：同一ID的单元格大小相同，等于该块的陆地总数
constraint forall(c in 0..card(land_cells)-1) (
    let {
        int: block_size = sum(i in 1..L, j in 1..H where puzzle[i,j] == 0) (
            bool2int(component_id[i,j] == c)
        )
    } in
    forall(i in 1..L, j in 1..H where puzzle[i,j] == 0) (
        component_id[i,j] == c -> island_sizes[i,j] == block_size
    )
);

% 判断两个单元格是否连通的函数
function var bool: is_connected(int: x1, int: y1, int: x2, int: y2) =
    % 若任意一个是水域则不连通，否则判断是否属于同一连通块
    (puzzle[x1,y1] == 1 \/ puzzle[x2,y2] == 1) ? false : (component_id[x1,y1] == component_id[x2,y2]);

% 求解并输出结果
solve satisfy;

output [
    if j == 1 then "\n" else " " endif ++ show(island_sizes[i,j])
    | i in 1..L, j in 1..H
];

关键说明 #

1. 连通块ID机制：通过component_id数组给同一连通块的陆地单元格分配相同ID，水域单元格ID设为-1，以此区分不同岛屿。
2. 四连通约束：代码中仅检查上下左右四个方向的相邻单元格，符合Nurikabe的规则；若需八连通，可添加对角线相邻的检查逻辑。
3. 岛屿大小计算：遍历每个连通块ID，统计对应ID的陆地单元格数量，再将该值赋值给块内所有单元格。
4. 连通性判断函数：通过对比两个单元格的component_id是否相等来判断是否连通，同时处理水域的特殊情况。

简化方案（依赖求解器支持） #

部分MiniZinc求解器（如Gecode、Chuffed）内置了connected约束，可替代手动构建连通块ID的逻辑，简化代码：

% 替换手动连通性约束的部分
constraint connected(
    [i | (i,j) in land_cells],
    [j | (i,j) in land_cells],
    [(i1,j1,i2,j2) | (i1,j1) in land_cells, (i2,j2) in land_cells where abs(i1-i2)+abs(j1-j2) == 1]
);

但此方式兼容性较差，若需跨求解器运行，建议使用手动构建的等价类约束。

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