MiniZinc派生枚举问题：如何简化变长算术谜的数据格式？

针对你扩展MiniZinc密码算术模型时遇到的类型不匹配问题，这里提供几种无需繁琐构造函数的优化方案：

方案1：统一枚举类型，用特殊枚举值表示零 #

不需要单独定义Letters_or_zero枚举，而是在原Letters枚举中添加一个代表零的特殊值（比如ZERO），这样所有涉及填充的位置直接使用这个枚举值即可，避免跨枚举类型的转换：

enum Letters = {ZERO, S, E, N, D, M, O, R, Y}; % 示例枚举，根据实际单词调整

% 数据声明可直接使用枚举值，无需构造函数
array[1..num_addends, 1..max_length] of Letters = [
  [S, E, N, D],
  [ZERO, M, O, R, E], % 短单词用ZERO填充
  [ZERO, ZERO, M, O, N, E, Y] % 和的位置也统一用ZERO填充对齐
];

这样Firsts、sums、tot都可以统一使用Letters类型，彻底消除类型不匹配问题，同时数据声明保持简洁。

方案2：使用可选类型替代枚举扩展 #

如果不想修改原Letters枚举，可以用MiniZinc的opt Letters类型来表示允许空（零填充）的位置，空值直接用none表示，无需额外构造函数：

enum Letters = {S, E, N, D, M, O, R, Y};

% 用opt Letters类型定义数组，none代表零填充
array[1..num_addends, 1..max_length] of opt Letters = [
  [S, E, N, D, none, none],
  [none, M, O, R, E, none],
  [none, none, M, O, N, E, Y] % 对齐到最长长度
];

% 在约束中处理none值：将none映射为0
constraint forall(i in 1..num_addends, j in 1..max_length) (
  if sums[i,j] is not none then value(sums[i,j]) >= 1 else value(sums[i,j]) = 0 endif
);

这种方式既保留了原Letters枚举的纯净性，又避免了类型转换的繁琐，数据声明中用none代替零填充，直观简洁。

方案3：调整数据结构，按实际长度存储单词 #

如果不想用零填充，可以将每个加数存储为单独的数组（长度可变），然后通过索引计算对齐到最高位：

enum Letters = {S, E, N, D, M, O, R, Y};

% 每个加数是变长数组，无需填充
array[1..num_addends] of array[int] of Letters = [
  [S, E, N, D],
  [M, O, R, E],
  [M, O, N, E, Y]
];

% 计算最长长度
int: max_len = max([length(addend) | addend in addends]);

% 约束中通过偏移计算每一位的数值
constraint forall(pos in 1..max_len) (
  sum(
    if length(addend) >= pos then value(addend[length(addend) - pos + 1]) else 0 endif
    for addend in addends[1..num_addends-1]
  ) + carry_in[pos] = value(addends[num_addends][length(addends[num_addends]) - pos + 1]) + 10 * carry_out[pos]
);

这种方案彻底取消了零填充，数据结构更贴合实际单词长度，同时避免了类型问题，只是约束部分需要额外处理索引偏移，但逻辑清晰。

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