如何最大化大于 32 位的 var int？

Question

我正在使用带有内置 Gecode 6.1.1 的 minizinc，我想最大化一个 objective 函数，其值远大于 max int 32。 32 位整数的最大值为 2147483646。虽然与 the reference of minizinc 中的整数最大值相关的信息似乎不多。但是下面的测试表明 Minizinc 使用 32 位整数。

测试很简单，就是尝试最大化一个var int。

var int: maxInt;
constraint maxInt>0;

solve maximize maxInt;

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

结果是

maxInt = 2147483646

结果接近最大 int32 值，而且 miniZinc 似乎无法 "maximize" 更进一步。下面的例子returns一个奇怪的错误。

var int: maxInt;
constraint maxInt>2147483646;

solve maximize maxInt;

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

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

Error: invalid integer literal in line no. 2 Error: syntax error, unexpected ',' in line no. 2 Process finished with non-zero exit code 1

我的问题如下：我可以在 minizinc 中使用 int64 位整数或任何其他大整数表示吗？如果可以，如何使用？（不能使用浮点数）理想情况下，我想举一些例子来说明如何使用

最大化某些东西

constraint maxLargeInt>2147483647;

Answer 1

这里的限制并不是真正的 MiniZinc，而是求解器。正如文档所述（来自 link 关于你引用的整数，我的重点）：

Overview. Integers represent integral numbers. Integer representations are implementation-defined. This means that the representable range of integers is implementation-defined. However, an implementation should abort at run-time if an integer operation overflows.

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

地理编码：2147483646
PicatSAT：72057594037927935 (2^54)
大笑：500000000

Answer 2

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

示例：

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;
----------
=========

请注意，求解器知道目标实际上是无界的，并且会通过消息发出警告。然后打印一个模型，其中 objective 函数是 "large enough" 无穷大的代表值，在本例中为 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;
----------
=========

如何最大化大于 32 位的 var int？

How to maximize a var int that is larger than 32 bits?

optimization

minizinc

gecode

optimathsat