-
Notifications
You must be signed in to change notification settings - Fork 9
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Use a SAT solver to work out the dependency tree #139
Comments
Our problemThe problem space is defined by a set of packages that depend on each other in various ways. A package is comprised of:
Also, not considered now but could be considered in the future:
Given a set of installed packages in the system, and a set of packages that we want to be installed, we want to know if there's a set of solutions to it, and which one is better. Or, we want to know if there is no solution, and why. This is a Satisfabiality problem that is NP-hard. Some of these features of packages are a non-issue for resolving the dependency problem: namespaces are just part of what defines a package, pinned and manually installed packages just create a new hard constraint to be added, etc. Pure SAT, MaxSAT, Pseudo-Boolean SAT problem?In the past, dependency problems have been solved either by custom heuristics or by using a SAT solver and pruning results with ad-hoc heuristics after the resolution. In our case, we have several strategies we want to apply to our problem, some of which may be selected at run time. Given the amount of strategies and the constraints arising from our package definition, we will define our problem as a Pseudo-Boolean SAT one. This allows to specify weights on our statements, to implement our strategies, and allows for multicriteria optimization. Also, since the expected number of charts installed in a cluster is going to be "low" (in the order of 10^1 instead of 10^3 or more that is normally seen for these problems), we may try to obtain more optimized solutions in a reasonable time. How does an upgrade operation work in a pure SAT dependency problem?On traditional Linux OS dependency problems, the satisfiability of the upgrades is checked after the fact that packages have entered the repositories. This is normally accomplished by running tools against the repositories. These can be SAT solvers, specific scheduled jobs (e.g: debcheck & paper, debgraph in Debian), CI jobs for default installations, CI jobs for upgrades between different distribution releases, etc, in addition to normal QA work. This is is also complemented by gating the package set through several repositories. E.g: OpenSUSE Factory -> Tumbleweed -> Leap, or Debian Unstable -> Testing -> Stable. On the distribution receiving new packages (OpenSUSE Factory, Debian Unstable), transient uninstallability problems are expected. These problems are increasingly exposed when the same package cannot be installed in several architectures. On the more stable distributions (Opensuse Leap, Debian Stable), it is expected that all or most of the installability problems have been found. In Hypper's case, we want the possibility to depend on packages (Helm charts) outside of our curated repositories. Therefore, we would benefit from knowing if a system can be upgraded or not, regardless of our ability on curating the repositories. Hence, we use a SAT solver directly when performing those upgrades. Strategies
Not considered right now:
Encoding the Pseudo-Boolean Optimization problem |
Existing solver libraries in Golang that we consideredWe want a MAXSAT/Pseudo-Boolean SAT solver library with ample feature support, good docs, good API, a Gini https://github.com/IRIFrance/gini1 big known consumer, github.com/operator-framework/operator-lifecycle-manager. Luet https://github.com/mudler/luet https://github.com/mudler/luetGPLv3. go-sat https://github.com/mitchellh/go-satPure SAT solver. saturday https://github.com/cespare/saturdayPure SAT solver. dpll https://github.com/bmatsuo/dpllPure SAT solver. Go dep https://github.com/golang/dep/tree/master/gpsDeprecated, too tightly coupled with go modules. vgo https://github.com/golang/goUses non-SAT solver heuristics: Non exported API, all under Selected implementationGophersat https://github.com/crillab/gophersatNo big known consumers, but several medium consumers (see |
How we handle upgrading shared dependencies is something we should ask the charts folks in rancher. They may have some insight. The same goes for any of our assumptions. I pinged some folks on this case. |
We should minimize changes to the installed packages. If a shared dependency is already present at an acceptable version we should continue running it at that version. |
For version bumps, that's easily doable, and should come for free: a "package" is defined by its version and chart, so asking for not bumping packages is asking to not install specific packages. For changes to values (and redeployments), we may need to include values to the package definition. |
Opened draft PR to be able to argue better than here in the comments: #171. |
No description provided.
The text was updated successfully, but these errors were encountered: