Re: SAT based britney
Hi,
Disclaimer: I'm not a member of the release team.
On Wed, 11 May 2011, Joachim Breitner wrote:
> * Do you get it? (i.e., did I explain it well enough or are there
> questions left)
I think so.
> * Do you think it can handle all current and anticipatable
> requirements? (I’m not involved in release team work and might missed
> some conditions.)
You mention that the tool can't deal properly with Conflicts for ensuring
installability. I wonder if there aren't more similar problems related
to this requirement of keeping package installable.
For instance, I wonder how you'd deal with alternative dependencies? I can
imagine that you can find out solutions where each package can be
individually installed but where both sets of dependencies are not
co-installable (in particular if you solve some dependencies with
different versions of the same binary package, and here Conflicts is not
involved).
I don't know how britney does it either, but I know that it tries to never
lower the resulting installability count of testing.
> * What do you think of the advantages and improvements that I point
> out?
To me it looks great but I have no experience with SAT solver and I
wonder whether the sheer amount of predicates that it will have to handle
will not result in something dog-slow.
> * Is it worth the hassle?
Given your description, it doesn't look like too complicated to implement.
I think it's worth trying at least if we are not able to find conceptual
problems (or if we can solve them).
> And before going into the details, here the high-level goals that I want
> to achieve with SAT-britney (stupid working title):
All of the goals outlined are great IMO.
> The system is three-layered. On the lowest level is a general purpose
> MAX-SAT-solver. It takes as input a propositional formula in conjunctive
> normal form with some variables, and a list of “desired” variables. It
Presented that way, it corresponds exactly to what is needed to implement
the rolling distributions described in
http://lists.debian.org/debian-devel/2011/05/msg00275.html
Maybe it can be a good testbed for the concept.
> * a satisfying assignment which is maximal, i.e. there is no satisfying
> assignment where a strict superset of desired variables is true.
FWIW, Britney tries to migrate packages one by one, starting with the most
important packages. It doesn't consider them all together.
> dependencies etc. It also needs to get the age and buggyness data. The
> result of the solver will be used to create the new set of packages for
> testing (how does this work, by the way – does britney create a new
> Packages file, does she create a .changes file processed by dak or even
> another way?). Initially, it could just create a large hint that can be
britney generates a Heidi file. It has this format:
<package> <version> <architecture>
<architecture> can also have the special value "source" for the source
package. The heidi file is then fed to "dak control-suite".
> So here is my heuristic to handle this: If a Conflicts or Breaks has an
> upper version constraint, then add a corresponding clause. If not,
> ignore it.
>
> This might lead to uninstallable packages in testing in corner cases
> (imagine some package depending on both exim4 and postfix), but such a
> case is clearly an RC bug that ought to be filed by someone and which
> would be detected by a run of edos-distcheck on unstable already.
I think it's more likely that such problems happen with conflicting
dependencies further down in the dependency tree (i.e. not directly on the
same package).
> what would migrate. Assume this RC bug is fixed, what would change). But
> maybe so slow that it still can be used for britney, but only with one
> run per migration (how often do packages migrate per day?).
I think it's twice a day currently.
> PS: Please give honest feedback. I’d rather been told that this is
> rubbish and not spend time on it than spending time on it and afterwards
> noticing that it will not be used.
Remember my feedback is one of an (interested) outsider, I have almost no
experience feeding hints to britney.
Cheers,
--
Raphaël Hertzog ◈ Debian Developer
Follow my Debian News ▶ http://RaphaelHertzog.com (English)
▶ http://RaphaelHertzog.fr (Français)
Reply to: