2.4. Задача разрешения зависимостей пакетов

2.4.1. SAT- и SMT-решатели

При установке пакета заданной версии необходимо установить все его зависимости – программные библиотеки и прочие файлы, обязательные для корректной работы пакета. Например, для пакета Debian его зависимости представлены другими пакетами Debian, а совместимые версии указаны в файле Packages.gz. Кроме того, у пакета также могут быть транзитивные зависимости – такие пакеты, от которых он зависит неявно, через другие пакеты.

В файлах Packages.gz со списками пакетов из компонентов репозитория Ubuntu main и universe, по результатам анализа которых в предыдущем разделе были построены графы зависимостей, приведены сведения о более 60 000 пакетов. Вследствие этого разрешение зависимостей вручную при установке пакета Debian являлось бы чрезвычайно трудоёмким процессом – ведь помимо построения графа зависимостей необходимо для каждой зависимости устанавливаемого пакета выбрать версию, совместимую и с пакетом, и со всеми его зависимостями, включая транзитивные. Поэтому на практике для разрешения зависимостей используются специализированные инструменты, такие как, например, универсальные решатели NP-полных задач [8].

Задача разрешения зависимостей является NP-полной [33] и может быть сведена к задаче выполнимости булевой формулы (Boolean Satisfiability Problem, SAT). Для решения SAT могут использоваться решатели NP-полных задач, такие как, например, Z3 [34] и MiniZinc [35]. В этом разделе рассмотрим процесс работы с Z3 на примере решения простой задачи выполнимости формул в теориях (Satisfiability Modulo Theories, SMT). В SMT, в отличие от SAT, в формуле могут фигурировать предикаты, оперирующие, например, битовыми векторами.

2.4.2. Пример описания задачи для SMT-решателя

Попробуем с помощью Z3 [34] автоматически решить следующую задачу:

На лужайке находятся фазаны и кролики. Можно рассмотреть всего 9 голов и 24 лапы. Сколько на лужайке кроликов и сколько фазанов?

Заметим, что 9 голов, которые можно рассмотреть по условию задачи, могут принадлежать как кроликам, так и фазанам. Кроме того, известно, что у кролика 4 лапы, а у фазана – 2. Обозначим число кроликов как $r$, а число фазанов – как $p$. Тогда условие задачи может быть представлено в виде системы уравнений с целочисленными переменными:

$$ \begin{cases} r + p = 9,\\ 4r + 2p = 24. \end{cases} $$

(1)

Решение для системы уравнений (1) легко найти автоматически при помощи решателя Z3. Установим пакет z3-solver для языка программирования Python при помощи пакетного менеджера PyPI:

~$ pip install z3-solver
Collecting z3-solver
  Downloading z3_solver-4.13.4.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (29.0 MB)
     ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 29.0/29.0 MB 18.0 MB/s eta 0:00:00
Installing collected packages: z3-solver
Successfully installed z3-solver-4.13.4.0

Создадим новый файл solve.py и поместим в него следующий код:

from z3 import *

r = Int("r")
p = Int("p")

s = Solver()
s.add(r + p == 9)
s.add(4 * r + 2 * p == 24)

print(s.check())
print(s.model())

В приведённом коде сначала создаются 2 целочисленные символьные переменные r и p, где r – число кроликов, а p – число фазанов. После этого создаётся экземпляр класса Solver, к которому добавляются ограничения на число голов и число лап, как в составленной выше системе уравнений. Затем выполняется проверка системы уравнений на наличие решений посредством вызова метода check. В случае, если решения существуют, результатом работы check будет константа sat, а в случае отсутствия решений – unsat. При помощи вызова метода model в stdout выводится найденное решение.

Проверим работу программы:

~$ python solve.py
sat
[p = 6, r = 3]

Решение задачи найдено автоматически – 6 фазанов и 3 кролика.

2.4.3. Разрешение зависимостей с помощью SMT-решателя

Теперь рассмотрим пример автоматического разрешения зависимостей при помощи SMT-решателя Z3 [34] для пакета root, граф зависимостей которого показан на рис. 19.

Стрелки, соединяющие пакеты в графе, обозначают факт наличия зависимости одного пакета от другого. В случае, если из одной и той же версии пакета A исходит несколько стрелок, указывающих на разные версии пакета B, то это значит, что пакет А совместим с несколькими версиями пакета B, и необходимо решить, какую версию B следует установить. В рассматриваемой задаче 2 версии одного и того же пакета устанавливать не нужно.

Из графа зависимостей, приведённого на рис. 19, следует, что пакет root версии 1.0.0 совместим с любой из версий пакета menu и только с версией 1.0.0 пакета icons. Это значит, что при установке пакета root обязательна установка любой из версий пакета menu, а также пакета icons версии 1.0.0. Пакет dropdown является транзитивной зависимостью root, поскольку явно root от dropdown не зависит, но каждой из версий пакета menu необходима установка пакета dropdown.

Рисунок 19. Граф зависимостей пакета root

Представим граф, показанный на рис. 19, в виде булевой формулы. Стрелки в графе зависимостей выразим как импликации, а совместимость одного пакета с различными версиями другого пакета укажем при помощи логического «или».

Введём следующие обозначения:

Пакет root обозначим как $r$.
Пакет menu – как $m$.
Пакет dropdown – как $d$.
Пакет icons – как $i$.

Версию пакета будем указывать справа от его имени, игнорируя номер патч-версии [8], поскольку в графе зависимостей на рис. 19 номер патч-версии всегда равен 0. Например, логическую переменную, обозначающую, следует ли устанавливать пакет root версии 1.0.0, обозначим как $r_{1.0}$ – такая переменная принимает значение 1 в случае, если пакет следует установить, и 0, если его устанавливать не следует.

