[jjoonathan]

I seem to recall that a poorly scaling sat solver in conda-forge broke so badly in 2020 that it shifted the tectonic plates underneath the entire academic python ecosystem away from conda and towards pip.

    Solving Environment | / - | \

[taeric]

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.

[theLiminator]

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

[rwmj]

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

[taeric]

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?)

[nemetroid]

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

[taeric]

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. :(

[nemetroid]

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

[rwmj]

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

[wodenokoto]

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

[froh]

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

[beecafe]

https://github.com/mamba-org/mamba

[klodolph]

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.

[nyrikki]

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.

[weavermarquez]

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...

[xavxav]

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?

[Karrot_Kream]

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.

[xavxav]

Oh right this is just Horn clauses, not CHCs

[thomasahle]

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

[tgamblin]

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

[taeric]

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?

[g8oz]

The ship of complexity has long sailed for many projects.

[taeric]

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

[teruakohatu]

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

[ubj]

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

[rowanG077]

Great! Conda honestly can't die fast enough.

[Macuyiko]

Curious to hear about your preferred alternative. Poetry?

[rowanG077]

Poetry, pip, nix or sending out butterflies to bend cosmic rays to write bits into memory. It really doesn't matter as long as it's not the hellscape that is conda.

[fock]

spack

[froh]

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

[notatallshaw]

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.

[unnah]

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.

[notatallshaw]

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...