Re: [UPLOADED] RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
- To: Julian Andres Klode <jak@debian.org>
- Cc: Michael Tautschnig <mt@debian.org>, APT Development Team <deity@lists.debian.org>, Daniel Burrows <dburrows@debian.org>
- Subject: Re: [UPLOADED] RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
- From: Pietro Abate <Pietro.Abate@pps.jussieu.fr>
- Date: Wed, 12 Jan 2011 13:15:24 +0100
- Message-id: <[🔎] 20110112121524.GA10850@uranium.pps.jussieu.fr>
- In-reply-to: <1293638807.7501.16.camel@jak-thinkpad>
- References: <1293039140.16550.36.camel@jak-thinkpad> <1293126621.2353.84.camel@jak-thinkpad> <1293542056.3085.69.camel@jak-thinkpad> <20101228133317.GA4876@l04.lan> <20101228142125.GA9930@uranium.pps.jussieu.fr> <1293547642.28690.9.camel@jak-thinkpad> <20101228151755.GA14500@uranium.pps.jussieu.fr> <1293638807.7501.16.camel@jak-thinkpad>
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.
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.
pietro
--
----
http://en.wikipedia.org/wiki/Posting_style
Reply to: