The Packing Chromatic Number of the Infinite Grid is 15: the story behind it
bsubercaseaux.github.io
bsubercaseaux.github.io
Congratulations, Bernardo!
I agree with you about Coq, although there are some very smart folks working on it. My concern is that most of the improvements I've heard of are not about usability directly (i.e., how fun and readable it is to work with). I also don't quite now of precise low-hanging fruits that would improve it in this direction, but hopefully theorem provers will get friendlier and easier to use as time advances. Also the library of lemmas other people have proved and one can just plug in is steadily growing, so that should also reduce the pain of proving new stuff...
> After more optimizations, it turned out the chessboard conjecture was false
> Figure 19: The smallest counterexample to the chessboard conjecture. The diamond of radius 14, and a 6 forced in the center, can be packing-colored with 14 colors only if the chessboard pattern is broken.
I don't understand why this is a counterexample to the conjecture. Painting the center with color 6 isn't part of the graph. Can the diamond of radius 14 be colored using a checkerboard pattern of 1s when the center color isn't 6?
Is the diamond of radius 14, with a 2 forced in the center and in all 4 squares adjacent to the center, a counterexample to the conjecture that the infinite grid is colorable at all?
Yes - the counterexample given can be shifted left by 1, making a the center color 1 (more 1s can be inserted completing the checkerboard pattern).
I suspect that the conjecture to which this is a counterexample was imprecisely stated in the blog post, although there could also be a reason that a counterexample with a 6 in the center leads to a general counterexample.
Just to make it fully precise, the conjecture was that if you take any $D_r$ graph, and force any color in the center (to avoid parity considerations that shift the chessboard pattern, assume the center color is different from $1$), then you can packing-color it if and only if you can do so after enforcing the chessboard pattern.
In simpler words, the conjecture was that you could assume without loss of generality that the 1s would make a chessboard pattern, and this is not true in general. It is however likely that a modified version of the chessboard conjecture is true. In particular, Don Knuth thinks it holds for all diamonds of odd radius. There is a precise way of formalizing his variant of the conjecture. However, I'm not too inclined to work on it now that the core problem has been solved...
About the "why 6 in the center?" implicit question in your comment: this is a nice question and I unfortunately only have a speculative answer (which is stated to some degree in the paper as we have an entire section on how to choose the center-color). In some sense, there's not really a way to answer this question super nicely: this is the smallest counter-example, and for some reason of the mathematical universe no smaller counter-example exists. I'm 90% sure that 6 is the smallest center-color for which a counter-example of this size exists. It's definitely possible to run 5 more experiments to confirm this, although given that it costs money to do so (even if neither me or my advisor are directly paying for the computing resources), I'm not sure if it's worth doing.
I'm interested in the conjecture that was stated in the post. That one just says "if a k-coloring exists, then a k-coloring in which the 1s form a perfect checkerboard pattern also exists".
That seems like it's enough to allow you to assume without loss of generality that the 1s form a checkerboard pattern. That's still a huge reduction in the search space - you need to consider that the pattern might be shifted, but that only doubles the amount of work you're doing (since there are only two ways to fill in a checkerboard pattern on a grid), while filling in the checkerboard cuts the amount of work you're doing by a factor of 2^k.
Also, it seems like something of an "error" (maybe not! What do we know about aperiodic colorings?) when thinking about checkerboarding to spend time considering graphs that won't tile the plane. The radius-14 diamond can't tile the plane while checkerboarded; a checkerboard pattern will hit more or less than half of the cells in the grid.
Here are two well-defined conjectures:
Conjecture 1. A packing-coloring of the infinite square grid exists using colors {1, ..., k} if, and only if, there exists one with a chessboard pattern (meaning that wlog all vertices (a, b) such that a+b is odd get color 1).
Conjecture 2. Let $D_{r, k, c}$ be the instance consisting of whether $D_r$ can be packing-colored with $k$ colors assuming it gets color $c$ in the center. Then enforcing that all vertices (a, b) such a+b is odd get color 1 does not change the satisfiability of the instance.
Conjecture 1 is true, based on our paper: if k <= 14, then no packing-coloring exists anyway, so the conjecture is vacuously true. If k >= 15, then we know of a packing-coloring that respects the chessboard pattern (the one in Figure 12), and so the conjecture holds.
Conjecture 2 is false, this is where the smallest counterexample in the post kicks in.
Note that given that 13 colors are not enough, we knew that if there was a solution with 14 colors, it must use color 6 somewhere, and by restricting ourselves to $D_{14}$ around such a vertex, we run into the issue!
About your last comment, we use diamond graphs to prove lower bounds (i.e., that a certain number of colors is not enough), while finite square grids are used to prove upper bounds (as in Figure 12).
About aperiodic colorings, see the other comment in this thread were we discuss about it a bit :)
I understand this, but I'll need to refer to it in a moment...
> Conjecture 2. Let $D_{r, k, c}$ be the instance consisting of whether $D_r$ can be packing-colored with $k$ colors assuming it gets color $c$ in the center. Then enforcing that all vertices (a, b) such a+b is odd get color 1 does not change the satisfiability of the instance.
I'll assume that D_r refers to a taxicab disc ("diamond") of radius r?
Conjecture 2 is well-defined, but I see several problems with it. Conjecture 1 seems like a reasonable thing to investigate (though it's not what I had in mind); Conjecture 2 doesn't.
Most obviously, Conjecture 2 is false, since D_{r, k, 1} is dramatically affected by forcing all cells at an odd taxicab distance from the center to take color 1.
Second, while you are correct to say that the existence of any checkerboard pattern which successfully k-colors the infinite grid implies the existence of a checkerboard pattern which k-colors the infinite grid and assigns color 1 to those vertices (a, b) such that a+b is odd, the same cannot be said (and you haven't said it) about a finite grid. It it then not obvious why, when discussing a finite grid, you want to restrict checkerboard patterns to those which assign color 1 to vertices at an odd taxicab distance from the center of the grid. You can't say "without loss of generality" about that choice; the grid is no longer infinite. In your 14-diamond, this presents the problem that the off-center checkerboard cannot color half of the cells in the grid, because -- to use a chessboard analogy -- the number of "black" cells is not equal to the number of "white" cells. This suggests an obvious reason why a checkerboard that is forced to color the smaller half of the diamond might prove to be inadequate to the task.
Third, it is not obvious why you want to restrict yourself to grids that have a center cell. The following grid is not a taxicab disc:
xxxxxx
xxxxxx
xxxxxx
xxxxxx
xxxxxx
xxxxxx
The question I'm really asking here is, I guess, "What is the point of your Conjecture 2? Who would care what the answer was?" You introduced it as a way to cut down on the search space for a computationally-intensive trial-and-error problem, and it appears to be effective at that goal. But you go on to say that you can't use it to achieve that goal because it's false, when a version of your conjecture that is (1) much more natural to pose; and (2) equally useful for the purpose of cutting the search space, might still be true! You wouldn't want the checkerboard to avoid the center of a diamond anyway, because if it goes through the center of the diamond, it will give you a bigger reduction in the search space than the checkerboard that avoids the center will!
Why is the conjecture not this one?
Checkerboard Conjecture: for any "interesting subset" [Diamonds on the grid? Bounded convex subsets of the grid? Connected subsets? This can be refined; maybe diamonds are fine.] of the infinite grid ℤ², if any packing-coloring exists with k colors, then a packing-coloring exists with k colors in which color 1 forms a checkerboard. That is to say, any two vertices v = (a, b) and w = (c, d) satisfy a+b ≡ c+d (mod 2) if and only if (either v and w both have color 1, or v and w both fail to have color 1).
In particular, to show that the packing-chromatic number of the infinite grid is 15, we needed to find a finite subgraph of the infinite square grid for which 14 colors are not enough. The class of sub-graphs that seemed more amenable to do this was that of diamonds (i.e., disks in the corresponding metric) of radius r. If you simply try to determine whether D_{14} can be packing-colored with 14 colors, that instance is too hard, so we make it easier by forcing a color in the center (this is a form of symmetry breaking). Forcing the center to take color 1 is the worst possible choice (see Fig 6. of the paper https://arxiv.org/pdf/2301.09757v1.pdf), therefore we want to force it to something other than 1, let's say 6 (this seems to be the best choice in practice). Your problem then reduces to determine whether D_{14} can be packing-colored with 14 colors, when forcing a 6 in the center. It turns out again that this is not easy enough to solve naively, so it would be really nice it we could assume without loss of generality that we can enforce the chessboard pattern as well as the 6 in the center (which given that the center has even coordinates, it would imply that the 1s are at odd coordinates). I try to prove this manually and failed. But we ran the experiment assuming the conjecture to be true, and effectively there is no packing-coloring for D_{14} with 14 colors, a 6 in the center, and 1s in every odd coordinate. If Conjecture 2 had been true, then we would have ended our work there, but then we realize we couldn't assume Conjecture 2: we found a way of packing-coloring D_{14} with a 6 in the center when removing the chessboard assumption.
So the formalization in our context that made the most sense was: "is it true that given any radius r, any value of k, and any value of c, the forced center color, we can assume the chessboard pattern?" (Noting that if the center is forced to 1 as you mention in your comment, then the chessboard pattern would be 1s on the even coordinates).
This is what I meant with Conjecture 2, so hopefully now it's clear why it was of interest for this particular problem. It's not obvious at all that Conjecture 2 is false provided this! unless you have a new argument I'm unaware of!
Your last question is of course interesting, and many variations of the conjecture make sense and could be studied; we didn't really pose Conjecture 2 thinking it was the most interesting formulation, but rather a sufficiently simple one that would have justified our result of (D_{14}+6 in the center + 1s at odd coordinates)-is-not-packing-colorable-with-14-colors to imply the final result.
The example of symmetry breaking in your post is "the instance of the largest color that appears closest to the center must appear in octant II".
I can understand this - by using a combination of rotations and reflections, any coloring that doesn't satisfy this constraint can be transformed into one that does. So the patterns we reject by using this "symmetry-breaking" approach are those that are identical, through one or more symmetries, to a pattern we won't reject. So far so good.
But forcing a color in the center can't be symmetry-breaking in this sense. Every symmetry of the diamond will map the center onto itself, so applying a "symmetry-breaking" rule that the center must be painted a particular color will let you rule out a total of zero patterns that can be transformed into patterns that match your rule. That is, literally, worthless.
Such a constraint will let you rule out patterns that aren't transformable into the patterns you do consider... but that's bad, not good.
What do you mean when you say that forcing a color in the center is a form of symmetry breaking?
formalizing this might be tricky, I mean something like a bijection from (the set of mappings from an infinite packing-coloring to a fixed colored sub-graph) to itself.
This is a good point; I had been thinking of the problem differently.
In this model, the diamond is viewed as just being a window onto the infinite grid, and we're not interested in whatever properties it might have considered as a finite graph. Thinking about it this way, the idea that the coloring in your article disproves is that "there is a 14-packing-coloring of the infinite grid which uses a chessboard pattern for color 1".
But then, since (by your later result) there is no 14-packing-coloring of the infinite grid, it's not too surprising that there isn't such a coloring that also features a chessboard.
What bothers me in this discussion of the chessboard conjecture is the switch: you say "at this point, we were conjecturing that using color 1 in the chessboard pattern that yields density 1/2 was optimal, meaning that you could packing-color a graph D_r with k colors (...) if, and only if, you could do it enforcing the chessboard pattern of 1's". And this seems plausible, and the illustration provided as a counterexample isn't actually a counterexample to this statement. You can packing-color the graph shown there with 14 colors, and you can do so while enforcing the chessboard pattern of 1s.
In your explanation here, you're viewing D_r as a subgraph of the successfully-colored infinite grid, not as a finite graph in its own right. That handily explains why the chessboard pattern goes around the center of D_r instead of through it. The illustration in the post does then show that there's a problem. But to my eye, the problem is in the premise of a successfully 14-packing-colored infinite grid, not in the chessboard conjecture. In between stating the chessboard conjecture and providing the counterexample, you changed what the chessboard conjecture said -- there is no reference to the infinite grid in your statement of the chessboard conjecture, but the illustration of a "counterexample" is a counterexample to a statement about the infinite grid. It feels wrong. :-/
I agree with you that just saying “D_r can be colored with k colors iff it can be done with a chessboard pattern of 1s” is a slightly different statement to which our counterexample is not a counterexample, but I think you got trapped into my initial omission in the blog post, which was a writing mistake rather a mathematical mistake. I don’t think there’s anything wrong here, but sorry for the original version of this post being sloppy in the writing.
I agree again with what you were saying some messages ago about how versions of the conjecture that do not consider the center color can be more mathematically interesting. A proof that D_r can be colored with k colors iff it can be done with the chessboard pattern would definitely be super nice.
If the diamond can be colored using the checkerboard pattern, then it is not a counterexample to the iff-qualified statement, because it is true that "you can packing-color the graph [while] enforcing the checkerboard pattern of 1s". The graph is 14-colorable and it is 14-colorable with a checkerboard pattern of 1s; both claims are true and the iff is satisfied.
Note that the "only if" direction of this conjecture is the only meaningful one; in the "if" direction, you have "if you can k-color a graph while obeying a particular coloring constraint, then you can k-color the graph", which is obvious.
It is easy to forget the scale at which academia operates.
The "supercomputer" m6idn.32xlarge with 128 vCPU on AWS costs $1.3409 per Hour (spot pricing). So 9000 hours of compute would be ~$12k.
Since transferring 36 TB of data out of AWS costs about $3,000, you can actually include the rest of the system including dual-CPU motherboard and tons of storage for $15,000.
I hope this reaches many, many people on HN. I wish I had read this in high school so that I better understood what ideal academia is all about.
So (again, without knowing much about the problem at hand), the answer to your question might be that the simplest possible examples are much simpler anyway.
As for the question of why no smaller counter-examples, I'm afraid I don't have any nice answers and perhaps there simply isn't a nice answer. Let me explain what I mean. My advisor Marijn Heule finished the resolution of Keller's conjecture (a conjecture about how N-dimensional cubes work in the Euclidean N-dimensional space), and the final answer is that the conjecture fails for the first time in dimension 8. "Why 8?" Again it's the same situation: it seems that that's just the way math is, something in the way the definitions and the objects behave makes it so that is the smallest counterexample. "Why" is a hard question to answer...
This is however extremely hard in my opinion (note that I say "opinion" on purpose, because I don't have any way to formalize this idea). Let me use a couple more examples: any Rubik's cube (3x3x3) can be solved in at most 20 moves (on the standard metric, counting double turns as one move), and a Sudoku needs at least 17 clues to have a unique solution. Why 20? Why 17? We (humanity) got to both answers through computation, and even though the computation requires mathematical observations to be made more efficient, at the end we still checked an in-human number of cases... So in all honesty, if I had to bet, I'd say we will probably never intuitively know why 20 moves or why 17 clues, or in my case, why 15 colors... I'd love to be proven wrong tho!
For graphs that are infinite in two dimensions I don't have an answer yet (and it's likely that I never will). I'm very fond of this question tho, so if you give me your email (you can contact me at bsuberca@cs.cmu.edu), I can promise to write you back if at some future point in time I have a solution to this, or if someone else shares one with me :)