Спекторський, Ігор ЯковичМачула, Антон Іванович2026-09-102026-09-102026Мачула, А. І. Математичне моделювання задачі розв’язання програмних залежностей методами теорії ґраток та булевих алгебр : дипломна робота … бакалавра : 124 Системний аналіз / Мачула Антон Іванович. – Київ, 2026. – 69 с.https://ela.kpi.ua/handle/123456789/82951Дипломна робота: 69 с., 9 рис., 6 табл., 2 додатки, 15 джерел. Об’єкт дослідження – задача розв’язання програмних залежностей у пакетних репозиторіях. Предмет дослідження – алгебраїчні структури (частково впорядковані множини, ґратки ідеалів порядку, булеві алгебри), що виникають при формалізації задачі інсталяційної сумісності, та методи їх обчислювальної реалізації засобами SAT і SMT солверів. Мета роботи – побудувати математичну модель задачі розв’язання програмних залежностей засобами теорії ґраток і булевих алгебр, дослідити умови збереження та руйнування ґраткової структури простору коректних інсталяцій, реалізувати прототип системи розв’язання залежностей та провести обчислювальні експерименти, що ілюструють теоретичні твердження. Методи дослідження – апарат теорії частково впорядкованих множин і ґраток, теорії булевих алгебр, теорії обчислювальної складності; застосування бібліотеки PySAT для роботи із SAT-солверами, системи Z3 для SMT та мови програмування Python для реалізації прототипу. Актуальність – існуючі менеджери пакетів реалізують розв’язання залежностей переважно евристично або прямим викликом SAT-солвера, тоді як алгебраїчна структура задачі залишається неявною; формалізація в термінах теорії ґраток дозволяє відокремити поліноміально розв’язні випадки від тих, де структура руйнується і потрібен SAT-солвер. Результати роботи – побудовано математичну модель задачі та доведено, що множина коректних інсталяцій у безконфліктному випадку є дистрибутивною ґраткою ідеалів порядку, яка руйнується при введенні обмежень несумісності; реалізовано прототип резолвера з SAT- та SMT-кодуваннями та механізмом видобування читабельного UNSAT-ядра; проведено функціонально-вартісний аналіз варіантів реалізації. Шляхи подальшого розвитку предмету дослідження – розширення моделі на випадок графа залежностей з циклами через апарат нерухомих точок, дослідження апроксимаційних алгоритмів для випадків з частковою ґратковою структурою та інтеграція з реальними пакетними менеджерами через адаптери до їхніх форматів метаданих.69 с.ukтеорія ґратокідеали порядкутеорема біркгофабулеві алгебризадача здійсненностіsatsmtрозв’язання програмних залежностей.lattice theoryorder idealsbirkhoff’s theoremboolean algebrassatisfiability problemsatsmtsoftware dependency resolutionBachelor Thesis