Математичне моделювання задачі розв’язання програмних залежностей методами теорії ґраток та булевих алгебр

Скорочена інформація про документ
dc.contributor.advisorСпекторський, Ігор Якович
dc.contributor.authorМачула, Антон Іванович
dc.date.accessioned2026-09-10T07:45:32Z
dc.date.available2026-09-10T07:45:32Z
dc.date.issued2026
dc.description.abstractДипломна робота: 69 с., 9 рис., 6 табл., 2 додатки, 15 джерел. Об’єкт дослідження – задача розв’язання програмних залежностей у пакетних репозиторіях. Предмет дослідження – алгебраїчні структури (частково впорядковані множини, ґратки ідеалів порядку, булеві алгебри), що виникають при формалізації задачі інсталяційної сумісності, та методи їх обчислювальної реалізації засобами SAT і SMT солверів. Мета роботи – побудувати математичну модель задачі розв’язання програмних залежностей засобами теорії ґраток і булевих алгебр, дослідити умови збереження та руйнування ґраткової структури простору коректних інсталяцій, реалізувати прототип системи розв’язання залежностей та провести обчислювальні експерименти, що ілюструють теоретичні твердження. Методи дослідження – апарат теорії частково впорядкованих множин і ґраток, теорії булевих алгебр, теорії обчислювальної складності; застосування бібліотеки PySAT для роботи із SAT-солверами, системи Z3 для SMT та мови програмування Python для реалізації прототипу. Актуальність – існуючі менеджери пакетів реалізують розв’язання залежностей переважно евристично або прямим викликом SAT-солвера, тоді як алгебраїчна структура задачі залишається неявною; формалізація в термінах теорії ґраток дозволяє відокремити поліноміально розв’язні випадки від тих, де структура руйнується і потрібен SAT-солвер. Результати роботи – побудовано математичну модель задачі та доведено, що множина коректних інсталяцій у безконфліктному випадку є дистрибутивною ґраткою ідеалів порядку, яка руйнується при введенні обмежень несумісності; реалізовано прототип резолвера з SAT- та SMT-кодуваннями та механізмом видобування читабельного UNSAT-ядра; проведено функціонально-вартісний аналіз варіантів реалізації. Шляхи подальшого розвитку предмету дослідження – розширення моделі на випадок графа залежностей з циклами через апарат нерухомих точок, дослідження апроксимаційних алгоритмів для випадків з частковою ґратковою структурою та інтеграція з реальними пакетними менеджерами через адаптери до їхніх форматів метаданих.
dc.description.abstractotherDiploma thesis: 69 p., 9 fig., 6 tables, 2 appendicies, 15 sources. Object of Research – the software dependency resolution problem in package repositories. Subject of Research – the algebraic structures (partially ordered sets, lattices of order ideals, Boolean algebras) arising in the formalization of the installation compatibility problem, and the methods of their computational implementation by means of SAT and SMT solvers. Objective – to build a mathematical model of the software dependency resolution problem using lattice theory and Boolean algebras, to investigate the conditions under which the lattice structure of the space of correct installations is preserved or destroyed, to implement a prototype dependency resolver, and to carry out computational experiments illustrating the theoretical claims. Research Methods – the apparatus of the theory of partially ordered sets and lattices, the theory of Boolean algebras, and computational complexity theory; the use of the PySAT library for working with SAT solvers, the Z3 system for SMT, and the Python programming language for implementing the prototype. Relevance – existing package managers solve dependency resolution mostly heuristically or by directly invoking a SAT solver, while the algebraic structure of the problem remains implicit; a lattice-theoretic formalization makes it possible to separate the polynomially solvable cases from those where the structure breaks down and a SAT solver is required. Results – a mathematical model of the problem was built and it was proved that the set of correct installations in the conflict-free case is a distributive lattice of order ideals, which is destroyed upon the introduction of incompatibility constraints; a resolver prototype with SAT and SMT encodings and a readable UNSAT-core extraction mechanism was implemented; a functional-cost analysis of the implementation variants was carried out. Future Development Paths – extending the model to dependency graphs with cycles via the fixed-point apparatus, investigating approximation algorithms for cases with partial lattice structure, and integrating with real package managers through adapters to their metadata formats.
dc.format.extent69 с.
dc.identifier.citationМачула, А. І. Математичне моделювання задачі розв’язання програмних залежностей методами теорії ґраток та булевих алгебр : дипломна робота … бакалавра : 124 Системний аналіз / Мачула Антон Іванович. – Київ, 2026. – 69 с.
dc.identifier.urihttps://ela.kpi.ua/handle/123456789/82951
dc.language.isouk
dc.publisherКПІ ім. Ігоря Сікорського
dc.publisher.placeКиїв
dc.subjectтеорія ґраток
dc.subjectідеали порядку
dc.subjectтеорема біркгофа
dc.subjectбулеві алгебри
dc.subjectзадача здійсненності
dc.subjectsat
dc.subjectsmt
dc.subjectрозв’язання програмних залежностей.
dc.subjectlattice theory
dc.subjectorder ideals
dc.subjectbirkhoff’s theorem
dc.subjectboolean algebras
dc.subjectsatisfiability problem
dc.subjectsat
dc.subjectsmt
dc.subjectsoftware dependency resolution
dc.titleМатематичне моделювання задачі розв’язання програмних залежностей методами теорії ґраток та булевих алгебр
dc.typeBachelor Thesis

Файли

Контейнер файлів
Зараз показуємо 1 - 1 з 1
Ескіз
Назва:
Machula_bakalavr.pdf
Розмір:
1.99 MB
Формат:
Adobe Portable Document Format
Завантажити
Ліцензійна угода
Зараз показуємо 1 - 1 з 1
Ескіз недоступний
Назва:
license.txt
Розмір:
8.98 KB
Формат:
Item-specific license agreed upon to submission
Опис:
Завантажити

Зібрання

Бакалаврські роботи (ММСА)
Бакалаврські роботи