satsolver SAT Solver for package management
- Michael Schroeder <firstname.lastname@example.org>
Welcome to the sat solver documentation page.
The SAT solver is a package dependency solver library which offers the following:
See History of satsolver for the SAT solver history.
Express packaga dependencies as boolean expressions. (in conjunctive normal form - CNF)
(! == boolean not)
- A requires B -> !A or B
- A conflicts B -> !A or !B (! (A and B) A obsoletes B -> A conflicts B
- A provides B -> B == A (replace all occurences of B in CNFs with A)
- Representation of package with name, version, architecture, dependencies
- Collection of solvables, like a repository or the rpm database
- Collection of repositories. See more at The Pool
- The installed packages are represented as a single repo
- The installed and available packages are represented as a Pool
The solver gets initialized by passing it the complete pool (all Solvables) and a single Source (called 'system', representing the installed Solvables).
It then creates rules to flag the Solvables of 'system' as installed.
See Code Conventions
for code conventions.
for a general overview on references about satisfiability, sat-solving and its relation to package dependencies.