[HN Gopher] Solving Boolean satisfiability and integer programmi...
___________________________________________________________________
Solving Boolean satisfiability and integer programming with Python
packaging
Author : mmaaz
Score : 74 points
Date : 2024-11-25 00:17 UTC (1 days ago)
(HTM) web link (mmaaz.ca)
(TXT) w3m dump (mmaaz.ca)
| amelius wrote:
| I wouldn't be surprised if pip had a SAT solver as a dependency.
| philipkglass wrote:
| 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...
| curiousgal wrote:
| Mamba is a drop in replacement for conda which solves that.
| akoboldfrying wrote:
| "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.
| worewood wrote:
| It probably has a heuristic for it
| StableAlkyne wrote:
| 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.
| taeric wrote:
| 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?
| __MatrixMan__ wrote:
| SAT solvers are great for when you want to create space in your
| day for idly thinking about the halting problem.
| woodruffw wrote:
| I think pip's current resolving backend (resolvelib) doesn't do
| any SAT solving.
| dvh wrote:
| When it comes to sat solvers I have to recommend this excellent
| video: backwards game of life
| https://youtube.com/watch?v=g8pjrVbdafY
| mmaaz wrote:
| On that note, uv, which I found to be orders of magnitudes
| faster (pip fails to solve even some small SAT/IP instances)
| uses something called PubGrub
|
| https://docs.astral.sh/uv/reference/resolver-internals/#reso...
| ziofill wrote:
| Is the opposite possible? I mean to have the dependency resolver
| use a sat solver? Would it be faster/slower?
| scheme271 wrote:
| Totally possible. Some dependency resolvers use a sat solver.
| The speed depends on the solver and optimizations in the solver
| vs resolver.
| philipov wrote:
| 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.
| SimplyUnknown wrote:
| 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.
| philipov wrote:
| Does it use a sat solver that has better average-case
| behavior, or does it sacrifice on full sat solvability?
| 3abiton wrote:
| This was a fun read, very ignobel spirit!
| mmaaz wrote:
| Thanks!
| ris wrote:
| This is a fun article, but the whole "dependency resolution
| problem" is a bit of a wild goose chase anyway, because the
| underlying data you're basing it all on (what package authors
| publish as their version constraints) is only slightly better
| than junk. For a start, python (like most ecosystems) is very
| limited in its ability to express compatibility constraints -
| it's not even able to understand the concept of stable branches
| that receive backports.
|
| Add to that most package authors putting about a second's thought
| into their version constraints, with other package authors being
| overzealous and for example thinking it's their duty to protect
| you from security vulnerabilities through their version
| constraints, and I frequently doubt the worth of putting all this
| SAT wizardry into these tools, as fun as it is.
| mmaaz wrote:
| I think this is a criticism about the general Python ecosystem,
| but the article has nothing to do with what other package
| authors do or security vulnerabilities etc. It converts SAT to
| "dependency resolution" by creating a bunch of dummy packages
| and dependencies that map back to the SAT instance. And it's
| definitely just for fun, I highly doubt it's useful except as
| an exercise in NP-complete reductions :)
___________________________________________________________________
(page generated 2024-11-26 23:01 UTC)