来自 var float 的 2D 数组的 MiniZinc 最大值

Question

我正处于学习 MiniZinc 的初级阶段，我想在不看代码的情况下完成 MiniZinc 教程中提供的 laplace.mzn 示例。我最初的尝试（如下面的代码块 1 所示）提供了正确的答案。我想尝试通过在 show_float() 函数中设置硬编码值 6 来概括输出语句，该函数指定输出中的每个浮点数都应该用 6 位动态右对齐（即找到 t 和以此为基础输出宽度。

我的第一次尝试是在代码块 2 中添加语句，但收到以下错误： MiniZinc：评估错误：
laplace.mzn:28:
在“m”的变量声明中
通话中“最大”
/home/str/MiniZinc/share/minizinc/std/builtins.mzn:278:
在 let 表达式中
/home/str/MiniZinc/share/minizinc/std/builtins.mzn:281:
在通话中'max_t'
/home/str/MiniZinc/share/minizinc/std/builtins.mzn:2020:
在 if-then-else 表达式中
/home/str/MiniZinc/share/minizinc/std/builtins.mzn:2023:
在 let 表达式中
/home/str/MiniZinc/share/minizinc/std/builtins.mzn:2025:
在调用'array_float_maximum'
/home/str/MiniZinc/share/minizinc/linear/redefinitions-2.0.mzn:16:
在 if-then-else 表达式中
/home/str/MiniZinc/share/minizinc/linear/redefinitions-2.0.mzn:19:
在调用'array_float_minimum_I'
/home/str/MiniZinc/share/minizinc/linear/redefinitions.mzn:108:
在 let 表达式中
/home/str/MiniZinc/share/minizinc/linear/redefinitions.mzn:110:
i = 1
通话中'ub'
无法确定界限

然后，虽然我对它的外观不满意，但我尝试了 Code Block 3，结果出现以下错误：
MiniZinc：评估错误：
/home/str/MiniZinc/share/minizinc/linear/redefs_lin_reifs.mzn:319:
在 if-then-else 表达式中
/home/str/MiniZinc/share/minizinc/linear/redefs_lin_reifs.mzn:321:
在呼叫“ub”
无法确定界限

在满足约束问题后如何从 't' 中获取最大值有什么建议吗？提前致谢。

代码块 1：

int: w = 5;
int: h = 5;

array[1..h,1..w] of var float: t;
float: top = 100.0;
float: bottom = 0.0;
float: left = 0.0;
float: right = 0.0;
float: corners = 0.0;

% Top row all the same except corners
constraint forall(c in 2..w-1)(t[1,c] = top);

% Bottom row all the same except corners
constraint forall(c in 2..w-1)(t[h,c] = bottom);

% First column all the same except corners
constraint forall(r in 2..h-1)(t[r,1] = left);

% Last column all the same except corners
constraint forall(r in 2..h-1)(t[r,w] = right);

% The four corners must be the same value
constraint t[1,1] = corners /\ t[1,1] = t[1,w] /\ t[1,w] = t[h,w] /\ t[h,w] = t[h,1];

constraint forall( r in 2..h-1, c in 2..w-1)( 4*t[r,c] = t[r-1,c] + t[r+1,c] + t[r,c-1] + t[r,c+1]);

solve satisfy;

output[ show_float(6,2,t[r,c]) ++
        if c = h then "\n" else " " endif
        | r in 1..h, c in 1..w ];

代码块 2：

var float: m = max(r in 1..h, c in 1..w)(t[r,c]);

代码块 3：

% Width of temperature grid
int: w = 5;

% Height of temperature grid
int: h = 5;

array[1..h,1..w] of var float: t;

% Temperature in the top row, bottom row, left row, right row, and corners
float: top = 100.0;
float: bottom = 0.0;
float: left = 0.0;
float: right = 0.0;
float: corners = 0.0;

% Top row all the same except corners
constraint forall(c in 2..w-1)(t[1,c] = top);

% Bottom row all the same except corners
constraint forall(c in 2..w-1)(t[h,c] = bottom);

% First column all the same except corners
constraint forall(r in 2..h-1)(t[r,1] = left);

% Last column all the same except corners
constraint forall(r in 2..h-1)(t[r,w] = right);

% The four corners must be the same value
constraint t[1,1] = corners /\ t[1,1] = t[1,w] /\ t[1,w] = t[h,w] /\ t[h,w] = t[h,1];

constraint forall( r in 2..h-1, c in 2..w-1)( 4*t[r,c] = t[r-1,c] + t[r+1,c] + t[r,c-1] + t[r,c+1]);

% Get the maximum value in t
var float: m;
constraint forall(r in 1..h, c in 1..w)(m >= t[r,c]);
constraint exists(r in 1..h, c in 1..w)(m = t[r,c]);

solve maximize m;

% Wish to replace the value six in the next line with m + 3, where the 3 represents
% character for the 2 digits to the right of a decimal point and 1 character for the
% decimal point
output[ show_float(6,2,t[r,c]) ++
        if c = h then "\n" else " " endif
        | r in 1..h, c in 1..w ];

Answer 1

cannot determine bounds 错误来自 MIP 求解器，我可以看到。这是由模型中将t 和m 定义为var float 引起的。它可以通过这些决策变量的一些修复 - 并且相当小的 - 域来修复。例如

var 0.0..100.0: m;
array[1..h,1..w] of var 0.0..100.0: t;

如果您使用可以将浮点数作为决策变量（例如 Gecode 或 JaCoP）处理的 FlatZinc 求解器运行，则不会引发此错误。但是，Gecode 很慢，因为 t 和 m 两个决策变量被定义为 var float，它们是巨大的域。如果您设置一个特定的 - 并且相当小的 - 域，例如0.0..100.0 然后 Gecode 很快就能解决这个问题。或者至少声明t 和m 应该大于或等于0（因为域远大于0..100，所以速度不快）。请注意，JaCoP 求解器没有这个问题； var float 不是很慢。