Re: [UPLOADED] RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
On Di, 2010-12-28 at 16:17 +0100, Pietro Abate wrote:
> On Tue, Dec 28, 2010 at 03:47:22PM +0100, Julian Andres Klode wrote:
> > > The entire idea about cudf is to let an external tool to deal with the
> > > encoding of the problem and decouple apt from all these low level
> > > issues. Using picosat and hard encoding optimization criteria in apt is
> > > basically going toward the same slippery slope of using an, abelit
> > > advanced, custom solution solver as we have now in apt.
> > CUDF solvers are nice, but not a substitute for a good default solver.
>
> My sugestion here was more to adopt a cudf solver as default solver
> (possibly as a dynamically linked library) rather then reinvent the
> wheel and re-encode the upgrading problem yet again with picosat. The
> people competing in the misc competition put a lot of efforts to came up
> with very optimized encondings of the problem.
>
> If you look at it a cudf solver is just
>
> - a cudf parser (there are already independent
> implementations of it in c / c++ / python / ocaml)
> - the problem encoding (this is the important and creative/difficult part)
> - an off-the-shelf solver (there are many around, here you just want to
> pick the best avalaible)
>
> using picosat effectively is writing yet another encoding of the problem
> using picaosat a sat solver... By since you are using a pure sat solver
> you will be forced to encode the problem in pure sat that is too low
> level for the nature of the problem. Nothing against it. I'm just trying
> to give you the picture and the state of art.
> If you adopt one solver as default solver of course you won't need to
> feed it cudf, but you could use build the internal data structure by
> hand exatcly as you are doing with picosat.
For a linked-in solver, the following points must be true:
* GPL-2 compatible license
* Acceptable performance
* C/C++ API, and no dependencies except for libc, libstdc++
* A documented API
* In Debian
My personal wishlist for use in other projects as well:
* LGPL-2.1 compatible license
* C API, no dependency except for libc
I never said that the picosat solution will stay, it's just one proposal
that I started to implement because it was in the archive, and has a
simple API. Once there are other solvers in the archive, we can
implement them as well, and choose the best solution at the end.
--
Julian Andres Klode - Debian Developer, Ubuntu Member
See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
Reply to: