Re: SAT based britney - formalisation of the problem
Hi,
On Wed, 29 Jun 2011, Ralf Treinen wrote:
> In fact, from out point of view the DIMACS format or MAX-SAT input
> format are already a specific encoding technique, and we think that
> one should first find a logical specification of what exactly one
> tries to achieve, before thinking about a specific encoding into
> MAX-SAT or whatever other solver technology.
But we're looking into having some concrete prototype in the short term
and I don't think that this kind of formalization will help us in that
regard. And I don't really see the expected benefits of this approach
either...
> Another element of the precise specification would be: one wants to
> have a maximal solution. What precisely is the sense of maximality here?
> Maximal number of binary packages? Maximal number of source packages? Should
> there be a way to give more weight to more "important" packages?
It would be nice to take the popularity into account indeed and give them
priority in terms of migration.
But really this is just a cherry on the top. If we already get something
working that gives a coherent set of package that can move without manual
hints, it would be great.
Cheers,
--
Raphaël Hertzog ◈ Debian Developer
Follow my Debian News ▶ http://RaphaelHertzog.com (English)
▶ http://RaphaelHertzog.fr (Français)
Reply to: