Hi, On Tue, 24 May 2011, Joachim Breitner wrote: > If cases where a conflict (of the non-versioned-kind, i.e. a conflict > only with regard to installability and not with regard to presence in an > suite) has an effect on the migrateability occur often, then this poses > indeed a serious problem. Can we still somehow map this to a SAT > problem? > > The complete solution would involve separate logical atoms for migrating > a package (foo_1234/testing) and for checking installability > (foo_1234/testing/installable_for_foo_1234, > bar_987/testing/installable_for_foo_1234). But for the installability of > each package, the installability of the dependencies have to be solved > independed, causing a quadratic explosion of atoms. Clearly not > possible.
Agreed that it's not possible that way. And I don't see any other way to express it as a SAT problem. 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. --- On another note, I have started some early coding to play with the concept/idea. You can grab it here: git clone git://anonscm.debian.org/~hertzog/sat-britney.git http://anonscm.debian.org/gitweb/?p=users/hertzog/sat-britney.git You can do simple stuff like this: $ python >>> import sat >>> dimacs = sat.DIMACS() >>> dimacs.init_variable("a", False) >>> dimacs.add_implication("!a", "b") >>> dimacs.add_implication("b", "c") >>> s = sat.Solver() >>> s.run(dimacs) (True, {'a': False, 'c': True, 'b': True}) >>> dimacs.init_variable("c", False) >>> s.run(dimacs) (False, None) I shared it to Joachim earlier and he asked me to continue the discussion here. So that's what I'm doing now. 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. > Having more readable operators such as implication, at-most-one and so > on should be the responsibility of the next layer. At least in my > design. It's really early, I have not put much thoughts on the precise design of the objects, I add stuff as I need them. So I'm not attached to the design... feel free to make suggestions, preferrably in the form of patches. :) For now it's not clear to me what your next layer is. Cheers, -- Raphaël Hertzog ◈ Debian Developer Follow my Debian News ▶ http://RaphaelHertzog.com (English) ▶ http://RaphaelHertzog.fr (Français) -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]
