2

我正在使用带有内置 Gecode 6.1.1 的 minizinc，我想最大化一个目标函数，其值远大于 max int 32。32 位整数的最大值是 2147483646。虽然似乎没有太多信息与minizinc 参考中的整数最大值相关。然而，以下测试表明 Minizinc 使用 32 位整数。

测试非常简单，它只是试图最大化一个 var int。

var int: maxInt;
constraint maxInt>0;

solve maximize maxInt;

output ["maxInt = \(maxInt)"];

结果是

最大整数 = 2147483646

结果接近最大 int32 值，并且 miniZinc 似乎无法进一步“最大化”它。以下示例返回一个奇怪的错误。

var int: maxInt;
constraint maxInt>2147483646;

solve maximize maxInt;

output ["maxInt = \(maxInt)"];

错误消息如下。该错误消息的信息量不是很大，但在尝试使用大于 2147483646 的数字时会显示。

错误：行号中的整数文字无效。2 错误：语法错误，行号中出现意外的“，”。2 进程以非零退出代码 1 结束

我的问题如下：我可以将 int64 位整数或任何其他大整数表示与 minizinc 一起使用吗？如果可以，如何？（使用浮点数不是一种选择）理想情况下，我想举一些例子来说明如何最大化某些东西

constraint maxLargeInt>2147483647;
4

2 回答 2

4

这里的限制并不是真正的 MiniZinc，而是求解器。正如文档所述（来自您引用的关于整数的链接，我强调）：

概述。整数代表整数。整数表示是实现定义的。这意味着整数的可表示范围是实现定义的。但是，如果整数运算溢出，实现应该在运行时中止。

以下是maxInt一些求解器在运行测试模型时的解决方案示例（使用约束maxInt > 0）：

  1. 地理编码：2147483646
  2. PicatSAT: 72057594037927935 (2^54)
  3. 大笑：500000000
于 2019-08-07T08:12:46.360 回答
2

您可能还想尝试OptiMathSAT，它有一个FlatZinc接口并且它使用无限精度算术，这意味着它不会产生任何数值限制/不稳定性（以效率为代价）。

例子：

var int: x ;
var int: y ;
constraint y = 2 * x;
solve maximize x;

output [
    "x = " ++ show(x) ++ ";\n" ++
    "y = " ++ show(y) ++ ";\n"
]

编译成

var int: INT____00001 :: is_defined_var :: var_is_introduced;
var int: x :: output_var;
var int: y :: output_var = INT____00001;
constraint int_lin_eq([-1, 2], [INT____00001, x], 0) :: defines_var(INT____00001);
solve maximize x;

这是 OptiMathSAT 的输出：

~$ optimathsat -input=fzn < test.fzn
% objective: x (optimal model)
% warning: x is unbounded: oo
x = 1000000000;
y = 2000000000;
----------
=========

请注意，求解器知道目标实际上是无界的，并通过消息警告它。然后它打印一个模型，其中目标函数是无穷大的“足够大”代表值，在这种情况下是1000000000. 该值实际上可以使用以下选项进行自定义：

~$ optimathsat -input=fzn -opt.theory.la.infinite_pow=18 < test.fzn 
% objective: x (optimal model)
% warning: x is unbounded: oo
x = 1000000000000000000;
y = 2000000000000000000;
----------
=========
于 2019-08-07T08:37:28.950 回答