Re: SAT based britney
On Thu, 26 May 2011, Joachim Breitner wrote:
> Am Donnerstag, den 26.05.2011, 11:58 +0200 schrieb Raphael Hertzog:
> > We could instead include it as a "post-process filter". We'd run
> > edos-distcheck on the result to identify what new packages
> > are uninstallable, and from this we could try to identify the
> > supplementary constraint to add.
>
> with identify, do you mean manually (which is also what I am suggesting)
> or automatically?
Automatically if possible.
> Automatically might be difficult. One approach would be to forcibly
> prevent any afterwards non-installable package from migrating, and then
> re-run sat-britney.
The non-installability can be caused on a package that has not migrated by
the migration of another package. So it needs to be more subtle than that.
> But even then the problem needs to be tackled manually later. Or maybe
> the situation is left until the problem dissolves by itself.
Yes, something like that. Either the non-migration causes troubles and I
expect the release managers/maintainer to investigate, or it doesn't cause
troubles and it might go away alone at some point.
> Ah, ok. So this function would actually be used in the next layer (the
> one that takes the readable constraints and feeds them to the
> MAX-SAT-solver).
Yes.
> The rationales for this separation:
> * Layer 1 needs to be fast, so eventually it is likely implemented in C
> using the picosat library.
For now, I'm just calling the picosat executable. What improvement do you
expect by switching to the library?
I guess it might be more convenient (or even required) for the part where
you try to get an answer to "why did this package not migrate". But I fear
that switching to the library means we're loosing a clear interface for
people who want to provide an alternative layer 1. At least we must be
careful to keep a reasonable abstraction on top of it.
> * Implementing the layer 1 interface might be interesting for
> non-Debian-related research parties whose result might be faster than
> anything we come up with. They will likely not want to worry about our
> human-readable syntax.
Somehow this is already the case since we can use any SAT solver provided
we express our problem with a DIMACS file. Or do you expect them to work
specifically on the MAX-SAT problem that we want to implement on top of a
normal SAT solver?
> * Layer 2 does string processing, so is likely not a good fit for C and
> rather something like Perl, Python or Haskell. This is ok as it is not
> doing the actually intensive calculations.
> * Layer 2 is still generic, so might be used (and thus tested and
> improved) by others. This more or less maximizes the non-Debian-specific
> part.
> * If it turns out that layer 3 and layer 2 are implemented in the same
> language (e.g. Ocaml, given the existing Debian libraries, or Haskell),
> it should be possible to combine them in one executable that does not
> actually serialize, write out, write and and parse the constraints but
> pass them around in their abstract form directly, thus saving time and
> space.
Speaking of languages, I picked python because britney2 is in python,
because we have python-apt, and several members of the release team
seem to know/use/appreciate python.
I know Perl & C too, but I'm afraid I don't know Ocaml & Haskell.
I am aware that Ocaml could have been interesting due to its dose3 library.
Cheers,
--
Raphaël Hertzog ◈ Debian Developer
Follow my Debian News ▶ http://RaphaelHertzog.com (English)
▶ http://RaphaelHertzog.fr (Français)
Reply to: