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