The underlying implementation of the main classical part of the solvers are fairly similar. See for example the overview of how to implements such systems by th

The underlying implementation of the main classical part of the solvers are fairly similar. See for example the overview of how to implements such systems by the main authors of SICStus Prolog and Gecode in https://chschulte.github.io/papers/schultecarlsson-cph-2006.html https://chschulte.github.io/papers/schultecarlsson-cph-2006.... . Choosing a solver to solve a specific problem comes down to experience, familiarity, available global constraints, and suitability for the problem and implementation environment at hand. With that said, solvers such as OR-Tools (in their newer CP-SAT engine) and Chuffed are using something called Lazy Clause Generation, which can be very effective for many problems. This is partly a newer way to implements CP solvers that uses a built-in SAT solver as the domain store. I know of no Prolog system that uses this architecture.