The alternative Python package manager "Conda" does use a SAT solver, which sounds elegant at first but can be frustrating when it runs into slow-to-resolve situations. (This happens frequently, which is why I no longer use Conda on my machines).
"Solves" in what sense? Dependency resolution is an NP-hard problem; if the tool you're using is guaranteed to run quickly, then either (1) there are cases it can't handle but conda can, or (2) the tool's author has just proven P=NP.
It is NP-hard, but realistically that should not be a concern for most dependency management questions users throw at it? Just how many variables are folks imagining are in a typical dependency tree?
Google claims the average number of dependencies is 35. My gut is most of these do not have too many versions, all told. Is this really big enough that you'd expect it to be the bottleneck?
The original Conda solver is just badly optimized, whether through the implementation or a poor language choice. For years, user performance concerns were written off as just the price you pay for the correctness of an SAT.
Mamba was a third party rewrite that was a couple orders of magnitude faster. Users started leaving Conda for Mamba. It scared the Conda developer enough that they dropped whatever invisible back-end features they were prioritizing, and within months they added a feature to install different dependency resolution libraries, targeting Mamba first.
The Conda package manager is available to users of the Anaconda/Miniconda distribution, which is very popular. Conda uses a sat solver for dependency resolution. It's a lot slower than pip, but it's not a thing that has to happen often enough for that to be a problem.
It's a good thing, however, that using conda doesn't preclude one from also using pip.
I wouldn't be surprised if pip had a SAT solver as a dependency.
The alternative Python package manager "Conda" does use a SAT solver, which sounds elegant at first but can be frustrating when it runs into slow-to-resolve situations. (This happens frequently, which is why I no longer use Conda on my machines).
https://www.anaconda.com/blog/understanding-and-improving-co...
Mamba is a drop in replacement for conda which solves that.
"Solves" in what sense? Dependency resolution is an NP-hard problem; if the tool you're using is guaranteed to run quickly, then either (1) there are cases it can't handle but conda can, or (2) the tool's author has just proven P=NP.
It is NP-hard, but realistically that should not be a concern for most dependency management questions users throw at it? Just how many variables are folks imagining are in a typical dependency tree?
Google claims the average number of dependencies is 35. My gut is most of these do not have too many versions, all told. Is this really big enough that you'd expect it to be the bottleneck?
The OP probably means "solved" as in "faster."
The original Conda solver is just badly optimized, whether through the implementation or a poor language choice. For years, user performance concerns were written off as just the price you pay for the correctness of an SAT.
Mamba was a third party rewrite that was a couple orders of magnitude faster. Users started leaving Conda for Mamba. It scared the Conda developer enough that they dropped whatever invisible back-end features they were prioritizing, and within months they added a feature to install different dependency resolution libraries, targeting Mamba first.
It probably has a heuristic for it
SAT solvers are great for when you want to create space in your day for idly thinking about the halting problem.
When it comes to sat solvers I have to recommend this excellent video: backwards game of life https://youtube.com/watch?v=g8pjrVbdafY
I think pip’s current resolving backend (resolvelib) doesn’t do any SAT solving.
Is the opposite possible? I mean to have the dependency resolver use a sat solver? Would it be faster/slower?
The Conda package manager is available to users of the Anaconda/Miniconda distribution, which is very popular. Conda uses a sat solver for dependency resolution. It's a lot slower than pip, but it's not a thing that has to happen often enough for that to be a problem.
It's a good thing, however, that using conda doesn't preclude one from also using pip.
Conda indeed is slow. However, mamba is a drop in replacement for Conda and uses a way faster solver, which makes it a lot more palatable.
Does it use a sat solver that has better average-case behavior, or does it sacrifice on full sat solvability?
Totally possible. Some dependency resolvers use a sat solver. The speed depends on the solver and optimizations in the solver vs resolver.
This was a fun read, very ignobel spirit!