Запишем булеву формулу для графа, показанного на рис. 19:

$$ \begin{align} ( r_{1.0} \implies (m_{1.5} \lor m_{1.4} \lor m_{1.3} \lor m_{1.2} \lor m_{1.1} \lor m_{1.0}) \land i_{1.0}) \land \\ ( m_{1.5} \implies d_{2.3}) \land ( m_{1.4} \implies d_{2.3} \lor d_{2.2}) \land ( m_{1.3} \implies d_{2.2}) \land \\ ( m_{1.2} \implies d_{2.2} \lor d_{2.1}) \land ( m_{1.1} \implies d_{2.2} \lor d_{2.1} \lor d_{2.0}) \land ( m_{1.0} \implies d_{1.8}) \land \\ ( d_{2.3} \implies i_{2.2}) \land ( d_{2.2} \implies i_{2.2}) \land ( d_{2.1} \implies i_{2.2}) \land ( d_{2.0} \implies i_{2.2}) \land \\ r_{1.0}. \end{align} $$

(2)

Кроме импликаций, обозначающих, что при установке пакета слева от оператора импликации необходимо установить его зависимости, указанные справа от оператора импликации, в формуле (2) есть последний компонент, обязывающий установить пакет $r_{1.0}$.

При установке пакета и его зависимостей пакетному менеджеру также необходимо убедиться, что для каждой зависимости установлена только одна из её версий. Это дополнительное правило можно представить в виде SMT-формулы – формулы, в которой логические переменные могут быть заменены предикатами:

$$ \begin{align} (m_{1.5} + m_{1.4} + m_{1.3} + m_{1.2} + m_{1.1} + m_{1.0} \leq 1) \land \\ (d_{2.3} + d_{2.2} + d_{2.1} + d_{2.0} + d_{1.8} \leq 1) \land \\ (i_{2.0} + i_{1.0} \leq 1) \land \\ (r_{1.0} \leq 1). \end{align} $$

(3)

Теперь для разрешения зависимостей необходимо объединить формулы (2) и (3) при помощи логического «и» и найти такие значения переменных, при которых полученная формула выполняется, либо показать, что таких значений нет и, следовательно, задача разрешения зависимостей не имеет решений.

Создадим файл deps.py и поместим в него словарь, ключами в котором являются короткие имена пакетов с указанием их версий, а значениями – списки, содержащие зависимости, сгруппированные по имени пакета. Содержимое словаря соответствует булевой формуле (2) и графу, показанному на рис. 19:

packages = {
    'r10': [('m15', 'm14', 'm13', 'm12', 'm11', 'm10'), ('i10',)],
    'm15': [('d23',)],
    'm14': [('d23', 'd22')],
    'm13': [('d22',)],
    'm12': [('d22', 'd21')],
    'm11': [('d22', 'd21', 'd20')],
    'm10': [('d18',)],
    'd23': [('i20',)],
    'd22': [('i20',)],
    'd21': [('i20',)],
    'd20': [('i20',)],
    'd18': [],
    'i10': [],
    'i20': [],
}

Дополним файл deps.py и опишем задачу для Z3 [34]:

from z3 import *
from itertools import groupby

var = {name: Bool(name) for name in packages}
s = Solver()
s.add(var['r10'])

for name in packages:
    for alts in packages[name]:
        s.add(Implies(var[name], Or([var[d] for d in alts])))

for _, versions in groupby(packages, lambda p: p[0]):
    s.add(Sum([var[v] for v in versions]) <= 1)

if s.check() == sat:
    print(s.model())

Сначала создадим словарь var, связывающий имена пакетов с инициализированными символьными логическими переменными. После этого создадим экземпляр класса решателя Solver и укажем, что пакет root версии 1.0.0 обязателен к установке, как в формуле (2).

Для каждого пакета и его зависимостей из словаря packages сформируем выражения с импликациями по формуле (2), воспользовавшись классами Implies и Or, и добавим сформированные выражения к набору ограничений экземпляра класса Solver при помощи метода add. Затем сгруппируем ключи словаря packages по имени пакета, получив таким образом списки версий, и добавим к набору ограничений решателя компоненты SMT-формулы (3), предварительно создав из списка версий символьную переменную Sum и сравнив её с единицей, единица при этом неявно преобразуется в символьную переменную.

После того, как задача для Z3 полностью описана, проверим при помощи вызова метода check, имеет ли задача решения, и в случае положительного результата выведем найденное решение в stdout. Оставим в stdout только логические переменные со значениями True при помощи утилиты grep:

~$ python deps.py | grep True
 r10 = True,
 m10 = True,
 d18 = True,
 i10 = True,

Выделим выбранные решателем версии пакетов на графе зависимостей символом «✓». Результат показан на рис. 20.

Рисунок 20. Выбранные SMT-решателем Z3 версии пакетов

Таким образом, SMT-решателем было найдено следующее решение:

Установить root версии 1.0.0.
Установить menu версии 1.0.0.
Установить dropdown версии 1.8.0.
Установить icons версии 1.0.0.

2.4.4. Упражнения

Задача 1. Добавьте в реализованную программу для разрешения зависимостей на Z3 дополнительное ограничение с целью проверки, что автоматически найденное решение — единственное. Убедитесь в единственности решения для графа зависимостей, показанного на рис. 19.

Задача 2. Докажите законы де Моргана на Z3.

Задача 3. Решите задачу о расстановке 8 ферзей на Z3.

Задача 4. Используйте язык MiniZinc вместо Z3 для разрешения зависимостей пакетов.

Задача 5. Разработайте инструмент разрешения зависимостей, в котором версии пакетов представлены в формате SemVer.

Keyboard shortcuts

Конфигурационное управление. Курс в РТУ МИРЭА