Explore ways to use other solvers instead of interacting with SAT solver directly

[mbargull]

There have been some suggestions for alternatives to the direct invocation of the SAT solver, namely libsolv and aspcud/clingo.

Though this is not something I expect to be addressed any time soon, it would certainly be interesting to see how those other solvers behave and perform! If some ambitious individuals want to look into trying those out within conda, they'd have to dig into conda.resolve.Resolve and essentially translate every interaction with the conda.common.logic.Clauses instances to what the other solvers expect and deal with how to express the multiple solving passes via some similar prioritization scheme.

refs:

• libsolv:

  • From @QuLogic in https://github.com/conda/conda/issues/1338#issuecomment-148310255:

    Write a lightweight, fast, open source, Python MILP or Pseudo-boolean optimization solver that beats out the thing conda is using.

    libsolv (possibly with hawkey for the Python API)? It's specifically created for package dependency solving. It might need some tweaking to read the conda package database, but the solver is pretty fast (e.g., I can tell it to install ~5000 texlive packages and it can leave out the 200 installed packages, determine the 250-300 conflicts and spit out the remaining in a matter of seconds.)

  • From @wolfv in https://github.com/conda/conda/issues/7694#issuecomment-424008271:

    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: https://github.com/openSUSE/libsolv

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

  • From @wolfv in https://gitter.im/conda/conda?at=5ba8fbfe0cfe7f30f1dfddca:

    Another question: I see that a switch of the SAT solver is discussed Was libsolv ever considered? it's the solver made for package management, coming out of SUSE and being used by fedora inside dnf apparently maybe that library could simplify conda greatly as it also already has a notion of repositories

• aspcud/clingo

  • From @domoritz in https://github.com/conda/conda/issues/7239#issuecomment-407127381

    If the solving algorithm is slow, it might be interesting to look into a powerful constraint solver such as https://potassco.org/aspcud/.

  • From @domoritz in https://github.com/conda/conda/issues/7694#issuecomment-424050753:

    https://github.com/potassco/clingo is an amazing solver and it has a conda package (https://github.com/potassco/conda). Clingo forms the basis of potassco.org/aspcud (which you can use to solve package resolution in debian and ubuntu, see https://potassco.org/aspcud/).

[wolfv]

The folks from libsolv react really friendly in this thread: https://github.com/openSUSE/libsolv/issues/284

Maybe we can get something going in this direction?

[peschue]

I have some experience with clingo and use the Conda clingo package a lot. I was wondering about the concrete idea which part of the Conda code you were considering to replace.

I have seen an abstraction from logical operations in conda.common.logic.Clauses. With clingo, a solution could contain a few logic program modules for representing certain reasoning tasks, common.logic.Clauses would not exist anymore.

What do you mean with the following?

[...] deal with how to express the multiple solving passes via some similar prioritization scheme.

Do you mean the following multi-criteria optimization in Resolve.solve?

• Removed packages: minimize count resolve.py#L961

• Requested packages: maximize versions resolve.py#L968

• Track features: minimize feature count ... and so on ...

Multi-criteria optimization is built into clingo so this code would be represented as constraints with different levels and weights and all resolved in one solver optimization.

What I could not find out immediately (and that is also interesting for a potential libsolv integration): from where is Resolve actually used? Is it only the following four calls in core/solve.py ssc.r.bad_installed(...), ssc.r.get_conflicting_specs(...), ssc.r.get_conflicting_specs(...), and ssc.r.solve(...)?

[wolfv]

Personally, without knowing each solver very well, I feel that it would be more robust and future proof to go with a solver that is decidedly made for package management, has been alive since 15 years, has backing from serious companies (Red Hat (Fedora), openSUSE, ...), and where the community of libsolv has shown a lot of interest in helping/adding features for the conda project (see the conda gitter channel) vs e.g. clingo as an academic project where there is a non-negligible risk that the maintenance burden will fall on the conda project if the authors are done with the research.

I think it would be pretty cool if @mbargull or @kalefranz could talk to the libsolv guys and see where this could be going.

[peschue]

