MiniZinc中all_equal接收var opt int数组报错问题求助

问题描述 #

编写MiniZinc数独代码时碰到类型错误：提示找不到签名为all_equal(array[int] of var opt int)的函数或谓词。第一段代码调用all_equal能正常运行，但第二段及带完整数独约束的代码里调用该函数就触发错误。疑惑点：

• 为什么传入的参数类型是var opt int而非预期的var int
• 替换成all_different就能正常运行
  需求是生成主对角线对称且对称映射恒定的有效数独网格。

第一段可运行代码 #

include "all_different.mzn";
include "all_equal.mzn";

int: DIMENSION = 3;
int: MAX_DIGIT = DIMENSION * DIMENSION;
set of int: DIGIT_RANGE = 1..MAX_DIGIT;
set of int: POS_LINEAR_RANGE = 1..MAX_DIGIT*MAX_DIGIT;
array[DIGIT_RANGE, DIGIT_RANGE] of var DIGIT_RANGE: grid;

% constraint rows
constraint forall(i in DIGIT_RANGE) (
  all_equal([grid[i, j] | j in DIGIT_RANGE])
);

第二段报错代码 #

include "all_different.mzn";
include "all_equal.mzn";

int: DIMENSION = 3;
int: MAX_DIGIT = DIMENSION * DIMENSION;
set of int: DIGIT_RANGE = 1..MAX_DIGIT;
set of int: POS_RANGE = 1..MAX_DIGIT;
set of int: POS_LINEAR_RANGE = 1..MAX_DIGIT*MAX_DIGIT;
array[DIGIT_RANGE, DIGIT_RANGE] of var DIGIT_RANGE: grid;

% get x, y from a 1..81 position representation
function POS_RANGE: pos_x(int: n) = (n-1) div MAX_DIGIT + 1;
function POS_RANGE: pos_y(int: n) = (n-1) mod MAX_DIGIT + 1;

% foreach digit have a map of its positions on the grid
array[DIGIT_RANGE] of var set of POS_LINEAR_RANGE: positions;
% all positions in the set of positions for a digit corresponds to the
% same digit
constraint forall(i in DIGIT_RANGE) (
  %all_equal([grid[i, j] | j in DIGIT_RANGE])
  all_equal([grid[pos_x(pos), pos_y(pos)] | pos in positions[i]])
);

完整数独约束代码 #

int: DIMENSION = 3;
int: MAX_DIGIT = DIMENSION * DIMENSION;
set of int: DIGIT_RANGE = 1..MAX_DIGIT;
set of int: POS_RANGE = 1..MAX_DIGIT;
set of int: POS_LINEAR_RANGE = 1..MAX_DIGIT*MAX_DIGIT;
array[DIGIT_RANGE, DIGIT_RANGE] of var DIGIT_RANGE: grid;

include "all_different.mzn";
include "all_equal.mzn";

% constraint rows
constraint forall(i in DIGIT_RANGE) (
  all_different([grid[i, j] | j in DIGIT_RANGE])
);

% constraint cols
constraint forall(j in DIGIT_RANGE) (
  all_different([grid[i, j] | i in DIGIT_RANGE])
);

% constraint blocks
array[DIGIT_RANGE] of DIGIT_RANGE: first_j = [3 * ((block_n-1) mod 3)+1 | block_n in DIGIT_RANGE ];
array[DIGIT_RANGE] of DIGIT_RANGE: first_i = [3 * ((block_n-1) div 3)+1 | block_n in DIGIT_RANGE ];
constraint forall(block_n in DIGIT_RANGE) (
  all_different(
    [grid[i, j] | i in first_i[block_n]..first_i[block_n]+2, j in first_j[block_n]..first_j[block_n]+2]
  )
);

% get x, y from a 1..81 position representation
function POS_RANGE: pos_x(POS_LINEAR_RANGE: n) = (n-1) div MAX_DIGIT + 1;
function POS_RANGE: pos_y(POS_LINEAR_RANGE: n) = (n-1) mod MAX_DIGIT + 1;

