On: Modern SAT solvers: fast, neat and underused (2018)

[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 → nemetroid]

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 → taeric]

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

[taeric → nemetroid]

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

[nemetroid → taeric]

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.

[taeric → nemetroid]

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?

[rwmj → taeric]

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