It 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?