Решатель Or-tools cp_sat не дает согласованных результатов

Question

У меня проблема с оптимизацией, и я использую решатель or-tools cp_sat. Количество переменных составляет около 3500 (все логические), но количество ограничений огромно (~ 750000). Из 3500 переменных ~ 3000 напрямую зависят от других 500. Я тестировал 2 сценария ios:

1. С простой целевой функцией, зависящей от ~ 3000 ограничивающих переменных.
2. со сложной целевой функцией, зависящей от ~ 3000 * 3000 новых переменных, где каждая новая переменная является попарно логическим_и из переменных в (1).

Для каждого случая мы заполняем решатель подсказками для ~ 500 переменных.

Для 1 он не может найти оптимальное решение за разумное время. Примерно через 30–45 минут работы функция цели незначительно улучшается, но решения удовлетворительны.

Для 2 поведение странное. Примерно в половине случаев он утверждает, что проблема НЕВЕРОЯТНАЯ, в половине случаев утверждает, что нашла ОПТИМАЛЬНОЕ решение, но возвращает только решение, подразумеваемое подсказками. Лишь в редких случаях (менее пары процентов запусков) он выполняет некоторую оптимизацию и возвращает FEASIBLE.

Кроме того, в случае 1 используется около 4-6 ГБ памяти, а в случае 2 используется 100-120 ГБ памяти. .

Ожидается ли поведение в случае 2? Как мне подойти к отладке этого?

Answer 1

Для случая 2 проблема становится очень большой. Вы создаете 9M логических переменных.

Используете ли вы многопоточность?

Можете ли вы попробовать уменьшить размер модели и посмотреть, все ли это нестабильно?

В чем проблема? детерминированность создания c?

Вы используете большой коэффициент? Возможно, вы столкнулись с ошибкой целочисленного переполнения?

Спасибо