1: \begin{abstract}

2: A packing $k$-coloring is a natural variation on the standard notion of graph $k$-coloring, where vertices are assigned numbers from $\{1, \ldots, k\}$, and any two vertices assigned a common color $c \in \{1, \ldots, k\}$ need to be at a distance greater than $c$  (as opposed to $1$, in standard graph colorings). Despite a sequence of incremental work, determining the packing chromatic number of the infinite square grid has remained an open problem since its introduction in 2002. We culminate the search by proving this number to be 15. %, using a combination of several automated reasoning and verification techniques which results in computer-checkable proof.

3: We achieve this result by improving the best-known method for this problem by roughly two orders of magnitude. The most important technique to boost performance is a novel, surprisingly effective propositional encoding for packing colorings. Additionally, we developed an alternative symmetry-breaking method. Since both new techniques are more complex than existing techniques for this problem, a verified approach is required to trust them. We include both techniques in a proof of unsatisfiability, reducing the trusted core to the correctness of the direct encoding. 

4: 

5: \keywords{Packing coloring  \and SAT \and Verification.}

6: \paragraph{\textbf{Acknowledgments}.}

7:         This work is supported by the U.S.\ National Science Foundation under grant CCF-2015445. 

8: We thank the Pittsburgh Supercomputing Center for allowing us to use Bridges2~\cite{cluster} in our experiments.

9: 	We thank as well the anonymous reviewers from TACAS2023 for their comments and suggestions. We also thank Donald Knuth for his thorough comments and suggestions. The first author thanks the Facebook group \emph{``actually good math problems''}, from where he first learned about this problem, and in particular to Dylan Pizzo for his post about this problem.

10: 

11: \end{abstract}

12: