Hacker News new | ask | show | jobs
by taeric 1116 days ago
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.

1 comments

Do you know of any python dependency managers that do this?
dnf is (or rather, was) written in Python and uses a SAT solver to solve dependencies for package installs in Fedora.
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. :(

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?
yum used ad-hoc Python code. It was also incredibly slow and often couldn't find a solution.
Isn’t mamba basically Vonda “with a faster silver”?
libsolv is underneath suse and some more Linux distributions. I think conda at some point switched there, too.