Re: [UPLOADED] RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
On Di, 2010-12-28 at 15:21 +0100, Pietro Abate wrote:
> hello.
>
> On Tue, Dec 28, 2010 at 02:33:18PM +0100, Michael Tautschnig wrote:
> > > * picosat prefers B in A | B if B > A (higher version ID wins)
> >
> > picosat doesn't care. If either of them poses a valid solution, it will give you
> > one of them. Which of them is chose purely depends on heuristics implemented in
> > picosat (might even be tied to the literal ids). If you want it to prefer a
> > different solution, that has to be encoded.
>
> The problems about the quality of the solution produced by a SAT solver
> is exactly what I meant when I said that picosat probably is not going
> to be the best choice here. The upgrade/installation problem is by
> nature an optimization problem. The solvers of the misc competition are
> all able to accept a function that allow you to express the use
> preferences or optional constraints.
>
> There are techniques to encode these preferences in SAT (like with
> minisat+), but I don't think this is the way to go. SAT solvers are only
> concerned about the existence of a solution, while here we want to find
> a good solution (among an exoneponental number of possible solutions) that
> respect your constraints.
Not really, you can declare literals more or less important than others
which deals with almost every case I throw at it.
/* Keep manually installed packages or installed packages that are
* candidates on the system and non-candidates away if possible. */
if (is_installed && (!is_automatic || cand == ver))
picosat_set_more_important_lit(var(ver));
else if (!is_installed && cand != ver)
picosat_set_more_important_lit(var(ver));
The solver will first try to solve the problems by setting non-candidate
versions to -1 and installed versions (manually installed or candidates)
to 1 and then trying other solutions.
>
> > > * picosat does not allow for optional clauses, Recommends are thus
> > > treated as Depends. I should ask them if they are interested in
> > > adding this.
> > What would be the semantics of "optional clauses" in terms of Boolean
> > satisfiability? What I could envision, however, is adding additional clauses
> > after the first round of solving the problem for Depends, using incremental SAT
> > solving. Add one of the Recommends at a time and see whether the problem can
> > still be solved. My question here would in particular be which semantics users
> > can expect from "Recommends" - will these packages always be installed or just
> > as many as possible or ...? As a user of apt I'd expect that either all of them
> > or none of them gets installed (depending on my apt config). Therefore I don't
> > see any need for "optional clauses", but I have to admit that I'm not that much
> > into apt development.
>
> You can easily encode "optional clauses" with the misc solver just
> giving to these clauses a different weigth in the search strategy.
> Certainly you can came up with nice encodings in SAT, but again, I think
> this is not the right tool here.
You can encode an all-or-nothing solution as (-VER | -RECOMMENDS | A |
B) and fine-grained solutions as (-VER | -RECOMMENDS_i | A_i | B_i). And
then removing RECOMMENDS from the set of assumptions if they have no
solution. Or you can solve the problem incrementally.
>
> The entire idea about cudf is to let an external tool to deal with the
> encoding of the problem and decouple apt from all these low level
> issues. Using picosat and hard encoding optimization criteria in apt is
> basically going toward the same slippery slope of using an, abelit
> advanced, custom solution solver as we have now in apt.
CUDF solvers are nice, but not a substitute for a good default solver.
--
Julian Andres Klode - Debian Developer, Ubuntu Member
See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
Reply to: