Математичне моделювання задачі розв’язання програмних залежностей методами теорії ґраток та булевих алгебр
Вантажиться...
Дата
2026
Автори
Науковий керівник
Назва журналу
Номер ISSN
Назва тому
Видавець
КПІ ім. Ігоря Сікорського
Анотація
Дипломна робота: 69 с., 9 рис., 6 табл., 2 додатки, 15 джерел.
Об’єкт дослідження – задача розв’язання програмних залежностей у пакетних репозиторіях. Предмет дослідження – алгебраїчні структури (частково впорядковані множини, ґратки ідеалів порядку, булеві алгебри), що виникають при формалізації задачі інсталяційної сумісності, та методи їх обчислювальної реалізації засобами SAT і SMT солверів. Мета роботи – побудувати математичну модель задачі розв’язання програмних залежностей засобами теорії ґраток і булевих алгебр, дослідити умови збереження та руйнування ґраткової структури простору коректних інсталяцій, реалізувати прототип системи розв’язання залежностей та провести обчислювальні експерименти, що ілюструють теоретичні твердження. Методи дослідження – апарат теорії частково впорядкованих множин і ґраток, теорії булевих алгебр, теорії обчислювальної складності; застосування бібліотеки PySAT для роботи із SAT-солверами, системи Z3 для SMT та мови програмування Python для реалізації прототипу. Актуальність – існуючі менеджери пакетів реалізують розв’язання залежностей переважно евристично або прямим викликом SAT-солвера, тоді як алгебраїчна структура задачі залишається неявною; формалізація в термінах теорії ґраток дозволяє відокремити поліноміально розв’язні випадки від тих, де структура руйнується і потрібен SAT-солвер. Результати роботи – побудовано математичну модель задачі та доведено, що множина коректних інсталяцій у безконфліктному випадку є дистрибутивною ґраткою ідеалів порядку, яка руйнується при введенні обмежень несумісності; реалізовано прототип резолвера з SAT- та SMT-кодуваннями та механізмом видобування читабельного UNSAT-ядра; проведено функціонально-вартісний аналіз варіантів реалізації. Шляхи подальшого розвитку предмету дослідження – розширення моделі на випадок графа залежностей з циклами через апарат нерухомих точок, дослідження апроксимаційних алгоритмів для випадків з частковою ґратковою структурою та інтеграція з реальними пакетними менеджерами через адаптери до їхніх форматів метаданих.
Опис
Ключові слова
теорія ґраток, ідеали порядку, теорема біркгофа, булеві алгебри, задача здійсненності, sat, smt, розв’язання програмних залежностей., lattice theory, order ideals, birkhoff’s theorem, boolean algebras, satisfiability problem, sat, smt, software dependency resolution
Бібліографічний опис
Мачула, А. І. Математичне моделювання задачі розв’язання програмних залежностей методами теорії ґраток та булевих алгебр : дипломна робота … бакалавра : 124 Системний аналіз / Мачула Антон Іванович. – Київ, 2026. – 69 с.