The new architecture of pkgng solver

[Vsevolod Stakhov]

Hello,

At the moment I plan to do the following:

1)
- introduce 'the universe' structure, which contains all deps (for 
install/fetch/upgrade), rdeps (for deinstall), conflicts and their rdeps 
(for install);
- add request list - a list of packages to install, remove or upgrade
- write universal solver code that takes universe and a request list and 
then either produces cudf output or uses an internal SAT solver;
- results are written into two lists: packages to add/upgrade and 
packages to remove (e.g. due to conflicts).

2)
Plan 'provides' logic that means that a dependency can be provided by a 
number of (potentially conflicting) packages. It is implemented as pkg 
field but it is not used by solver.

3)
Internal solver should work based on the following procedure:

1. Iterate over the universe and create a boolean problem:
  * A depends on B that is provided by B1, B2 or B3 is transferred to a 
set of rules: (!A | B1 | B2 | B3)
  * A conflicts between B1, B2 and B3 is transferred to the following: 
(!B1 | !B2) & (!B1 | !B2) & (!B1 | !B3)
  or in case of conflict to a provided feature if A conflicts with B 
provided by B1, B2 or B3:
(!A | !B1) & (!A | !B2) & (!A | !B3)

2. Explicit requests for install or remove are written as:
(A) - install A
(!A) - remove A

3. For all explicit request (e.g. install A) set the value of these 
requests either to true (for packages to install) or false (for packages 
to deinstall).

4. Iterate over the record and set all unary rules to true, for example
(A) & (!A | B1 | B2 | B3) & (!A | !C) which means that A depends on (B1 
or B2 or B3) and conflicts with C. After this step we set A to TRUE as 
it is unary rule.

5. For all other rules perform propagation procedure, substitute 
variables to make a rule as true. For example in the previous example:
  * (A) & (!A | B1 | B2 | B3) & (!A | !C) - A is TRUE;
  * (!A | !C) - !C should be TRUE as !A is FALSE and C thus is FALSE;
  * (!A | B1 | B2 | B3) - !A is FALSE, so one of B1/B2/B3 should be TRUE.

6. For the last step there is a choice, what to select. I'd suggest to 
follow this logic:
  * try installed packages first;
  * do not install any packages that are not needed (e.g. set all 
available alternatives to FALSE);

7. Check the overall expression and if it is FALSE try to reassign the 
last assigned variable from the previous step.

8. 6 and 7 till the expression is either TRUE or there is no way to 
reassign variables (unsolvable solution).

With this logic we have only a single problematic point - how to convert 
the packages universe and request to a SAT problem. On the other hand, 
with this architecture we have a *universal* solution for all procedures 
(install/remove/upgrade). Moreover, it is compatible with CUDF format, 
therefore I suggest to rework the current jobs architecture to this one.

I'll do it if there are no objections.

(And, well, we need to think eventually what to do with share libraries 
dependencies and flexible dependencies, e.g. Depends: libsomething (>1.4))

-- 
Vsevolod Stakhov