[Семинар по планированию] Лоран Перрон (Google Франция) | Решатель CP-SAT

Ключевые слова: Программирование ограничений, SAT-решатель, Целочисленное линейное программирование Решатель CP-SAT разработан группой исследования операций Google и является частью пакета оптимизации с открытым исходным кодом OR-Tools. Это реализация чисто целочисленного решателя программирования ограничений на основе SAT-решателя с использованием генерации ленивых дизъюнкций. Он черпает вдохновение из решателя chuffed и из пленарного доклада Питера Стакки на конференции CP 2013, посвященного генерации ленивых дизъюнкций. Решатель CP-SAT улучшает решатель chuffed в двух основных направлениях. Во-первых, он использует симплекс наряду с SAT-движком. Во-вторых, он реализует и использует портфель разнообразных рабочих процессов для своей части поиска. Использование симплекса дает очевидные преимущества линейной релаксации линейной части полной модели. Это также положило начало интеграции технологии MIP в CP-SAT. Это огромная работа, поскольку решатели MIP являются зрелыми и сложными. Он включает в себя предварительную обработку (которая уже была частью CP-SAT), двойные сокращения, специфические правила ветвления, отсечения, фиксацию сниженной стоимости и более продвинутые методы. Он также позволяет тесно интегрировать исследования сообщества Scheduling on MIP с самыми передовыми алгоритмами планирования. Это позволило совершить прорывы в решении и доказательстве сложных задач планирования для задач Job-Shop и задач планирования проектов с ограничениями по ресурсам. Использование портфеля различных рабочих упрощает тестирование новых идей и внедрение ортогональных методов с минимальными сложностями, за исключением контроля взрыва потенциальных рабочих. Эти рабочие могут быть классифицированы по нескольким критериям, таким как поиск прямых решений — с использованием полных решателей, локального поиска или поиска в большой окрестности, — улучшение двойных границ, попытка сокращения задачи с помощью непрерывного зондирования. Такое разнообразие поведения повысило устойчивость решателя, а непрерывный обмен информацией между рабочими привел к значительному ускорению при параллельном запуске нескольких рабочих. В целом, CP-SAT — это передовой решатель, демонстрирующий непревзойденные результаты в сообществе программистов ограничений, прорывные результаты на тестовых задачах планирования (с закрытием многих открытых проблем) и конкурентоспособные результаты с лучшими решателями задач целочисленного линейного программирования (на задачах чисто интегрального программирования). Организаторы: Зденек Ханзалек (ЧТУ в Праге), Михаэль Пинедо (Нью-Йоркский университет) и Гохуа Ван (Шанхайский университет Цзяотун). Веб-страница семинара: https://schedulingseminar.com/