One of the patterns the CMU team used to prove that 14 colors/numbers isn’t enough to solve the packing problem; note that, in the upper left, the “chessboard” pattern of 1s is interrupted.
CMU Team Uses Bridges-2 to Solve a 21-Year-Old Coloring Problem in Mapping
Four colors can paint any two-dimensional map without two neighboring areas sharing a color. But what if each color needed to be a different distance away from itself? Color number one had to be two “countries” away from itself, and color number 10 had to be 11 countries away? What if the map was also infinite? A team from CMU used PSC’s Bridges-2 system to narrow the candidates to one answer: 15 colors are just enough. This Packing Chromatic Number Problem is fascinating by itself, but also has relevance for real-world problems.
WHY IT’S IMPORTANT
In order to paint the countries in a map so that no two neighbors have the same hue, you need at most four colors. Mathematician Francie Guthrie was pretty sure this was so when he formulated the Four Color Problem, back in 1852. But it wasn’t until more than a hundred years later, in 1976, that mathematicians used computers to provide a final proof.
“A very natural question is how many colors do I need for that map of the world — how many pens should I buy? It turns out that the answer is four … They [solved] that with computer assistance. Even to this day, nobody has been able to recreate that proof with pen and paper.”
—Bernardo Subercaseaux, CMU
What if we made the rule harder? What if we assigned a number to each shade of color, and “countries” that have a certain color/number need to be separated by more than that number of countries? In other words, countries labeled “1” need to be at least two countries away from each other; those labeled “15” need to be at least 16 away? What’s the minimum number of colors/numbers it would take to paint that map?
This Packing Chromatic Number Problem, first proposed in 2002, is fascinating on its own. But like the Four Color Problem, it matters in the real world as well. One important example is when the Federal Communications Commission assigns radio frequencies to broadcasters. Power, and distance, matter. A high-powered station can’t be too close to a low-powered station on the same frequency. The Packing Chromatic Number Problem is relevant to that and other real-world scheduling problems.
The problem fascinated CMU graduate student Bernardo Subercaseaux. When CMU professor Marijn Heule spoke for Subercaseaux’s grad school class, the PhD candidate immediately realized that the kinds of problems Heule was attacking with computerized proofs were relevant to it. Subercaseaux contacted Heule. It led to a collaboration, and then Heule advising Subercaseaux for his dissertation topic.
As the two approached the problem, though, their computing needs ballooned. The answer lay in an account on PSC’s NSF-funded Bridges-2 supercomputer.
HOW PSC HELPED
Both Subercaseaux’s and Heule’s initial work and that by previous researchers had shown that 15 colors were more than enough to solve the problem, and 12 were too few. The question was whether 13 was enough, or you need 14, or even 15. The computing environment they chose for cracking this problem was Bridges-2.
“I really like how user-friendly Bridges-2 is. I made a repository that I share with my students that they just clone. And then they as soon as they have an account on Bridges … it just runs everything.”
— Marijn Heule, CMU
Conceptually, as in the Four Color Problem, their task was simple. To show that 15 is the right answer, all they needed to do was show that a map with 14 colors couldn’t work, and that 15 would. They’d do the former by testing millions of coloring patterns using the computer until they found one that didn’t work.
In practice, though, the problem grows in complexity for each added color. For example, proving that 14 colors weren’t enough was going to take about 100 times as much computational power as proving 13 weren’t enough, which the team did in 2022. Even with the most powerful supercomputers, the complexity grew so fast that a solution would take months of computation — more than scientists can get on any system.
Subercaseaux approached the problem first by figuring out how to simplify it. Symmetry proved to be the key. If one solution was the mirror image of another, only one of the two needed to be solved. By leveraging such symmetry, he was able to narrow the needed solutions eight times.
“If 15 colors are the minimum you need, then that means that, for example, six colors are definitely not going to make it… But then, as you get closer and closer to the answer… it takes a really long time to discard [each new] case … So especially with 14 colors, which is really, really, really close to working … discarding [each] case starts taking a rather long time, because it’s very close to working … Just having a trusted environment [like Bridges-2] to run many experiments really reliably [was] very important.”
— Bernardo Subercaseaux, CMU
The other key was splitting the problem into as many equal sized pieces as he could. Bridges-2’s regular memory nodes have 128 cores apiece, each able to solve part of the problem. By performing 128 pieces in parallel and then reassembling them into one answer, Subercaseaux could speed up the work by dozens of times. But that’s easier said than done. The investigators had to ensure that each chunk of the problem could be solved in about the same amount of time, or one part would hang up and the final solution would have to wait on it, eliminating the advantage of parallel computation. Much of the work focused on getting the division of labor right.
Eventually the team got the computation working. Only two days of processing on Bridges-2 gave them their answer: 14 colors were not enough. By process of elimination, it had to be 15. Not only did the CMU scientists solve the problem, they also constructed a 34-terabyte proof that can be validated by formally verified checkers, to provide full confidence in the correctness of the result. The team presented their results at the International Conference on Tools and Algorithms for the Construction and Analysis of Systems in April 2023.