[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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).


> 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.

Raphaël Hertzog ◈ Debian Developer

Follow my Debian News ▶ http://RaphaelHertzog.com (English)
                      ▶ http://RaphaelHertzog.fr (Français)

Reply to: