SAT solutions, including libsolv, is (somewhat surprisingly) not a suitable solution for pip, and Python packages in general, at least at the present time. The Google Doc link in dimino’s comment[1] covers the issues quite thoroughly (at around page 10–12).
What I understand from the RfP is that evaluating work is basically done, and the main work is to integrate the backtracking implementation into pip. But one of the more important task listed IMO is to untangle the current resolver implementation from other pip components. This implies that 1) the new resolver will be a relatively isolated component, allowing code reuse for alternative package managers, and 2) the resolver can more easily switch to a SAT solution when it becomes viable to do so.
Skip to here for a bit more info: https://github.com/pypa/pip/issues/988#issuecomment-55267449...
An explanation of the problem and the solution's approach: https://docs.google.com/document/d/1x_VrNtXCup75qA3glDd2fQOB...