Re: SAT based britney
On Wed, 22 Jun 2011, Stefano Zacchiroli wrote:
> The package installation problem (as routinely solved by the SAT-based
> edos-distcheck monitor ) is: find a subset of the repository that is
> coherent (satisfies all dependencies and conflicts) and contains the
> wanted package. This is a typical NP-complete problem, due to the
> presence of both disjunctive dependencies and conflicts .
>  http://edos.debian.net/weather/
>  http://www.computer.org/portal/web/csdl/doi/10.1109/ASE.2006.49
Can we have a copy of this article?
> This analysis, of course, relies on the assumption that package
> dependencies can be arbitrarily complex, with inter-related conflicts
> and alternative dependencies. As Joachim and others have already pointed
> out, conflicts are not really taken into account in his proposal. Maybe
> it is indeed possible to find a good approximation of the problem by
> ignoring conflicts and doing some subsequent repair-step, by hand or
> automatically. However, we have problems of understanding what exactly
> the justification of such an approximation would be. Can we really make
> any assumptions on what kind of conflicts would be RC bugs, and hence do
> not have to be taken into account? If we can find such assumptions then
> we should probably cast them into policy. How to deal with conflicts
> seems to be a crucial point to evaluate the proposal in more depth.
I'm not sure I underestand so I'll reformulate and you'll tell me if I
got it right.
You're suggesting that one way to legitimately ignore the problem of
Conflicts would be to have the Debian policy only allow usage of Conflicts
for cases that cannot create problems during testing migration. Is that
I'm not sure how you can formally define whether a Conflicts is likely to
create migrations problems or not.
However we know the common use cases for Conflicts and it seems to me that
they are ok:
1/ conflict for files that have moved within binary packages of the same
source, policy requires the conflicts/breaks to be versionned, and the
simple rule that requires all the binary packages of the source to
be moved together makes it moot
2/ conflicts for files that have moved between binary packages of
different sources, policy requires the conflicts/breaks to be
versionned, and the problem can be solved prior to the definition of
the SAT problem by adding a supplementary rule that forces the upgrade
of both source packages together
3/ permanent conflict for a service provided, the various conflicting
packages are usually alternatives in dependencies (via virtual
packages) and as such there's very few dependency trees that would
force to have two conflicting packages together
4/ permament conflict for a random file conflict that has not yet been
solved by renaming one side. This should be temporary.
To mitigate the problem we could however do some special analysis on
non-versionned conflicts before generating the SAT problem to see whether
the situation of conflicting packages changed between testing and
unstable: if yes we might want to do a first run that does not introduce
new Conflicts in testing.
> helping out with that. But according to our experience, for it to happen
> the problem should not be underestimated and, more importantly, should
> be properly formalized in a way which is independent of some specific
> encoding technique.
Can you be more explicit?
Is DIMACS the "specific encoding technique" that you're referring to?
If yes, how else should the problem be formalized?
Raphaël Hertzog ◈ Debian Developer
Follow my Debian News ▶ http://RaphaelHertzog.com (English)
▶ http://RaphaelHertzog.fr (Français)