Crate rattler_libsolv_rs

source ·
Expand description

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.

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.
  • Dependencies
    Holds information about the dependencies of a package.
  • 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
  • VersionSetId
    The id associated with a VersionSet.

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 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 is describes a set of “versions”. The trait defines whether a given version is part of the set or not.