Re: SAT based britney
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)
Reply to: