# Rigorous packing of unit squares into a circle

Let $r_{n}$ be the radius of the smallest circle into which one can pack $n$ non-overlapping unit squares that are free to rotate. For $n = 1, 2$, $r_{1} = \frac{\sqrt{2}}{2}$ and $r_{2} = \frac{\sqrt{5}}{2}$ are proved to be optimal. For $n \geq 3$ only guesses of $r_{n}$ are known. This paper introduces a computer-assisted method to find rigorous enclosures for $r_{n}$ and the corresponding optimal arrangements. Given an upper bound $\ol r_{n} > 0$ for $r_{n}$, we formulate the containment and the non-overlapping conditions as a constraint satisfaction problem (CSP) and ask for every arrangement satisfying $r_{n} \leq \ol r_{n}$. We solve the problem using an interval branch-and-bound procedure implemented in the rigorous solver \GL {} to ensure the mathematical certainty of our statements. General purpose interval methods cannot solve the CSP due to symmetries in the search domain. To overcome this difficulty, we split the problem into a set of subproblems by adding tiling constraints specially designed for the packing of unit squares. Our procedure also iterates on the number of squares to discard simple subproblems and avoid the exponential growth of hard ones. As an application, we find a rigorous enclosure for the optimal arrangement of $n = 3$. In this case, the proof requires the solution of $6$, $43$ and $12$ subproblems with $1$, $2$ and $3$ unit squares respectively.

Submitted