On 07/01/2011 10:25 PM, Raphael Hertzog wrote: > 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.
That's already an option in britney2. This SAT based design seems overcomplex due to all the special casing AFAICT. I also don't buy that a Conflicts relationship should be special instead of a plain one like now. I won't stop anyone from experimenting with a SAT based solution, though from a release point of view, I think it would be better to start using britney2 and kill its bugs (which unfortunately will take some time AFAICS) before diving into a SAT based adventure. Cheers Luk -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]
