Hi, 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 MAX-SAT-solver). > 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 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. Greetings, Joachim -- 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