I think the statistical methods would be better compared to a sat solver like Z3. Prolog gives you more flexibility, but it isn't going to be able to use the advanced search techniques that Z3 can take advantage of. Optimizers like Optaplanner are in sort of the same family as Z3, but they often trade being better at optimization for the ability to quickly find solutions, particularly if the number of solutions is small.
In my experience, seeing OptaPlanner pitted against the other best-of-the-best enterpise-grade solvers, OptaPlanner wins when scaling out - very clearly. Not when scaling down. This is the nature of the Local Search algorithms.
