Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Solver improvements: 1) use CryptoMiniSat as the default SAT solver #7694

mbargull opened this Issue Aug 26, 2018 · 4 comments


None yet
4 participants
Copy link

mbargull commented Aug 26, 2018

@mbargull mbargull referenced this issue Aug 26, 2018


Solver improvements: meta issue #7700

1 of 7 tasks complete

This comment has been minimized.

Copy link

wolfv commented Sep 24, 2018

Hi @mbargull I saw your comments on the linked issues. The improved speed of the new SAT solver looks great.

However, I am wondering if other solutions have been considered?

Specifically, the SAT solver coming out of OpenSUSE, which is used by other distros such as Fedora, could be a very interesting alternative:

I am no expert and there might be downsides. But I could only find libsolv referenced in one comment on some other PR.


This comment has been minimized.

Copy link
Member Author

mbargull commented Sep 24, 2018

Hi @wolfv,

thanks for the suggestion! It's somewhat similar to @domoritz's comment in #7239 (comment):

If the solving algorithm is slow, it might be interesting to look into a powerful constraint solver such as

So, my answer in #7239 (comment) also applies to your question:

Thanks for the link. For the long-term I can imagine it could make sense to abstract and factor out all that dependency/constraint resolution. But currently there is some Conda-specific special handling happening in the code which makes this a bit more complicated. So this is nothing we can change any time soon, IMO.

Plus #7239 (comment):

why you think this can't be expressed as constraints in a general language like ASP?

Oh, it's not that I don't think it can be expressed that way. I think it would be a nice thing to do, in fact. My comment was more directed toward that some parts of conda's code are written in a "Conda specific way" (for lack of words..). Meaning, it might take some effort to entangle those bits and I'd be surprised if someone would be willing to take this on any time soon :/. (Plus there is some part, called features, that is not very well integrated into the overall dependency resolution process with channel priorities and all -- we have to solve this problem before we do any other substantial changes there, IMO.)
Overall, I don't think it would be tremendous witchcraft to translate the problem with an appropriate DSL, but we'd need someone that has the time and knowledge to do so, I think


This comment has been minimized.

Copy link

domoritz commented Sep 24, 2018 is an amazing solver and it has a conda package ( Clingo forms the basis of (which you can use to solve package resolution in debian and ubuntu, see


This comment has been minimized.

Copy link
Member Author

mbargull commented Sep 27, 2018

@wolfv, @domoritz, I opened gh-7808 such that your suggestions are tracked in an own issue since this one is more for the (hopefully) short-term integration of CMS.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.