Hello,
sorry for dropping in late in this discussion, but we learned only
recently that this discussion was going on on debian-release. We have
discussed a bit the proposal within the Mancoosi team in Paris; I will
try to reply from the point of view of the team (hence, the "we").
In short:
- we are generally in favor of using existing logical formalisms and
resolver engines for this kind of problems.
- however, we think that the testing migration problem is harder than
SAT solving.
The package installation problem (as routinely solved by the SAT-based
edos-distcheck monitor [1]) 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 [2].
[1] http://edos.debian.net/weather/
[2] http://www.computer.org/portal/web/csdl/doi/10.1109/ASE.2006.49
Even oversimplifying, the testing migration problem is:
find a subset of the set of migration candidates
such that for all packages x in testing after performing this migration
there is a coherent subset of testing that contains x
That, is the structure is "exists-forall-exists", instead of just
"exist". This should yank the problem out of NP-complete into some
higher level in the polynomial hierarchy. And this is letting aside the
even harder problem of finding the "best" subset---as opposed as finding
just one such subset---in accordance to the goals of the release team.
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.
Besides this principal scepticism some more specific remarks:
- having all packages installable in testing is a noble goal, however
during a release cycle it typically gets lost even in i386, and has to
be restored by the release team before the release. Even then it is
usually not satisfied on the less popular architectures, at least not
for arch:all packages (see [3]). For this reason one probably would
rather want to say something like: any package that was installable
before the migration should also be installable after the
migration. This also includes the constraint that the migration
process should not remove packages from testing (unless intervention
by the release team). Otherwise, a maximal solution could imply to
migrate 2 packages to testing and to remove one.
[3] http://edos.debian.net/edos-debcheck/stable.php
- About efficiency: as Mark said, modern SAT solvers are extremly
efficient. However, one should not forget that one has to consider all
architectures in parallel, that is we need a solution that works on
all achitectures. You would have at least one variable per package in
testing, plus one per migration candidate plus variables for source
packages and probably also for virtual packages. This would yield, as
a very rough estimate, 50k variables, multiplied by 11 release
architectures gives 550k variables. And that's a lot.
All that considered, this mail does not want to be a dissuasion in
trying this out. Our experience has shown that there are indeed
communities of researchers and practitioners out there which are very
much interested in trying their solvers against "real" problem instances
coming from realities like Debian.
For instance, the MISC competition we have set up [4] to attack the
"package upgrade problem" on top of the CUDF format [5] has given great
results in terms of new solvers and encoding techniques; such results
are now flowing into Debian package managers [6]. It might be possible
to setup a similar virtuous cycle that will challenge researchers to
attack the testing migration problem and we are actually interested in
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.
[4] http://www.mancoosi.org/misc-2011/
[5] http://www.mancoosi.org/cudf/primer/
[6] http://packages.debian.org/experimental/apt-cudf
On behalf of the Mancoosi group in Paris,
Ralf Treinen
Stefano Zacchiroli
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
Attachment:
signature.asc
Description: Digital signature