> ... SAT solvers only really seem to be good at Sudoku.
This is really not true.
SAT solvers are really good these days, and many (exact) algorithms (for NP-hard problems) simply use some SOTA SAT solvers and are automatically competitive.
This is really not true.
SAT solvers are really good these days, and many (exact) algorithms (for NP-hard problems) simply use some SOTA SAT solvers and are automatically competitive.
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.
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.