  Using a SAT-solver on top of a partial previously-known solution we improve
the upper bound of the packing chromatic number of the infinite square lattice
from 17 to 15. We discuss the merits of SAT-solving for this kind of problem as
well as compare the performance of different encodings. Further, we improve the
lower bound from 12 to 13 again using a SAT-solver, demonstrating the
versatility of this technology for our approach.
