Conda is still unbearably slow. Mamba is a vastly better mostly drop-in replacement.

Second this. Not only is it faster, but the error messages in Mamba are much more helpful and sane.

Great! Conda honestly can't die fast enough.

Curious to hear about your preferred alternative. Poetry?

spack

Poetry, pip, nix or manually writing the bits into memory. It really doesn't matter as long as it's not the hellscape that is conda.

That was always a bit of a red herring, from my understanding. Yes, if you poorly model something into an ad hoc SAT solver, expect slowness.

Which is a bit of the general idea of these being underused. If you can get your problem into a SAT form or three, than feed it to a state of the art solver, it can work amazingly well. But, you will be spending a lot of time moving to and from the SAT formulation.

Do you know of any python dependency managers that do this?

I don't. That said, I think the problems are typically small enough that you don't gain much by hunting for a good SAT formulation? Python doesn't do anything that any other dependency manager does. (Does it?)

DNF uses a SAT solver. It’s even listed first among the motivations for creating DNF:

> DNF is a fork of Yum 3.4 that uses libsolv via hawkey for a backend. The main goals of the project are:

> * using a SAT solver for dependency resolving

> ...

https://fedoraproject.org/wiki/Features/DNF

Fun, I'll have to look at that. The major implication, though, is that yum does the same thing without an explicit sat formulation. Right?

Edit: I will note that the linked doc is silly old. And it seems that the original proposed replacement for YUM was Hawkeye, and is deprecated? But DNF is still steaming ahead? I didn't find any obvious links talking about performance. Did the SAT idea pan out? I'd almost think it was a bust, with some of these wikis. :(

yum used ad-hoc Python code. It was also incredibly slow and often couldn't find a solution.

Yes, DNF has replaced Yum by now and definitely uses SAT internally. Here's a link that's probably even older, but more informative:

https://en.opensuse.org/openSUSE:Libzypp_satsolver

Any evidence that the sat formulation helps over the choice of not python? My hunch is it was also somewhat naive python?

I'm not sure what kind of evidence that would be. Version selection is NP-complete, so there is no known algorithm that efficiently solves all problem instances.

You can spend time looking really hard at the problem instances you have and identifying common patterns, and write a complex algorithm that works well as long as the dependencies you are trying to solve at least sort-of follow these patterns. This usually works well until it fails completely, at which point you can look really hard for new patterns in new use cases, and make your complex algorithm handle those as well.

But there's also the option of turning your problem into a SAT (or answer set programming, or constraint programming, or integer programming, etc.) formulation, using an existing SAT solver, and not have to write any complex algorithm at all.

Evidence that it is faster than non sat formulations? So, npm? Whatever go does? Poetry/pip? Java/maven? Or have all of those migrated to sat?

libsolv is underneath suse and some more Linux distributions. I think conda at some point switched there, too.

Isn’t mamba basically Vonda “with a faster silver”?

dnf is (or rather, was) written in Python and uses a SAT solver to solve dependencies for package installs in Fedora.

From this and Dart, I think one of the lessons here is that SAT solvers are the wrong technique for solving dependencies. SAT solvers find “better” solutions by some metric, but humans using package managers want something which is both simpler and faster.

As an example:

Schaefer's dichotomy theorem shows that, when possible, just make sure to use Horn clauses when possible.

Takes a bit of thinking but is superior to huristics or SAT solvers if you can refactor to allow for it.

Wait, this is very relevant to some work I’ve been doing recently, how do you conclude that Horn clauses should be preferred from Schaefer’s theorem?

Isn't it just that Horn clauses are easy to understand, and they are guaranteed to be fast.

Take a look at https://en.wikipedia.org/wiki/Boolean_satisfiability_problem... (based on Schaefer's "The complexity of satisfiability problems"). Horn clause satisfiability problems (HORN SAT) fall in P-c.

Oh right this is just Horn clauses, not CHCs

Not sure if related, to Schaefer's theorem, but I dove into Answer Set Programming [1] recently, which follows this approach, enabling the use of fast-ish SMT solvers, which are a generalization of SAT solvers! Boolean/Propositional Logic is to Predicate Logic as SAT is to SMT. There's a very nice course about it from the developers of Potassco, one of the best open source Answer Set Programming framework [2].

The syntax looks like Prolog, but predicate negations are a first class citizen, avoids infinite loops.

Prolog's approach is like a depth first search through a search tree -- ASP is like a nondeterministic turing machine, exploring all branches simultaneously from the bottom up.

[1] https://en.wikipedia.org/wiki/Answer_set_programming

[2] https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfi...

Dart as in the language? Dart uses a SAT solver: https://github.com/dart-lang/pub/blob/master/doc/solver.md

My gut is that was the point? That Dart uses a SAT solver to no discernible advantage.

I will also note that this amuses me to no end. If you have enough dependencies that you need the speed of a SAT solver.... how many dependencies do you have? And why are they changing so dang much?

The ship of complexity has long sailed for many projects.

I imagine most individual projects are still low enough in dependencies that you still have to try for that to be the slow part.

Also there had been a growing trend for most popular packages to offer precompiled wheels on PyPI instead of just sdist releases.

This meant that people who had moved to Conda because they couldn't get Pip to install important packages into their environment took another look and found that actually they could get things installed using Pip now.

At the same time Pip also got a resolver allowing you to have install time confidence you're not installing conflicting package, and recently (Pip 23.1+) the resolver's backtracking got pretty good.

That said Conda mostly solved this (and once mamba is the default resolver engine things will be really fast), Pip is not ever going to be a package manager, and Poetry still isn't an environment manager, and most other Python package/installer alternatives to Conda won't do things like install your Jupyterlab's nodejs dependency.

After many years I now almost exclusively use Pip to install into an environment, but still nothing beats Conda for bootstraping the non-Python-package requirement's (such as Python itself) nor for getting things working when you are in a weird environment that you can't install OS dev libraries into.

Is Conda actually moving towards making mamba the default? Last I heard, they were distinctly uninterested in that, since mamba is implemented in C++, and they would rather rely on their own slow Python code, which they can more easily modify.

Yes they are, it's been integrated and stable in conda since last year, you can turn it on with a solver config set: https://www.anaconda.com/blog/a-faster-conda-for-a-growing-c...

the problem wasnot using a sat solver but how they used it.

many package dependency managers use sat solvers since suse spearheaded this in 2007/2008 with libsolv, which is blazing fast for large repositories.

https://research.swtch.com/version-sat