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

Question

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;

Answer 1

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

Answer 2

You may also want to try OptiMathSAT, it has a FlatZinc interface and it uses infinite precision arithmetic, meaning that it does not incur in any numerical limit/instability (at the cost of efficiency).

---

Example:

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

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

compiles into

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;

this is the output of OptiMathSAT:

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

Notice that the solver knows that the goal is actually unbounded, and it warns about it with a message. It then prints a model in which the objective function is a "large enough" representative value for infinity, which in this case is 1000000000. This value can actually be customized with the following option:

~$ optimathsat -input=fzn -opt.theory.la.infinite_pow=18 < test.fzn 
% objective: x (optimal model)
% warning: x is unbounded: oo
x = 1000000000000000000;
y = 2000000000000000000;
----------
=========