APT SAT solvers and stuff [WAS: Re: Bug#683786: apt-get cross build dependency resolution of arch:all, m-a:none packages]
On Mon, Aug 06, 2012 at 01:05:13AM +0200, David Kalnischkies wrote:
> (We have a big FIXME for this in the build-dep code and I hope to get
> this code replaced by reusing our "normal" solver more, so this might
> get better in the future, but probably never really solved until we have
> a SAT (or its technical superior successor [invented by me] XYZ) solver…)
On the topic of solvers: SAT solvers don't really work. A pure SAT solver
cannot handle unsatisfiable recommends. APT currently ignores recommends
that cannot be satisfied which is a good thing to do. A SAT solver cannot
do this (this needs a PMAX-SAT solver). As a standard SAT solver also
cannot really do global optimization, it's probably not that cool for
dependency handling (we would need a partial weighted max sat solver
if I recall correctly).
As an alternative, you can use pseudo-boolean optimization (set of
hard constraints and a global sum to minimize/maximize). This works
rather well, at least clasp can solve most problems with good
results in sufficient time. There are some problems with overflows
in the scores for the optimization function, though. I used a PBO
encoding derived from that found in Mancoosi, but slightly
simplified.
Furthermore, it seems that libsolv has rudimentary Debian support (by
parsing sources.list and Packages files itself, and broken support
for some architectures). I don't know whether it might be worthwhile
to integrate APT with libsolv (by making libsolv generate its structures
using the apt-pkg library instead of ad-hoc self-parsing) and use that for
solving dependencies, and I don't know how it handles unsatisfiable
Recommends. If it can handle that, and produces good results, it
might be a good idea to work on this for jessie.
And if anyone has other good GPL-compatible solvers for PWMAX-SAT or
PBO written in C or C++ I could look at, that would be helpful as
well. What is needed for integration with APT would be (in my
opinion):
(a) good enough performance
(b) GPL-compatible license
(c) reporting on why things can't be satisfied
(d) A library written in C or C++ with relatively stable API
(e) No global state used between function calls, that is,
the ability to have multiple solver instances.
(f) Active upstream development
I can work-around (e) easily enough using fork() and some shared
memory magic, though. And a non-library solution might also work,
if it can be made a library later on.
--
Julian Andres Klode - Debian Developer, Ubuntu Member
See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
Reply to: