I think the problem with SAT solvers is that they’re complicated, in terms of computation and also how easy it is to understand by someone who didn’t study formal methods.

WFC is brute-force-simple, but because it’s simple it’s quite computationally inexpensive (unless it hits a lot of dead-ends) and I wouldn’t be surprised if it could often find an adequate solution quicker than a SAT solver. At least for games, where a result doesn’t need to be perfect, just good enough.