Minizinc字谜模型中至多k与至少k约束的优化实现问询

一、至多k个指定单词组合出现的高效实现 #

最简洁且利于求解器传播的方式是利用MiniZinc的sum约束结合布尔表达式，这种写法能让求解器快速剪枝无效解，提升运行效率。

实现步骤 #

1. 先为每个目标单词定义布尔变量，标记该单词是否出现在网格中：

% 固定中间单元格为不可赋值（示例设为空格，若单词需用到固定字符可替换）
constraint grid[2,2] = ' ';

% 定义各目标单词的存在条件
var bool: has_axe = (grid[1,1] = 'a' /\ grid[1,2] = 'x' /\ grid[1,3] = 'e');
var bool: has_ace = (grid[1,1] = 'a' /\ grid[1,2] = 'c' /\ grid[1,3] = 'e');
var bool: has_ero = (grid[1,2] = 'e' /\ grid[3,2] = 'o'); % 适配中间单元格不可赋值的场景
var bool: has_evo = (grid[1,2] = 'e' /\ grid[3,2] = 'o');

2. 直接对布尔变量求和，添加至多k的约束：

int: k; % 自定义参数，如k=2
constraint sum([has_axe, has_ace, has_ero, has_evo]) <= k;

如果不想单独定义布尔变量，也可以直接在sum中嵌入表达式，代码更紧凑：

constraint sum([
    (grid[1,1] = 'a' /\ grid[1,2] = 'x' /\ grid[1,3] = 'e'),
    (grid[1,1] = 'a' /\ grid[1,2] = 'c' /\ grid[1,3] = 'e'),
    (grid[1,2] = 'e' /\ grid[3,2] = 'o'),
    (grid[1,2] = 'e' /\ grid[3,2] = 'o')
]) <= k;

二、至少k个指定单词组合出现的实现 #

逻辑与至多k约束对称，同样使用sum约束，仅调整不等式方向：

实现步骤 #

1. 复用上述布尔变量或表达式定义；
2. 添加求和大于等于k的约束：

constraint sum([has_axe, has_ace, has_ero, has_evo]) >= k;

或直接嵌入表达式的写法：

constraint sum([
    (grid[1,1] = 'a' /\ grid[1,2] = 'x' /\ grid[1,3] = 'e'),
    (grid[1,1] = 'a' /\ grid[1,2] = 'c' /\ grid[1,3] = 'e'),
    (grid[1,2] = 'e' /\ grid[3,2] = 'o'),
    (grid[1,2] = 'e' /\ grid[3,2] = 'o')
]) >= k;

批量单词场景优化 #

若目标单词数量较多，可通过循环批量生成存在条件，减少重复代码：

% 存储目标单词的位置与字符序列
array[1..4] of tuple((int, int), string): target_words = [
    ((1,1), "axe"),   % 第1行起始的横向单词
    ((1,1), "ace"),
    ((1,2), "ero"),   % 第2列起始的纵向单词（适配中间单元格不可赋值）
    ((1,2), "evo")
];

% 批量生成单词存在的布尔变量
array[1..4] of var bool: has_word = [
    grid[start_row, start_col] = word[1] /\ 
    grid[start_row, start_col+1] = word[2] /\ 
    grid[start_row, start_col+2] = word[3]
    where let {
        (start_row, start_col) = target_words[j][1];
        string: word = target_words[j][2];
    } in true for j in 1..4
];

% 至多k约束
constraint sum(has_word) <= k;
% 至少k约束
constraint sum(has_word) >= k;

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