[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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.

Reply to: