Before you go and try to encode "all problems as SAT instance", I'd recommend to consider that SAT formulations require a fixed number of (Boolean) variables. Sure, you can use tens of thousands of helper variables to encode a problem, but at a certain point this gets unwieldy and basically all you're doing is working around SAT limitations and spend your time implementing a SAT encoder (and translator for the answer into your original domain language as you say).

Even simple goal-directed block's world-like robotic planning problems where the number of moves and the items to pickup/putdown are variable are much easier formulated and solved using Prolog.

"All" isn't right.

You can only encode decision problems in NP into a SAT instance of polynomially-balanced size. Sure, that's a lot of things, but there are things provably not in this set.