Re: SAT based britney
Hi,
On Sun, 15 May 2011, Joachim Breitner wrote:
> No, that should be no problem. Versioned constraints are resolved
> precisely to the list of existing concrete packages which fulfill the
> requirement before the resulting constraint being passed to the
> SAT-solver, so no irregularities there. As long as the invariant that
> for each binary package, there is exactly one version in testing, is not
> overwritten manually then the migratability of A and B means A is
> installable and B is installable using the same set of packages. 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.
> 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?
Cheers,
--
Raphaël Hertzog ◈ Debian Developer
Follow my Debian News ▶ http://RaphaelHertzog.com (English)
▶ http://RaphaelHertzog.fr (Français)
Reply to: