The strongest insight here is that the SAT solver did not merely solve the same problem faster. It solved a better-formulated problem: choose the pieces as well as their placement.