[gentoo-dev] Re: SAT-based dependency solver: request for test cases

[Martin Vaeth]

Michael Lienhardt <michael.lienhardt@×××××××.net> wrote:
>
> ad-hoc fixes and tweaks that can hardly be encoded into SAT constraints.

The main difficulty which I see is that one does not want only _some_
solution, but among all solutions one which optimizes certain quantities.
So it seems to me that a discrete optimization under constraints
is required instead of a pure SAT solver (although formally, of course,
such an optimization problem can be reduced to SAT, I do not know whether
you went the road):

a. The number of packages which change their status (from installed to
uninstalled or vice versa) should be minimal.

b. Similarly, the number of USE-flag changes necessary to achieve this
aim should be minimized.
(You didn't tell whether your solver already supports such changes,
but when it is finished, it definitely should.)

Hopefully in near future, there will be a second class of USE-flags
whose change is "cheap" which should be excluded from this minimization
restriction:
https://bugs.gentoo.org/show_bug.cgi?id=424283
I think the main reason why nobody dared to implement them yet
(although almost everybody wants them) are exactly these implications
on the current solver in portage which nobody dares to change anymore
seriously.

c. A solution with dependency loops should be avoided if possible
(which is why currently the PDEPEND hacks do exist: To tell the solver
which loops are not a problem.)

d. In || ( ... ) clauses the left-most packages should be preserved.
There are similar (and more difficult) rules for REQUIRED_USE.

e. Last but not least: The preferences are ordered a > b > c > d
(A dependency loop of uninstalled packages should probably have even
higher priority than a).
Additionally the change installed -> uninstalled should be less
"expensive" than the change uninstalled -> installed.
The correct weighting of the quantities should probably be a matter
of discussion (or preferrably even user-customizable), and preferrably
should not depend only on the number of packages but also on other
customizable quantities (e.g. the package size).

Perhaps - if one can rely on some solver - in a future EAPI instead
of the size heuristic, one could give a hint for how "expensive" it
is to recompile a certain package, so that dependency results can
be better optimized for that.

IIRC, this is already built in rudimentarily in portage's current
solver by defining the recompilation costs of virtual packages as 0.

> I don't deal with installation order [...] circular dependency problem

++
Once the packages are known, the installation order and breaking of
unavoidable circles is a matter of a single graph traversal in the
resulting subgraph which needs neglectable linear time.
However, if there is a solution without a circle this should have
been found instead in the first place (cf. c).