Graph-based solver based on primitives
This is a playground for a new solver based on a multigraph (graph in the following).
The graph consists of nodes and edges.
Each node is a set of versions.
Each edge connects one node to an ordered group of nodes (an or group), and has a weight. The weights are +1 for depends, 0 for recommends, and -1 for conflicts).
The root node has no versions, but depends on all manually installed packages and all packages selected for installation. To be precise, for each installed package, there is an edge root -> installed|candidate.
The goal of the solver is to iteratively apply the primitives until the graph only contains one node. If the graph becomes empty, the problem was unsolvable.
Reduction Primitives
These primitives reduce the graph to a smaller one, but do not change satisfiability.
Merge helper: Two nodes can also merged by creating a new node with the union of the edges of both nodes, and the union of the package sets of the nodes.
Edge unification
If there exists two edges a->X and b->Y where X and Y are Or groups, and there are paths root->D1->..->Dn->a and root->D'1->..->D'm->b where D1..Dn and D'1 and D'n are single choice groups, and X is a subset of Y, then the edge b->Y is replaced by the edge b->X.
Cycle elimination
If there is a cycle of the form a->D1->...->Dn->a where all D1..Dn are single choice groups, the nodes a and Dn are merged into a node {a, Dn}.
Subsumption
If there exists a node that only has a single parent, the node is merged with the parent.
Root subsumption
Any node n for which there exists an positive edge root->n is subsumed by the root, but different to normal merge, any positive edges p->n for any node p are eliminated, as are all nodes m with negative edges m->n.
This behavior is different from normal subsumption to avoid introducing cycles on the root node.
Conflict elimination
If there is a positive path of the form root->D1->...->Dn->a where all D1..Dn are single choice groups (a "must install a" scenario"), any nodes n with negative edges n->a must be removed.
Unsatisfiable choice elimination
If there is a negative path of the form root->D1->...->Dn->a where all D1..Dn are single choice groups (a "must not install a" scenario"), any edges p->X are replaced by edges p->X\a.
No choice elimination
If there is a edge a->{} (an unsatisfiable dependency), the node a is eliminated from the graph.
Branch primitives
Branch primitives restrict the search space, but may lead to unsatisfiability. They only apply to non-negative edges.
The solver should record the graph before running branch primitives so it can backtrack if the choice turned out unsatisfiable.
Choice
The choice primitive finds the smallest Or group in the graph and picks one of the choices.
Choice Elimination
If there is an edge a->x|Y and we tried x but did not gain a result, the edge is replaced by a->Y.
Caveats
The solver cannot remove manually installed packages, it will report an error of not being able to satisfy dependencies or conflicts.
How do I tell the user which conflict caused a resolution failure?