Crate resolvo

Implements a SAT solver for dependency resolution based on the CDCL algorithm (conflict-driven clause learning)

The CDCL algorithm is masterly explained in An Extensible SAT-solver. Regarding the data structures used, we mostly follow the approach taken by libsolv. The code of libsolv is, however, very low level C, so if you are looking for an introduction to CDCL, you are encouraged to look at the paper instead or to keep reading through this codebase and its comments.

Modules

• problem
  Types to examine why a problem was unsatisfiable, and to report the causes to the user.
• range
  Ranges are constraints defining sets of versions. They are a convenience struct that implements crate::VersionSet for any version type that implements Ord + Clone.
• runtime
  Solving in resolvo is a compute heavy operation. However, while computing the solver will request additional information from the crate::DependencyProvider and a dependency provider might want to perform multiple requests concurrently. To that end the crate::DependencyProviders methods are async. The implementer can implement the async operations in any way they choose including with any runtime they choose. However, the solver itself is completely single threaded, but it still has to await the calls to the dependency provider. Using the AsyncRuntime allows the caller of the solver to choose how to await the futures.

Structs

• Candidates
  A list of candidate solvables for a specific package. This is returned from DependencyProvider::get_candidates.
• DefaultSolvableDisplay
  Display merged candidates on single line with | as separator.
• KnownDependencies
  Holds information about the dependencies of a package when they are known.
• Mapping
  A Mapping<TValue> holds a collection of TValues that can be addressed by TIds. You can think of it as a HashMap<TId, TValue>, optimized for the case in which we know the TIds are contiguous.
• NameId
  The id associated to a package name
• Pool
  A pool that stores data related to the available packages.
• Solvable
  A solvable represents a single candidate of a package. This is type is generic on V which can be supplied by the user. In most cases this is going to be something like a record that contains the version of the package and other metadata. A solvable is always associated with a NameId, which is an interned name in the Pool.
• SolvableId
  The id associated to a solvable
• Solver
  Drives the SAT solving process
• SolverCache
  Keeps a cache of previously computed and/or requested information about solvables and version sets.
• StringId
  The id associated with a generic string
• VersionSetId
  The id associated with a VersionSet.

Enums

• Dependencies
  Holds information about the dependencies of a package.
• UnsolvableOrCancelled
  The root cause of a solver error.

Traits

• DependencyProvider
  Defines implementation specific behavior for the solver and a way for the solver to access the packages that are available in the system.
• PackageName
  The solver is based around the fact that for every package name we are trying to find a single variant. Variants are grouped by their respective package name. A package name is anything that we can compare and hash for uniqueness checks.
• SolvableDisplay
  Defines how merged candidates should be displayed.
• VersionSet
  A VersionSet describes a set of “versions”. The trait defines whether a given version is part of the set or not.