Re: [UPLOADED] RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
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 exponental number of possible solutions) that
respect your constraints.
> > * 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.
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.
p
--
----
http://en.wikipedia.org/wiki/Posting_style
Reply to: