Ограничение времени, установленное в командной строке, не ограничивает время выполнения

Я пытаюсь запустить модель MiniZinc с помощью решателя OSICBC через bash со следующими аргументами командной строки (с ограничением по времени 30000 мс или 30 с):

minizinc --solver osicbc model.mzn data.dzn --time-limit 30000 --output-time

Но только для этого прогона весь процесс после выполнения команды для получения выходных данных занимает около минуты, а в выходных данных в конце отображается «Истекшее время: 36,21 с».

Является ли это правильным подходом к наложению ограничения по времени при запуске этой модели, где общее затраченное время включает время, с которого вызывается команда, выходы которой отображаются в моем терминале?


ubuntu-18.04 linux time-limiting minizinc
person Stoner    schedule 14.10.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Флаг командной строки --time-limit был введен в MiniZinc 2.2.0, чтобы позволить пользователю ограничивать комбинированное время, затрачиваемое компилятором и решателем. Он также ввел --solver-time-limit, чтобы просто ограничить время решателя.

Обратите внимание, что minizinc даст решателю дополнительное время для вывода своих окончательных решений.

Если вы почувствуете, что эти флаги не ограничивают работу решателя указанным временем и не останавливаются в течение секунды указанного лимита, то это может указывать на ошибку, и я предлагаю вам сделать отчет об ошибке: https://github.com/MiniZinc/libminizinc/issues

person Dekker1    schedule 14.10.2018
comment
Спасибо за подробную разбивку и пояснения! А также за то, что снова ответил на один из моих вопросов по MiniZinc :) - person Stoner; 15.10.2018
comment
Просто из любопытства, работает ли флаг --solver-time-limit для решателя osicbc? Например, при вызове следующим образом: minizinc --solver osicbc --solver-time-limit 10000 model.mzn data.dzn? - person Stoner; 15.10.2018
comment
Я заметил, что из minizinc.org/doc-2.2.1/en/ find_mus.html, у некоторых решателей есть собственные параметры, например --timeout <seconds>, которых osicbc, похоже, нет .. - person Stoner; 15.10.2018
comment
Решатели могут иметь свои собственные аргументы командной строки, хотя я думаю, что флаг timeout для findMUS, скорее всего, является ошибкой. Такие вещи, как тайм-ауты, поддерживаются использованием стандартных флагов (minizinc.org/doc-2.2.1/en/). Если решатель поддерживает установку тайм-аута, он будет указан с помощью флага -t. если он не работает или пытается работать дольше, он будет отключен драйвером MiniZinc. - person Dekker1; 15.10.2018
comment
Спасибо за ваше разъяснение! Это очень помогает :) - person Stoner; 15.10.2018