5 ms·
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 pytho
by jjoonathan 3y ago
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 | / - | \
- teruakohatu 3y agoConda is still unbearably slow. Mamba is a vastly better mostly drop-in replacement.
- ubj 3y agoSecond this. Not only is it faster, but the error messages in Mamba are much more helpful and sane.
- rowanG077 3y agoGreat! Conda honestly can't die fast enough.
- taeric 3y agoThat 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 3y agoDo you know of any python dependency managers that do this?
- taeric 3y agoI 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 3y agoDNF 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 https://fedoraproject.org/wiki/Features/DNF
- taeric 3y agoFun, 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. :(
- klodolph 3y agoFrom 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 3y agoAs 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.
- xavxav 3y agoWait, 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?
- thomasahle 3y agoIsn't it just that Horn clauses are easy to understand, and they are guaranteed to be fast.
- Karrot_Kream 3y agoTake a look at https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Schaefer's_dichotomy_theorem 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 3y agoOh right this is just Horn clauses, not CHCs
- weavermarquez 3y agoNot 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 https://en.wikipedia.org/wiki/Answer_set_programming [2] https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfilqPUgpClMKYu https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfi...
- notatallshaw 3y agoAlso 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 3y agoIs 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 3y agoYes 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-community https://www.anaconda.com/blog/a-faster-conda-for-a-growing-c...
- froh 3y agothe 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 https://research.swtch.com/version-sat