[yochem]

No way pip actually is a really inefficient SAT solver!

[stabbles]

For a long time it was not because there was no backtracking.

Now it is just an exhaustive, recursive search: for the current package try using versions from newest to oldest, enqueue its dependencies, if satisfied return, if conflict continue.

[taeric]

If there was no backtracking, that implies it couldn't solve every sudoku? That is rather amusing with the implication that it couldn't solve every dependency, as well?

[fernandotakai]

uv actually talks about this in their resolver docs https://docs.astral.sh/uv/reference/resolver-internals/