Not really because of the cut operator. It can be optimized with tricks like tabling, but changing the evaluation order is generally unsafe. I think a larger as

Not really because of the cut operator. It can be optimized with tricks like tabling, but changing the evaluation order is generally unsafe. I think a larger aspect is that a SAT/SMT solver introduces an even more confusing black box than Prolog's evaluation strategy. You can reason about the performance of Prolog programs in ways that you just can't with SAT/SMT solvers.