Question: is there a reason we would choose a solver like this instead of encoding the effects in prolog and let it generate plans for us? Why would one approach be better than the other?
Prolog does not, by default, remember conflicts and avoid them. Solvers do, most of them.
Look for Conflict-Driven Clause Learning (CDCL) SAT solvers for one example. The pseudoboolean and integer programming solvers and optimizers learn cutting planes marking subspaces where no (better) solution exists, for another example.
Question: is there a reason we would choose a solver like this instead of encoding the effects in prolog and let it generate plans for us? Why would one approach be better than the other?