CSP, SAT && RL
Luet allows you to specify 3 types of set of contraints on a package definition:
The package definition in your tree definition, along with its Requires and Conflicts, are turned into Boolean formulas that are consumed by the solver to compute a solution. The solution represent the state of your system after a particular query is asked to the solver (Install, Uninstall, Upgrade).
Requires and Conflicts
A list of requires and conflicts, composed of one or more packages, becomes a SAT formula. The formula is then given to the SAT solver to compute a finite state set of packages which must be installed in the system in order to met the requirements.
As Luet allows to express constraints with selectors ( e.g.
A depends on >=B-1.0) it generates additional constraints to guarantee that at least one package and at most one is picked as dependency (ALO and AMO).
Provides constraints are not encoded in a SAT formula. Instead, they are
expanded into an in-place substitution of the packages that they have to be replaced with.
They share the same SAT logic of expansion, allowing to swap entire version ranges (e.g.
>=1.0), allowing to handle package rename, removals, and virtuals.
- OPIUM (Luet is inspired by it): https://ranjitjhala.github.io/static/opium.pdf
- FROM TRACTABLE CSP TO TRACTABLE SAT: https://www.cs.ox.ac.uk/files/4014/maxclosed_orderencoding_v16_TR.pdf
- Solver concepts applied to packages (
Was this page helpful?
Glad to hear it! Please tell us how we can improve.
Sorry to hear that. Please tell us how we can improve.