Just for completeness I would like to mention that aspcud is a dedicated package dependency resolver tool based on clingo that is integrated into the Debian and Ubuntu apt package manager infrastructure. The tool was made by the clingo developers dedicated for that purpose and uses the CUDF format for describing packages and their dependencies. I do not know if CUDF is compatible with the way Conda represents packages and dependencies but it could be an interesting standard to look at, with existing standard solutions for resolving conflicts and dependencies. (I am neither affiliated with CUDF nor with clingo but I think a clean interface between package management systems and solvers is a good idea.)

[msarahan]

Sorry for the delay here. I'm trying to dig into this a bit. I took a look at CUDF - I think this sort of thing is the right approach, as it will allow more solvers to support a single kind of input, and that will allow conda to use more solvers. I have asked on the libsolv issue above to learn more about how libsolv does these kinds of things.

More discussion of aspcud at https://github.com/ocaml/opam/issues/1800 More interesting yum/libsolv/dnf discussion here: https://news.ycombinator.com/item?id=9560270

We're also curious about the Z3 SMT solver from Microsoft, https://github.com/Z3Prover/z3

Above all, we're looking to engineer this better than we did the first time around. We need to make it easier to map conda's "MatchSpec" and solving priorities concepts to other solvers more than we need to adapt that stuff to one single alternative solver.

[QuLogic]

That HN discussion seems to be about yum/dnf, not libsolv really. And pretty old.

[dimpase]

it would be good to have an idea about the size of computational challenges one faces there, given that SAT problems are in general hard to solve. E.g. at the moment it seems that http://doc.sagemath.org/html/en/installation/conda.html basically gets stuck in "solving environment", and I really want to know why.

Any way to dump the underlying SAT problem in some format?

[wolfv]

@dimpase you can get some information (and some sort of progress indication) by adding -vvv to conda. That turns on the highest verbosity level.

I just tried your command on conda and it does indeed take very long (I didn't let it finish). If you are not aware, we (@QuantStack) have started to prototype a conda that's based on libsolv. For the moment it's called mamba and you can get it from conda-forge:

conda install mamba -c conda-forge
mamba create -n sage sage -c conda-forge

This was executing for me in less than a second (after downloading the repository data).

[msarahan]

Conda 4.7.1 is also quite a bit faster. It's on conda-canary channel right now. It has some "channel churn" issues where if you specify channels on the CLI with -c, conda doesn't preserve existing packages well enough. If you only do one create command, or if you set your channels in .condarc or with conda config, you should be fine.

If you haven't already, please read https://www.anaconda.com/understanding-and-improving-condas-performance/ for more ideas on what you do to improve things. In particular, using the strict channel priority setting can help a lot.

conda config –set channel_priority strict

[dimpase]

while mamba create -n sage sage -c conda-forge completed very quckly, it resulted in a broken install due to python 3 assumed(?). Is mamba a complete drop-in replacement, in the sense that one can use python=2/3 ?

[wolfv]

yes, you can force 2.7 by doing mamba create -n sage sage python=2.7 -c conda-forge

I quickly checked and there seems to be a version of sage 8.3 explicitly pointing to python 3.6. Contrary to miniconda2/3 we don't default to one of the two python versions and currently just pick the latest. This behavior could be changed quite easily.

if you find your installation being broken, please head over to the mamba repo (https://github.com/QuantStack/mamba) to report the issue over there :)

[dimpase]

well, I still have a crash at startup after doing the latter, but OK, this is just a sagemath packaging problem in conda, I suppose. Perhaps @isuruf knows more about it.

[github-actions[bot]]

Hi there, thank you for your contribution to Conda!

This issue has been automatically marked as stale because it has not had recent activity. It will be closed automatically if no further activity occurs.

If you would like this issue to remain open please:

1. Verify that you can still reproduce the issue in the latest version of Conda

2. Comment that the issue is still reproducible and include:

   • What version of Conda you reproduced the issue on
   • What OS and version you reproduced the issue on
   • What steps you followed to reproduce the issue

3. It would also be helpful to have the output of the following commands available:

   • conda info
   • conda config --show-sources
   • conda list --show-channel-urls

NOTE: If this issue was closed prematurely, please leave a comment and we will gladly reopen the issue.

In case this issue was originally about a project that is covered by the Anaconda issue tracker (e.g. Anaconda, Miniconda, packages built by Anaconda, Inc. like Anaconda Navigator etc), please reopen the issue there again.

Thanks!