This is indeed the case. If you want to solve dependencies in a way that works well, you want an index that describes all your available package versions.

While solving dependencies is indeed NP complete, they can be fairly fast in practice because of various specificities : each rule is generally only a few variables, and the rules have a specific form allowing for more efficient rule representation (e.g. "at most one of variable", etc...). In my experience, it is not more difficult than using graph-based algorithms, and

FWIW, at Enthought, we are working on a pure python SAT solver for resolving dependencies, to solve some of those issues. I am actually hacking on it right at PyCon, we hope to have a first working version end of Q2, at which point it will be OSS, and reintegrated in my older project depsolver (https://github.com/enthought/depsolver).