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

Re: SAT based britney


Am Donnerstag, den 26.05.2011, 11:58 +0200 schrieb Raphael Hertzog:
> On Tue, 24 May 2011, Joachim Breitner wrote:
> That said, I'm not sure we need to deal with it from the start at the SAT
> solver level.
> 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 might be difficult. One approach would be to forcibly
prevent any afterwards non-installable package from migrating, and then
re-run sat-britney. But even then the problem needs to be tackled
manually later. Or maybe the situation is left until the problem
dissolves by itself.

> Joachim wrote:
> > Am Mittwoch, den 25.05.2011, 12:06 +0200 schrieb Raphael Hertzog:
> > > Next I want to add some functions like add_implication(a, b)
> > > that would convert the common boolean constraints the we want
> > > to handle to CNF.
> > 
> > Hmm, not sure if this should be added at this layer. I’d rather have
> > implemented the MAX-SAT part on top of picosat using a minimal, CNF
> > syntax. This keeps this part simple and easy to replace with more
> > powerful implementations.
> I don't see what it changes here. The DIMACS object stores all the
> information in plain CNF format. The add_implication() is just a
> convenience function to feed the data.

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

> For now it's not clear to me what your next layer is.

Here is my three-layering-idea, concisely put:
 1. A max-sat-solver, with input and output in DIMACS format.
 2. A still generic wrapper that takes human-readable clauses and has
support for things like "A implies one of B C D", "at most one of A B
C", "not C" as constraints. When you replace A, B,... by atoms like
ghc_7.0.3-1_amd64/testing, then these constrains become intelligible.
 3. The Debian specific part, which takes the Packages/Sources and
generates the readable constraints, and further interprets the result to
pass it to dak.

The rationales for this separation:
 * Layer 1 needs to be fast, so eventually it is likely implemented in C
using the picosat library.
 * 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.
 * 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
 * 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


Joachim "nomeata" Breitner
Debian Developer
  nomeata@debian.org | ICQ# 74513189 | GPG-Keyid: 4743206C
  JID: nomeata@joachim-breitner.de | http://people.debian.org/~nomeata

Attachment: signature.asc
Description: This is a digitally signed message part

Reply to: