Re: [UPLOADED] RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
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. Cudf IHMO is a nice
abstracion, but in the end is just a way to allow solver poeple to focus
only on the interesting part of the problem without dealing with other
low level details. As apt-get upstream if of course in your (our)
interest to adopt the best solution brewed by the misc competition and
integrate it at a lower level of abastraction in apt-get. Maintaing a
cudf interface of course will be a plus as will give ppl the possibility
to keep playing with other solvers if the want to and to advance the
state of art.
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.
my 2 cents.
p
--
----
http://en.wikipedia.org/wiki/Posting_style
Reply to: