Re: [UPLOADED] RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
On Mi, 2011-01-12 at 13:15 +0100, Pietro Abate wrote:
> On Wed, Dec 29, 2010 at 05:06:47PM +0100, Julian Andres Klode wrote:
> > On Di, 2010-12-28 at 16:17 +0100, Pietro Abate wrote:
> > >
> > > Here there is a description of the encoding used by other solvers :
> > > http://mancoosi.org/reports/d4.2.pdf
> > >
> > > It might be an interesting read.
>
> This is another encoding used by zypp...
> http://en.opensuse.org/openSUSE:Libzypp_satsolver_basics
>
> They are using minisat (another sat solver) and hardcoding heuristics
> to find a good solution in the problem encoding. I'm not sure if they
> run the solver multiple times (restart) to refine the solution.
The picosat-based solver is based on that document, although it may not
do everything in the correct way. But they wrote their own specific
solver (sat-solver) instead of using a general one. My solution started
as a proof of concept that I can use a general-purpose SAT solver to
find sane solutions.
> Another interesting encoding is the one used in apt-pbo (there are a
> couple of articles on the web, easy to find). This one uses minisat+
> (not packaged in debian) that is a pseudo boolean solver built on top of
> minisat where you can spacify the optimization function (ex: paranoid,
> trendy, etc) along side with the problem encoding.
minisat+ does not seem to be maintained, and the performance does not
appear to be acceptable from what I read.
So while all this stuff is good in theory, in practice it does not get
us anywhere without a library implementing it which has a compatible
license, and stable enough API and ABI. For my purposes, less than or
equal to LGPL-2.1 restrictions and written in C; for APT-only purposes a
library written in C++ and GPL-2 compatible is also acceptable.
Most solvers shared in source form seem to be undocumented, without
license notes, and not suitable for libraries - completely unusable for
many people, except maybe its author (at least for a short amount of
time, until they forget how it works).
[OPINION]
And many solvers are written in C++ and/or by Windows users, both good
indicators of idiots at work - yes, good C++ code can exist, but as C++
is a large[1] piece of shit[2], most code written in it is as well[3].
[1] They can't seem to have enough features
[2] Linus:
"C++ is a horrible language. It's made more horrible by the fact
that a lot of substandard programmers use it, to the point where
it's much much easier to generate total and utter crap with it.
Quite frankly, even if the choice of C were to do *nothing* but
keep the C++ programmers out, that in itself would be a huge
reason to use C."
[3] The same as 2
[/OPINION]
--
Julian Andres Klode - Debian Developer, Ubuntu Member
See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
Reply to: