I understand the sentiment for a problem where the instance size is quite known. SAT solvers have become incredibly fast. Just note that encoding terms of vari

I understand the sentiment for a problem where the instance size is quite known. SAT solvers have become incredibly fast. Just note that encoding terms of various shapes in SAT is very difficult. Encoding terms of unknown size doubly so. Encoding problems in Prolog is very easy in that sense, as you can build arbitrarily shaped terms very easily and you can constrain variables within terms and not only on the top level. The sudoku example, with the fixed shape and all variables at the top level is a prime example for SAT solving though.