  We consider so-called squaring the square-puzzles where a given square (or
rectangle) should be dissected into smaller squares. For a specific instance of
such problems we demonstrate that a mathematically rigorous solution can be
quite involved. As an alternative to exhaustive enumeration using tailored
algorithms we describe the general approach of formulating the problem as an
integer linear program.
