[zypp-devel] Current cases which Zypp doesn't handle well?
Hello all, I quite like the fact that Zypp uses a SAT solver to do its dependency generation. However, I'm curious if there are any situations which you have encountered where Zypp does a poor job, from a solving or usability perspective. For example, are there any cases where your heuristic for dealing with degrees of freedom does poorly? Any places where the language of boolean formulas is not expressive enough (e.g. you want integer ranges or comparisons?) Some context: I recently happened upon this project: http://www.cs.wm.edu/~tdillig/mistral/index.html And it seems like it adds some features to SAT solvers that would be really useful for package managers: in particular, it has an "explain" module which can take some desired end-result (conclusion) and the current state (hypothesis), and find the minimal set of extra hypothesis necessary to reach the end-result. This seems to more directly correspond to the package solving problem, so I'm interested in comparing the two approaches! Thanks, Edward -- To unsubscribe, e-mail: zypp-devel+unsubscribe@opensuse.org To contact the owner, e-mail: zypp-devel+owner@opensuse.org
On Fri, Dec 14, 2012 at 11:14:01PM -0800, Edward Z. Yang wrote:
I quite like the fact that Zypp uses a SAT solver to do its dependency generation. However, I'm curious if there are any situations which you have encountered where Zypp does a poor job, from a solving or usability perspective.
Well, I don't know of any, but as I'm the author, I'm a bit biased ;)
For example, are there any cases where your heuristic for dealing with degrees of freedom does poorly?
libsolv (the solver library used by zypp) uses a very simply heuristic: - it tries to keep the currently installed packages (unless the solver job says otherwise) - if there are choices, it always goes for the "best" package. This normally matches what the user expects, if new packages have to be downloaded and installed, they will be the newest ones, thus saving extra work later on.
Any places where the language of boolean formulas is not expressive enough (e.g. you want integer ranges or comparisons?)
For the package dependencies, we don't really need integer ranges. They would be useful to minimize some metric the user provides, but libsolv doesn't do that (see above).
Some context: I recently happened upon this project:
http://www.cs.wm.edu/~tdillig/mistral/index.html
And it seems like it adds some features to SAT solvers that would be really useful for package managers: in particular, it has an "explain" module which can take some desired end-result (conclusion) and the current state (hypothesis), and find the minimal set of extra hypothesis necessary to reach the end-result. This seems to more directly correspond to the package solving problem, so I'm interested in comparing the two approaches!
Thanks for the link, I didn't know about mistral before. I'm looking forward to your comparison. Cheers, Michael. -- Michael Schroeder mls@suse.de SUSE LINUX Products GmbH, GF Jeff Hawn, HRB 16746 AG Nuernberg main(_){while(_=~getchar())putchar(~_-1/(~(_|32)/13*2-11)*13);} -- To unsubscribe, e-mail: zypp-devel+unsubscribe@opensuse.org To contact the owner, e-mail: zypp-devel+owner@opensuse.org
Excerpts from Michael Schroeder's message of Mon Dec 17 18:07:41 +0700 2012:
For the package dependencies, we don't really need integer ranges. They would be useful to minimize some metric the user provides, but libsolv doesn't do that (see above).
The funny thing about metrics is, while they seem like a good idea, it's often hard to get the users to actually articulate their utility functions. I wonder what metrics you actually would want. Edward -- To unsubscribe, e-mail: zypp-devel+unsubscribe@opensuse.org To contact the owner, e-mail: zypp-devel+owner@opensuse.org
participants (2)
-
Edward Z. Yang -
Michael Schroeder