However, Heule found the discovery of past results invigorating. It proved that other researchers found the problem important enough to go on and confirmed to him that the only outcome worth achieving was to solve the problem thoroughly.
“When we realized that there had been 20 years of research on this issue, it completely changed the picture,” he said.
Avoid vulgarity
Over the years, Heule has succeeded by finding efficient ways to search among the multitude of possible combinations. His approach is known as the SAT—short for “satisfaction.” It involves constructing a long formula, called a Boolean formula, that can have two outcomes: 0 or 1. If the result is 1, the formula is true and the problem is satisfied.
For the encapsulated coloring problem, each variable in the formula can represent whether a given cell is occupied by a given number. The calculator tries to assign variables to satisfy the formula. If the computer can do that, you know that it is possible to pack the mesh according to the conditions you have set.
Unfortunately, a simple encoding of the encapsulated coloring problem as a Boolean formula can span millions of terms—one computer or even a group of computers can run the experiment forever. different ways of assigning variables within it.
“Trying to do this brute force will bring the universe to an end if you do it naively,” says Goddard. “So you need some great simplification to bring it down to something even possible.”
Furthermore, every time you add a number to the packaging coloring problem, it becomes about 100 times harder, because the way combinations can multiply. This means that if a series of parallel computers could exclude 12 from a calculation day, they would need a 100 day computation time to exclude 13.
In a way, Heule and Subercaseaux consider scaling a computationally robust approach vulgar. “We had some promising ideas, so we thought, ‘Let’s try to optimize our approach until we can solve this problem in a bit,’” Subercaseaux said. in less than 48 hours of computation on the cluster’,” said Subercaseaux.
To do that, they had to think of ways to limit the number of combinations the cluster had to try.
“[They] not only wanted to solve it, but solved it in an impressive way,” he said. Alexander Soifer of the University of Colorado, Colorado Springs.
Heule and Subercaseaux realized that many combinations are essentially the same. If you’re trying to fill a diamond square with eight different numbers, it doesn’t matter if the first number you place is one above and one to the right of the middle square, or one below and one at the top. to the left of the center square. center Square. The two positions are symmetrical with each other and constrain your next move in the same way, so there’s no reason to test both.
If every packing problem can be solved with a checkerboard pattern, where a 1-second diagonal grid covers the entire space (like dark spaces on a chessboard), the calculations can be simplified so many. However, that is not always the case, as in this example of a finite cell with 14 numbers. The right checkerboard pattern is broken in several places towards the upper left.Courtesy of Bernardo Subercaseaux and Marijn Heule
