viccuad
commented
3 years ago Existing solver libraries in Golang that we considered
We want a MAXSAT/Pseudo-Boolean SAT solver library with ample feature support, good docs, good API, a thriving community, verbose output, in Golang, and with a compatible license that can be statically linked. We want a solver that is used in the field, updated continously with latest SAT improvements from SAT competitions. We want a solver that handles optimization problems (hence, a pseudo-boolean SAT solver).
Gini https://github.com/IRIFrance/gini
1 big known consumer, github.com/operator-framework/operator-lifecycle-manager. Only pure SAT CNF problems.
Luet https://github.com/mudler/luet https://github.com/mudler/luet
GPLv3. It defines a pure SAT problem (with constraints and literals inspired by OPIUM) (see https://github.com/mudler/luet/blob/master/pkg/solver/solver.go#L37-L54). It uses the pure SAT solving of gophersat, and, if there's some failure, it uses qlearning to recover (see https://github.com/mudler/luet/blob/master/pkg/solver/resolver.go). See also https://luet-lab.github.io/docs/docs/concepts/overview/constraints/.
go-sat https://github.com/mitchellh/go-sat
Pure SAT solver. Last developed 4 years ago. No known consumers.
saturday https://github.com/cespare/saturday
Pure SAT solver.
dpll https://github.com/bmatsuo/dpll
Pure SAT solver.
Go dep https://github.com/golang/dep/tree/master/gps
Deprecated, too tightly coupled with go modules.
vgo https://github.com/golang/go
Uses non-SAT solver heuristics: https://research.swtch.com/vgo-principles https://research.swtch.com/vgo-mvs
Non exported API, all under src/cmd/go/internal/{mod*,mvs}.
Selected implementation
Gophersat https://github.com/crillab/gophersat
No big known consumers, but several medium consumers (see https://github.com/search?q=gophersat&type=code). Solves pseudo-boolean, MAXSAT problems (e.g: efficiency problems). Provides sub-optimal solutions to PB/MaxSAT problems as soon as it finds them, without needing to wait for the optimal solution. We can then decide how much we want to wait for a solution. Last development Nov 2020. Announcement email 2017: https://groups.google.com/g/golang-nuts/c/SE1dNC8N46o/m/0drzp9jdAQAJ.
mattfarina
Our problem
The problem space is defined by a set of packages that depend on each other in various ways. A package is comprised of:
~,^). They get collapsed into a specific semver when deployed.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. Nowadays, more and more dependency problems are solved either by reducing the problem space (eg: go modules) or by using a SAT solver, with or without heuristics to help reduce the problem space.
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. In addition, some solvers have the ability to return sub-optimal solutions as soon as they find them, without waiting for the optimal solution calculation.
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