optimizationminizincgecodeoptimathsat

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


I am using minizinc with built-in Gecode 6.1.1 and I want to maximize an objective function with values that are far greater than the max int 32. The maximum value of an integer with 32 bits is 2147483646. While not much information seems to be available related to the maximum value for integers in the reference of minizinc . However the following test shows that Minizinc uses 32 bit integers.

The test is very simple, it just tries to maximize a var int.

var int: maxInt;
constraint maxInt>0;

solve maximize maxInt;

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

The result is

maxInt = 2147483646

The result is close to the max int32 value and also miniZinc seems to be unable to "maximize" it further. The following example returns a weird error.

var int: maxInt;
constraint maxInt>2147483646;

solve maximize maxInt;

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

The error message is the following. The error message is not very informative but it is shown when trying to use numbers larger than 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

My question is the following: Can I use int64 bit integers or any other large integer representation with minizinc and if yes how? (Using floats is not an option) Ideally I would like to have some example on how to maximize something with

constraint maxLargeInt>2147483647;

Solution

  • It's not really MiniZinc that is the limit here, it's the solver. As the documentation state (from the link about integers you cited, my emphasis):

    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.

    Here are some examples of the solution of maxInt for some solvers when running you test model (using the constraint maxInt > 0):

    1. Gecode: 2147483646
    2. PicatSAT: 72057594037927935 (2^54)
    3. Chuffed: 500000000