Лаборатория 6.2. Логических и оптимизационных методов анализа сложных систем
Основные направления исследований лаборатории:
точные и приближенные алгоритмы решения комбинаторных задач за счет сводимости к проблеме булевой выполнимости (SAT) и её оптимизационному варианту – проблеме максимальной выполнимости (MaxSAT);
методы исследования сложных технических систем, в частности, многоуровневых транспортно-логистических систем, на основе интеграции средств информационно-логического, математического и имитационного моделирования и анализа данных.
Важнейшие научные результаты:
Разработаны точные алгоритмы решения SAT, основанные на концепции декомпозиционной трудности; разработаны различные подходы к декомпозиционному представлению булевых формул; разработанные алгоритмы применены для решения трудных вариантов SAT, связанных с задачей проверки эквивалентности булевых схем, а также к задачам оценивания стойкости криптографических функций, используемых в современных системах компьютерной безопасности.
Предложена и развита концепция вероятностных лазеек в SAT: лазейками (Backdoors) называются такие множества переменных в рассматриваемой формуле, знание которых позволяет существенно сократить время решения SAT в отношении этой формулы. В отличие от сильных лазеек, вероятностные лазейки малой размерности не являются редким феноменом, что делает перспективным их использование для решения трудных примеров SAT, связанных с различными индустриальными задачами.
Разработаны приближенные алгоритмы решения задачи MaxSAT за счет принципа склеивания переменных (Merging Variables Principle, MVP). Данный принцип может использоваться как в контексте концепции локального поиска, так и совместно с эволюционными вычислениями. Основанные на MVP алгоритмы продемонстрировали практическую эффективность на задачах размещения (Location Problem), а также на задачах поиска прообразов криптографических хеш-функций при дополнительных ограничениях на хеш.
Разработаны новые параллельные алгоритмы решения SAT, базирующиеся на методе Cube-and-Conquer. С помощью этих алгоритмов впервые найдены прообразы 43-шаговой функции сжатия MD4, 29-шаговой функции сжатия MD5 и 24-раундовой функции сжатия SHA-1. Также с помощью разработанных алгоритмов впервые перечислены расширенно самоортогональные диагональные латинские квадраты порядка 10 и диагональные латинские квадраты Брауна порядка 10. Кроме того, найдена тройка диагональных латинских квадратов порядка 10, которая является наиболее близкой к тройке попарно ортогональных диагональных латинских квадратов порядка 10.
Разработана технология моделирования транспортных систем при учете случайных факторов, основанная на теории массового обслуживания с применением групповых потоков заявок и сетей массового обслуживания. Построены и исследованы модели городских транспортно-пересадочных узлов, крупных железнодорожных станций и участков, морских портов в России и за рубежом, включая Монголию и Вьетнам.
Внешний вид и структурная модель специализированного морского терминала
Предложена технология построения математических моделей и численных методов исследования транспортно-логистических объектов и систем на основе физических аналогий. Так, задачи о размещении логистических объектов и организации системы коммуникаций между ними сведены к задачам вариационного исчисления специального вида; на основе оптико-геометрической аналогии и принципов Ферма и Гюйгенса разработаны эффективные численные методы их решения.
Карта района Нам Дана, Нге Ана (Вьетнам) и оптимальное расположение больниц
Разработаны численные методы построения внешней и внутренней аппроксимации множеств со сложной геометрией для случая специальной неевклидовой метрики, с помощью которых решены задачи оптимального размещения объектов логистической инфраструктуры с учетом пространственных ограничений.
Внутренняя и внешняя аппроксимации множества равными шарами