Re: SAT based britney - formalisation of the problem
Hi again,
On Thu, Jun 23, 2011 at 01:06:44PM +0200, Joachim Breitner wrote:
> > 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.
>
> Correct. That is why I suggested to use the format already used in a
> MAX-SAT competition:
> http://maxsat.ia.udl.cat/requirements/
In fact, from out point of view the DIMACS format or MAX-SAT input
format are already a specific encoding technique, and we think that
one should first find a logical specification of what exactly one
tries to achieve, before thinking about a specific encoding into
MAX-SAT or whatever other solver technology. One way of formalising
this could be stated in the following style:
1) one defines first a certain abstraction of a distribution (like
ignoring certain kinds of conflicts). This has of course to be exactly
defined. Lets call this function a().
2) lets say that the result of migration a set m to a testing distribution
t is denoted as "t+m"
3) then you say: you look for a migration set m, such that for the
testing distribution t:
every "interesting" installation request that is satisfiable in a(t)
is also satisfiable in a(t+m)
Ideally, a() would be the identity function, that is no abstraction
at all.
The important question here would be to define what are precisely the
"interesting" installation requests. Candidates are:
- install one arbitrary single package A. This seems to be the definition
currently used in britney.
- install an arbitray *set* of packages together. This might be interesting
in some cases, but seems to be too restrictive.
Another element of the precise specification would be: one wants to
have a maximal solution. What precisely is the sense of maximality here?
Maximal number of binary packages? Maximal number of source packages? Should
there be a way to give more weight to more "important" packages?
Cheers -Zack and Ralf.
--
Ralf Treinen
Laboratoire Preuves, Programmes et Systèmes
Université Paris Diderot, Paris, France.
http://www.pps.jussieu.fr/~treinen/
Reply to: