Hi, Am Montag, den 16.05.2011, 11:44 +0200 schrieb Raphael Hertzog: > On Sun, 15 May 2011, Joachim Breitner wrote: > > And in > > the absence of conflicts, this means that A and B are co-installable. > > Yes, but what about this, T is the package we're considering to migrate. > > T depends on A, B > A depends on D1 | D2 > B depends on D2 | D3 > D1 conflicts with D3 > D2 is not satisfiable/installable in testing (but is in unstable) > D1 is installable alone in testing > D3 is installable alone in testing > > That said, I don't know if the current britney would detect anything wrong > here either. There is a conflict, so I’m not claiming to handle this perfectly. I hope such cases are rare. And note that my system allows for manual addition of rules, so if we come across situations that are treated insufficiently, and such situations are rare enough, additional constraints can be added by the RM team. E.g. in this case, after some thought, the additional constraint "T implies D2" should be sufficient. > > Yes, I had things like this in mind. Also, it should be able to handle > > multi-way-transitions between several suits > > (unstable/testing/cut/volatile/stable-updates) with invariants that > > should hold across different suites (e.g. a package in cut may not be > > older than the one in testing) in one run. That is why I have added the > > suffix /testing in the proposed syntax. > > I'd rather start with small objectives and build up if it works well. :-) > > I started looking up some of the literature around SAT solver. I suppose > you are more familiar with the topic than me. > > Did you have some ideas of how to implement all this? > > We have quite some SAT solvers in Debian and they all seem to support > the DIMACS format as input (which requires to transform all boolean > constraints to CNF). But they give a solution or they return > unsatisfiable. > > You mentioned the possibility to do several "iterations" to implement a MAX-SAT > solver. Can you elaborate? Here is my proposal of using a regular SAT solver to solve PMAX-SAT in the way we want, with an additional overhead linear in the number of desired atoms (not great, but maybe still good enough in practice): Run MAX solver once and get at one satisfiable set (this should exist, in the worst case it is migrate nothing. If it does not, then testing is broken and the RM team has to remove some constraints, e.g. for a broken package, the constraint that at least some version of a package has to exist. This has the effect of allowing it to be dropped from testing if needed). Then take all desired atoms (i.e. migrations) set to true, and add them as axioms to the set of clauses. Take one atom not set to true, and also force it true. If satisfiable, we know this can migrate and we repeat with the next atom. This might set other desired atoms to true, for example if the package was part of a larger migration that the initial run did no migrate – great, less work to do. Try setting the next desired atom to true. If not satisfiable, we get a minimal unsatisfiable core. This is the explanation why this package cannot be migrate. In further runs we set this atom to false (which probably only has the effect of speeding things up) and try setting the next desired atom to true. If the SAT solver can be tricked, e.g. by default assignments, picosat has such an option, to set a lot of desired atoms to true in the first run, the number of iterations might be low. If this turns out to be insufficient, we will need help from theoretical computer scientists. But my plan would be to implement this DIMACS-based PMAX-solver algorithm with a DIMACS-like interface to have something to work with, and then improvements below this layer can be implemented independent of the rest of the sytem. 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