Policies in sat-solver

Definition

Policies are assumptions (decisions) in the code not reasoned by the dependency semantics.

Motivation

There are local policies, looking at a small set of packages during solving. Examples:

There are global policies, looking at the complete transaction after solving is complete.

Examples:

Global policies are currently not supported at all.

Generally, policies help the solver to choose from multiple possibilities. In most cases, this can be represented as a filter operation working on a list of candidates and filtering out unwanted ones - ideally resulting in a single candidate.

Recognized policies

These are the policies we currently know of (which should be exposed via the policy layer)

Generic filter

The generic function is 'choose among multiple candidates' by

Policy engine implementation

The policy engine should support policies in a generic way.

Some policies might be quite complex, it should be possible to build up a policy chain - passing a result back to the default engine after applying a specific filter.

Helper functions can help implementing policies, e.g.

Policy engine API


doxygen