Except you first have to encode the problem as a logic expression over (potentially tens of thousands of) Boolean variables. Might be impractical, or might even

Except you first have to encode the problem as a logic expression over (potentially tens of thousands of) Boolean variables. Might be impractical, or might even be impossible for eg robotic planning with an unlimited number of planning steps, and doesn't necessarily extend well to solving with respect to an objective function (eg optimization). What you usually see is a domain-specific problem description/language that then gets compiled into a SAT problem using a custom transformator/generator program. In other words, the problem of a suitable problem description language isn't solved ;) You can override/customize Prolog's default search strategy as desired, Prolog being Turing-complete. Prolog syntax and resolution in this case just provides a straightforward starting point; which is much needed as you explore the complexities and challenges of your problem domain to kick-off a project (you know, as opposed to prematurely optimizing a program for transforming you DSL into a SAT/SMT formulation). I think Prolog works very well for this. Note Prolog also has libraries for offloading to SAT solvers and eg. z3 supports a Datalog subset as an alternative to SMTLIB/Lisp-like syntax.