Guix and Nix don’t actually solve constraint problems, though. By design, they omit the dependency resolution that other package managers do, and humans manage

Guix and Nix don’t actually solve constraint problems, though. By design, they omit the dependency resolution that other package managers do, and humans manage the dependencies. If you want to change versions, you need to do some hacking to update things and propagate requirements through the package graph. You could think of Spack (github.com/spack/spack) as a nix/guix-like model, but with a solver. Spack uses ASP (which is prolog-like but reduces to SAT with optimization) but packages are written in an embedded python DSL.