> Building a SAT solver into the package manager seems to be a solution in search of a problem.

I can't tell you which ones off the top of my head, but I'm sure a number of package managers do use constraint solvers to find dependencies matching the constraints.