A Computer-Assisted Proof Solves the ‘Packing Coloring’ Problem

Heule, however, found the discovery of past results invigorating. It demonstrated that other researchers found the problem important enough to work on, and confirmed for him that the only result worth obtaining was to solve the problem completely.

“Once we figured out there had been 20 years of work on the problem, that completely changed the picture,” he said.

Avoiding the Vulgar

Over the years, Heule had made a career out of finding efficient ways to search among vast possible combinations. His approach is called SAT solving—short for “satisfiability.” It involves constructing a long formula, called a Boolean formula, that can have two possible results: 0 or 1. If the result is 1, the formula is true, and the problem is satisfied.

For the packing coloring problem, each variable in the formula might represent whether a given cell is occupied by a given number. A computer looks for ways of assigning variables in order to satisfy the formula. If the computer can do it, you know it’s possible to pack the grid under the conditions you’ve set.

Unfortunately, a straightforward encoding of the packing coloring problem as a Boolean formula could stretch to many millions of terms—a computer, or even a fleet of computers, could run forever testing all the different ways of assigning variables within it.

“Trying to do this brute force would take until the universe finishes if you did it naively,” Goddard said. “So you need some cool simplifications to bring it down to something that’s even possible.”

Moreover, every time you add a number to the packing coloring problem, it becomes about 100 times harder, due to the way the possible combinations multiply. This means that if a bank of computers working in parallel could rule out 12 in a single day of computation, they’d need 100 days of computation time to rule out 13.

Heule and Subercaseaux regarded scaling up a brute-force computational approach as vulgar, in a way. “We had several promising ideas, so we took the mindset of ‘Let’s try to optimize our approach until we can solve this problem in less than 48 hours of computation on the cluster,’” Subercaseaux said.

To do that, they had to come up with ways of limiting the number of combinations the computing cluster had to try.

“[They] want not just to solve it, but to solve it in an impressive way,” said Alexander Soifer of the University of Colorado, Colorado Springs.

Heule and Subercaseaux recognized that many combinations are essentially the same. If you’re trying to fill a diamond-shaped tile with eight different numbers, it doesn’t matter if the first number you place is one up and one to the right of the center square, or one down and one to the left of the center square. The two placements are symmetric with each other and constrain your next move in exactly the same way, so there’s no reason to check them both.