alt Hacker NewsIt seems like a lot of the difficulty is in finding arrangements that satisfy constraints. I wonder if an alternative approach would be to use a SAT solver. I suppose the problem with that approach would be that the solver might always find an 'easy' solution that doesn't look random. I know that some SAT solvers let you randomly assign the initial assignments of the variables, but that doesn't mean you get a random solution. Has anyone tried a similar approach?
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.