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

conflict

Types to examine why a problem was unsatisfiable, and to report the causes to the user.

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.

snapshot

Provides DependencySnapshot, an object that can capture a snapshot of a dependency provider. This can be very useful to abstract over all the ecosystem specific code and provide a serializable object that can later be reused to solve dependencies.

utils

Defines several helper functions and structs that make it easier to implement a custom dependency provider.

Structs

Candidates

A list of candidate solvables for a specific package. This is returned from DependencyProvider::get_candidates.

ConditionId

The id associated with a Condition.

ConditionalRequirement

A ConditionalRequirement is a requirement that is only enforced when a certain condition holds.

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

Problem

Describes the problem that is to be solved by the solver.

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.

VersionSetUnionId

The id associated with a union (logical OR) of two or more version sets.

Enums

Condition

A condition defines a boolean expression that evaluates to true or false based on whether one or more other requirements are true or false.

Dependencies

Holds information about the dependencies of a package.

HintDependenciesAvailable

Defines for which candidates dependencies are available without the DependencyProvider having to perform extra work, e.g. it’s cheap to request them.

LogicalOperator

A LogicalOperator defines how multiple conditions are compared to each other.

Requirement

Specifies the dependency of a solvable on a set of version sets.

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.

Interner

An object that is used by the solver to query certain properties of different internalized objects.