% foreach digit have a map of its positions on the grid
array[DIGIT_RANGE] of var set of POS_LINEAR_RANGE: positions;
% all positions in the set of positions for a digit corresponds to that
% digit
constraint forall (i in DIGIT_RANGE) (
  forall(pos in positions[i]) (
    grid[pos_x(pos), pos_y(pos)] = i
  )
);
% the positions of a digit are a complete set of that digit's positions
% (cardinal is 9)
constraint forall (i in DIGIT_RANGE) (
  card(positions[i]) = MAX_DIGIT
);
% actual restriction: for each position for a digit, symmetric position
% has to always be the same digit
constraint forall (i in DIGIT_RANGE) (
  all_equal([grid[pos_y(pos), pos_x(pos)] | pos in positions[i]])
);

solve satisfy;

错误原因分析 #

核心问题出在可变集合的遍历类型：

• 第一段代码里，[grid[i,j] | j in DIGIT_RANGE]遍历的是固定整数集合，生成的数组类型是array[int] of var int，完全匹配all_equal的标准签名。
• 第二段和完整代码里，[grid[pos_x(pos), pos_y(pos)] | pos in positions[i]]遍历的是var set of POS_LINEAR_RANGE（可变集合，元素是变量），MiniZinc会自动将这类数组的元素标记为var opt int——因为求解器在预处理阶段无法确定集合里的所有元素是否存在，所以用可选类型表示可能的缺失。
• 标准库的all_different函数支持opt类型的输入，但all_equal只接受非可选的变量类型，因此触发找不到匹配签名的错误。

修正方案 #

方案1：直接定义对称映射（推荐） #

不需要用可变集合关联数字和位置，直接通过全局对称约束实现需求：

1. 定义一个恒定的对称映射数组sym_map，每个数字对应一个固定的对称目标数字
2. 约束所有位置(x,y)满足grid[y,x] = sym_map[grid[x,y]]
3. 保证sym_map是双射，避免映射冲突

修正后的完整代码

int: DIMENSION = 3;
int: MAX_DIGIT = DIMENSION * DIMENSION;
set of int: DIGIT_RANGE = 1..MAX_DIGIT;
set of int: POS_RANGE = 1..MAX_DIGIT;
array[DIGIT_RANGE, DIGIT_RANGE] of var DIGIT_RANGE: grid;

% 定义对称映射：每个数字映射到另一个数字（恒定双射）
array[DIGIT_RANGE] of var DIGIT_RANGE: sym_map;
constraint all_different(sym_map);
% 可选：保证对称映射是自反的，即sym_map[sym_map[i]] = i
constraint forall(i in DIGIT_RANGE) (sym_map[sym_map[i]] = i);

include "all_different.mzn";

% 数独基础约束：行唯一
constraint forall(i in DIGIT_RANGE) (
  all_different([grid[i, j] | j in DIGIT_RANGE])
);

% 数独基础约束：列唯一
constraint forall(j in DIGIT_RANGE) (
  all_different([grid[i, j] | i in DIGIT_RANGE])
);

% 数独基础约束：3x3块唯一
array[DIGIT_RANGE] of DIGIT_RANGE: first_j = [3 * ((block_n-1) mod 3)+1 | block_n in DIGIT_RANGE ];
array[DIGIT_RANGE] of DIGIT_RANGE: first_i = [3 * ((block_n-1) div 3)+1 | block_n in DIGIT_RANGE ];
constraint forall(block_n in DIGIT_RANGE) (
  all_different(
    [grid[i, j] | i in first_i[block_n]..first_i[block_n]+2, j in first_j[block_n]..first_j[block_n]+2]
  )
);

% 核心对称约束：每个位置的对称位置值等于当前值的映射
constraint forall(x in DIGIT_RANGE, y in DIGIT_RANGE) (
  grid[y, x] = sym_map[grid[x, y]]
);

solve satisfy;

方案2：保留原positions集合的修正 #

如果坚持使用原有的positions集合逻辑，直接替换all_equal为明确的约束：利用已有的grid[pos_x(pos), pos_y(pos)] = i约束，直接指定所有对称位置的值为同一个固定变量：

% 保留原有数独基础约束、positions定义及相关约束...

% 为每个数字定义其对称映射的目标数字
array[DIGIT_RANGE] of var DIGIT_RANGE: sym_digit;
constraint all_different(sym_digit);

% 约束：数字i的所有对称位置的值都是sym_digit[i]
constraint forall(i in DIGIT_RANGE) (
  forall(pos in positions[i]) (
    grid[pos_y(pos), pos_x(pos)] = sym_digit[i]
  )
);

% 可选：保证对称映射的双向性
constraint forall(i in DIGIT_RANGE) (
  sym_digit[sym_digit[i]] = i
);

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