Is the opposite possible? I mean to have the dependency resolver use a sat solver? Would it be faster/slower?

The Conda package manager is available to users of the Anaconda/Miniconda distribution, which is very popular. Conda uses a sat solver for dependency resolution. It's a lot slower than pip, but it's not a thing that has to happen often enough for that to be a problem.

It's a good thing, however, that using conda doesn't preclude one from also using pip.

Totally possible. Some dependency resolvers use a sat solver. The speed depends on the solver and optimizations in the solver vs resolver.