Re: SAT based britney - formalisation of the problem
On Fri, 01 Jul 2011, Luk Claes wrote:
> That's already an option in britney2.
>From what I understood the auto-hinter is limited to a few simple cases.
> This SAT based design seems overcomplex due to all the special casing
> AFAICT.
What special casing?
> I also don't buy that a Conflicts relationship should be special
> instead of a plain one like now.
They are special only in the sense that they can't be represented
as part of the SAT problem and thus need to be taken into account
while creating the SAT problem to hand over to a SAT solver.
> 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.
They are not mutually exclusive. :)
Cheers,
--
Raphaël Hertzog ◈ Debian Developer
Follow my Debian News ▶ http://RaphaelHertzog.com (English)
▶ http://RaphaelHertzog.fr (Français)
Reply to: