Solving Boolean satisfiability and integer programming with Python packaging (opens in new tab)

This is a fun article, but the whole "dependency resolution problem" is a bit of a wild goose chase anyway, because the underlying data you're basing it all on (what package authors publish as their version constraints) is only slightly better than junk. For a start, python (like most ecosystems) is very limited in its ability to express compatibility constraints - it's not even able to understand the concept of stable branches that receive backports.

Add to that most package authors putting about a second's thought into their version constraints, with other package authors being overzealous and for example thinking it's their duty to protect you from security vulnerabilities through their version constraints, and I frequently doubt the worth of putting all this SAT wizardry into these tools, as fun as it is.

I wouldn't be surprised if pip had a SAT solver as a dependency.

Is the opposite possible? I mean to have the dependency resolver use a sat solver? Would it be faster/slower?

This was a fun read, very ignobel spirit!