如何处理或避免MiniZinc填字网格模型中的非固定变量

我用MiniZinc构建了一个填字游戏布局模型，核心是把字符序列（单词）放到网格上，决策变量是每个单词的起始位置和方向（上下左右或对角线），网格单元格的字符值是次要变量。

以单词“grows”和“drop”放在4×5网格为例，期望的解形式如下：

d
grows
 o
 p

 p
grows
 r
 d

注：字母按字母表顺序编码为数字。

现在的问题是：解中被单词占用的单元格值是固定的，但未被占用的单元格变量处于非固定状态，导致大量无效解，干扰有效解筛选。我试过把空白单元格赋值为0的最小化方法，但这种方法会优先选择高值符号重叠的解，不符合需求。

以下是用单词“edge”和“egg”（可在e和g处重叠）的复现代码：

% minrep.mzn
int: mrows = 3 ;
int: ncols = 4 ;

int: nwords = 2 ;
int: nletters = 7 ;

array[1..nwords] of int: wordstart = [1, 5] ;
array[1..nwords] of int: wordlength = [4,3] ;

% only two words: 'edge' and 'egg';

array[1..nletters] of int: wordletternumbers = [e, d, g, e, e, g, g ] ;

int: a =  1; int: b =  2; int: c =  3; int: d =  4; int: e =  5; int: f =  6; int: g =  7;

int: numletters = 8 ;  % the length of this truncated "alphabet"

array[1..numletters] of string: letters = ["a", "b", "c", "d", "e", "f", "g", "h" ] ;

% decision variables, the primary unknowns
array[1..nwords, 1..2] of var 1..max(mrows,ncols): rowcolofwi ;

% secondary unkowns: letter numbers in the cells
array[1..mrows, 1..ncols] of var 1..numletters: letternumberofrc ;

constraint forall (ll in 0..(-1+wordlength[1]))
( letternumberofrc[ rowcolofwi[1,1], rowcolofwi[1,2]+ll] = wordletternumbers[wordstart[1]+ll] ) ;

constraint forall (ll in 0..(-1+wordlength[2]))
( letternumberofrc[ rowcolofwi[2,1]+ll, rowcolofwi[2,2]] = wordletternumbers[wordstart[2]+ll] ) ;

%constraint letternumberofrc[2,1] = e ; % this forces 'edge' into the second row
%constraint letternumberofrc[3,1] = e ; % this forces 'edge' into the third row

solve satisfy ;

output [ "  " ++ if is_fixed(letternumberofrc[rr,cc]) then letters[fix(letternumberofrc[rr,cc])] else "."  endif ++
" " ++ if cc < ncols then "" else "\n" endif  | rr in 1..mrows , cc in 1..ncols ]++ ["\n"] ;

请问该如何处理这些非固定变量？

方法1：固定空白单元格为特定值（推荐） #

调整单元格变量的取值范围，加入代表空白的固定值（比如0），然后约束所有未被单词占用的单元格必须等于该空白值。这样所有单元格变量都会被固定，彻底避免无效解。

修改步骤：

• 将letternumberofrc的域从1..numletters改为0..numletters，用0代表空白
• 添加核心约束：明确每个单元格要么被某个单词的字符覆盖，要么为0
• 调整输出逻辑，把0映射为空白字符串

修改后的代码示例：

% minrep.mzn
int: mrows = 3 ;
int: ncols = 4 ;

int: nwords = 2 ;
int: nletters = 7 ;

array[1..nwords] of int: wordstart = [1, 5] ;
array[1..nwords] of int: wordlength = [4,3] ;

% only two words: 'edge' and 'egg';

array[1..nletters] of int: wordletternumbers = [e, d, g, e, e, g, g ] ;

int: a =  1; int: b =  2; int: c =  3; int: d =  4; int: e =  5; int: f =  6; int: g =  7;

int: numletters = 8 ;  % the length of this truncated "alphabet"
int: blank = 0; % 定义空白值

array[0..numletters] of string: letters = ["", "a", "b", "c", "d", "e", "f", "g", "h" ] ; % 索引0对应空白字符串

% decision variables, the primary unknowns
array[1..nwords, 1..2] of var 1..max(mrows,ncols): rowcolofwi ;

% secondary unkowns: letter numbers in the cells (0代表空白)
array[1..mrows, 1..ncols] of var 0..numletters: letternumberofrc ;

% 约束第一个单词的位置和字符
constraint forall (ll in 0..(-1+wordlength[1]))
( letternumberofrc[ rowcolofwi[1,1], rowcolofwi[1,2]+ll] = wordletternumbers[wordstart[1]+ll] ) ;

% 约束第二个单词的位置和字符
constraint forall (ll in 0..(-1+wordlength[2]))
( letternumberofrc[ rowcolofwi[2,1]+ll, rowcolofwi[2,2]] = wordletternumbers[wordstart[2]+ll] ) ;

% 核心约束：所有未被单词占用的单元格必须为空白值0
constraint forall(rr in 1..mrows, cc in 1..ncols) (
    letternumberofrc[rr,cc] = blank
    \/ exists(w in 1..nwords, ll in 0..(-1+wordlength[w])) (
        % 判断当前单元格是否属于单词w的位置范围
        (w == 1 /\ rr == rowcolofwi[1,1] /\ cc == rowcolofwi[1,2] + ll)
        \/ (w == 2 /\ rr == rowcolofwi[2,1] + ll /\ cc == rowcolofwi[2,2])
    )
);

solve satisfy ;

output [ "  " ++ letters[fix(letternumberofrc[rr,cc])] ++
" " ++ if cc < ncols then "" else "\n" endif  | rr in 1..mrows , cc in 1..ncols ]++ ["\n"] ;

方法2：去除次要变量，直接通过决策变量生成输出 #

如果不需要单元格变量存储值，可以直接通过单词的起始位置和方向，在输出阶段计算每个单元格是否被占用，完全避免非固定变量的问题。这种方法适合只需要输出网格布局的场景。

方法3：调整最小化目标（若需要优先重叠解） #

如果仍想用最小化方法，但不想优先高值符号重叠，可以修改目标函数，比如最小化空白单元格的数量，或者最大化单词重叠的字符数：

% 最大化重叠字符数
solve maximize sum(rr in 1..mrows, cc in 1..ncols) (
    count([letternumberofrc[rr,cc] == wordletternumbers[k] | k in 1..nletters], true) > 1 ? 1 : 0
);

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