Как максимизировать var int, размер которого превышает 32 бита?

Я использую minizinc со встроенным Gecode 6.1.1, и я хочу максимизировать целевую функцию со значениями, которые намного больше, чем max int 32. Максимальное значение целого числа с 32 битами составляет 2147483646. Хотя, похоже, не так много информации быть доступным относительно максимального значения для целых чисел в справке minizinc. Однако следующий тест показывает, что Minizinc использует 32-битные целые числа.

Тест очень простой, он просто пытается максимизировать var int.

var int: maxInt;
constraint maxInt>0;

solve maximize maxInt;

output ["maxInt = \(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;

optimization minizinc gecode optimathsat
person Spyros K    schedule 07.08.2019    source источник

Ответы (2)


arrow_upward
4
arrow_downward

Это не совсем MiniZinc, который здесь является пределом, это решающая программа. Как указано в документации (из ссылки на целые числа, которую вы процитировали, мой акцент):

Обзор. Целые числа представляют собой целые числа. Целочисленные представления определяются реализацией. Это означает, что представимый диапазон целых чисел определяется реализацией. Однако реализация должна прерваться во время выполнения при переполнении целочисленной операции.

Вот несколько примеров решения maxInt для некоторых решателей при запуске вашей тестовой модели (с использованием ограничения maxInt > 0):

  1. Gecode: 2147483646
  2. PicatSAT: 72057594037927935 (2 ^ 54)
  3. Взбитые: 500000000
person hakank    schedule 07.08.2019
comment
Спасибо, это действительно так. - person Spyros K; 07.08.2019

arrow_upward
2
arrow_downward

Вы также можете попробовать 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;
----------
=========
person Patrick Trentin    schedule 07.08.2019