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 \u2014 short for \u201csatisfiability.\u201d 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.<\/p>\n

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\u2019s possible to pack the grid under the conditions you\u2019ve set.<\/p>\n

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

\u201cTrying to do this brute force would take until the universe finishes if you did it na\u00efvely,\u201d Goddard said. \u201cSo you need some cool simplifications to bring it down to something that\u2019s even possible.\u201d<\/p>\n

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\u2019d need 100 days of computation time to rule out 13.<\/p>\n

Heule and Subercaseaux regarded scaling up a brute-force computational approach as vulgar, in a way. \u201cWe had several promising ideas, so we took the mindset of \u2018Let\u2019s try to optimize our approach until we can solve this problem in less than 48 hours of computation on the cluster,\u2019\u201d Subercaseaux said.<\/p>\n

To do that, they had to come up with ways of limiting the number of combinations the computing cluster had to try.<\/p>\n