Bug#761948: ITP: libsolv -- dependency solver using a satisfiability algorithm

[Michael Tautschnig <mt@debian.org>]

Hi Mike,

[...]
> >> Search the internet  for 'sat solver' to get links to the theory behind it.
> >> .
> >[...]
> >
> >Is there any chance the package could be refactored such as not to
> >exclusively
> >rely on the built-in SAT solver? Debian presently ships (at least) sat4j,
> >Minisat and PicoSAT as competitive (i.e., participating in the SAT
> >competition)
> >solvers. As this is C source, linking against PicoSAT would likely be the
> >easiest of those.
> >
> >Best,
> >Michael
> 
> This question actually needs to be directed to upstream, I fear.
> 

Yes, of course. And it's not of immediate urgency/importance. But upstream's
note (the bit on "Search the internet" quoted above) sounds like a pretty
ignorant variant of "RTFM." I consider it "ignorant," because there are
off-the-shelf SAT solvers available (and packaged, as said) so IMHO this should
really be "we ship our own SAT solver, but you can also use existing solvers x y
z."

> Please note: libsolv is not intended (by me) to integrate or use
> other solvers already present in Debian. It is a dependency of
> libzypp which will provide the shared library for (open)SUSE's
> zypper package management tool.
> 
> The reason for bringing this into Debian is to provide obs-build as
> a service on Debian machines (as I already wrote in my original ITP
> message).
> 

Got that and I think this is perfectly fine. But maybe, as future maintainer of
that package (for Debian) you could get in touch with upstream for their own (!)
benefit as libsolv might then arrive at even faster dependency solving.

Best,
Michael