Re: SAT based britney - formalisation of the problem
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
Reply to: