5 ms·

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for t

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

abdullahkhalids 3y ago
Miniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.
- StableAlkyne 3y ago
  Miniconda is faster (I prefer it, personally)... ...but Miniconda and Anaconda are the same package manager, the difference is that Anaconda comes batteries-inclused with a ton of common packages. The reason Miniconda is faster isn't the solver, it's because it doesn't have 250 packages to go through the long checking process on. If you have a large, complex environment in Miniconda, that environment will get slower and slower to resolve over time.
  - taeric 3y ago
    250 is not a big number... :(
- VHRanger 3y ago
  They have the same resolver (Conda) You just have fewer packages installed with miniconda, so the sat problem is much smaller
scoresmoke 3y ago
Yes, this is a big disadvantage. But have you tried Mamba that aims at implementing Anaconda more efficiently? It works really well in most cases. https://mamba.readthedocs.io/ https://mamba.readthedocs.io/
- bouchard 3y ago
  You can use mamba's much faster solver directly with conda. conda install -n base conda-libmamba-solver conda config --set solver libmamba
- StableAlkyne 3y ago
  Mamba is great, and I use it when possible. It's probably the single best thing to happen to Anaconda in years. Nowadays it's installed automatically, but up until a month ago you had to deal with the slow solver to install it. And fortunately it will become the default by Q4! The point I was making is the old solver left an impression on me that SAT is slow and inefficient, that's all really :)
deleted 3y ago
[deleted]
bonzini 3y ago
Fedora's dnf also uses SAT and it's way faster (with caching) than the handwritten resolver it replaced.
mathisfun123 3y ago
> Anaconda's absurdly slow dependency resolver On the one hand this is like comparing apples and oranges. On the other hand SAT is slow for dependency management not because the solver itself is slow (it might well be - I don't know which solver they packaged) but because it's an NP-complete problem. Back to sympy: a computer algebra system (CAS) is primarily (IMHO) an algebra system, not a matrix manipulation library or a pde solver or whatever kitchen sink collection of things is in all of them. Algebra in this context means manipulating algebraic expressions and that's term rewriting and that's also NP-complete (well at least in some form or fashion, eg egraph extraction). So in summary - there's no way out of using SAT/SMT here. > slow, clunky, etc Just to put a finer point on this - it's a very shallow thing to look at conda's or whomever's implementation and then paint over SAT/SMT with that same brush. The way that I usually describe z3 is that it is nuclear weapons grade industrial software. I mean jesus christ its stated goal is solving NP complete/hard problems and it frequently succeeds at this goal on problems with millions of decision variables and clauses. It is absolutely the highest tech piece of tech out there (XYZ pytorch/tensorflow ai ml thing pales in comparison) and we are all extremely lucky that it is licensed permissively and developed completely in the open (and basically by one guy!). And it is being used in many many places for very serious engineering.

abdullahkhalids 3y ago

Miniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.

StableAlkyne 3y ago
Miniconda is faster (I prefer it, personally)... ...but Miniconda and Anaconda are the same package manager, the difference is that Anaconda comes batteries-inclused with a ton of common packages. The reason Miniconda is faster isn't the solver, it's because it doesn't have 250 packages to go through the long checking process on. If you have a large, complex environment in Miniconda, that environment will get slower and slower to resolve over time.
- taeric 3y ago
  250 is not a big number... :(
VHRanger 3y ago
They have the same resolver (Conda) You just have fewer packages installed with miniconda, so the sat problem is much smaller

scoresmoke 3y ago

Yes, this is a big disadvantage. But have you tried Mamba that aims at implementing Anaconda more efficiently? It works really well in most cases. https://mamba.readthedocs.io/ https://mamba.readthedocs.io/

bouchard 3y ago
You can use mamba's much faster solver directly with conda. conda install -n base conda-libmamba-solver conda config --set solver libmamba
StableAlkyne 3y ago
Mamba is great, and I use it when possible. It's probably the single best thing to happen to Anaconda in years. Nowadays it's installed automatically, but up until a month ago you had to deal with the slow solver to install it. And fortunately it will become the default by Q4! The point I was making is the old solver left an impression on me that SAT is slow and inefficient, that's all really :)

deleted 3y ago

[deleted]

bonzini 3y ago

Fedora's dnf also uses SAT and it's way faster (with caching) than the handwritten resolver it replaced.

mathisfun123 3y ago

> Anaconda's absurdly slow dependency resolver On the one hand this is like comparing apples and oranges. On the other hand SAT is slow for dependency management not because the solver itself is slow (it might well be - I don't know which solver they packaged) but because it's an NP-complete problem. Back to sympy: a computer algebra system (CAS) is primarily (IMHO) an algebra system, not a matrix manipulation library or a pde solver or whatever kitchen sink collection of things is in all of them. Algebra in this context means manipulating algebraic expressions and that's term rewriting and that's also NP-complete (well at least in some form or fashion, eg egraph extraction). So in summary - there's no way out of using SAT/SMT here. > slow, clunky, etc Just to put a finer point on this - it's a very shallow thing to look at conda's or whomever's implementation and then paint over SAT/SMT with that same brush. The way that I usually describe z3 is that it is nuclear weapons grade industrial software. I mean jesus christ its stated goal is solving NP complete/hard problems and it frequently succeeds at this goal on problems with millions of decision variables and clauses. It is absolutely the highest tech piece of tech out there (XYZ pytorch/tensorflow ai ml thing pales in comparison) and we are all extremely lucky that it is licensed permissively and developed completely in the open (and basically by one guy!). And it is being used in many many places for very serious engineering.