But Heule felt energized by discovering past results. This demonstrates that the other researcher feels the problem is important enough to work on, and confirms that the only result worth gaining for him is to completely solve the problem. Did.
“Once we found out that we had been working on this problem for 20 years, things changed completely,” he said.
avoid vulgar
Over the years, Heule has made a career out of finding efficient ways to search through vast combinations. His approach is called his SAT solution (short for “Satisfaction Possibility”). This involves building long expressions called boolean expressions. This expression has two possible outcomes of him, 0 or 1. If the result is 1, the expression is true and the problem is satisfied.
For packing coloring problems, each variable in the formula may represent whether a particular cell is occupied with a particular numeric value. Computers look for ways to assign variables to satisfy an expression. If your computer can do it, you know it’s possible to pack the grid under the conditions you set.
Unfortunately, encoding the packing coloring problem directly as a boolean expression can lead to millions of terms, and a computer or even a group of computers would take forever to keep testing all the different ways to assign variables. may be
“If you try to force this, naively it will take you until the end of the universe,” Goddard said. “So we need some cool simplifications to make it viable.”
Furthermore, each additional number added to the packing color problem increases the number of possible combinations, increasing the difficulty by a factor of about 100. This means that if a bank of computers working in parallel can exclude 12 in his daily calculation, then excluding 13 would require 100 days of computational time.
Heule and Subercaseaux thought that scaling up the brute-force computational approach was, in some ways, vulgar. “We had some promising ideas, so we took the mindset of, ‘Let’s try optimizing our approach until he can solve this problem on a cluster in less than 48 hours of computation,’” he says. said.
To do that, we had to come up with a way to limit the number of combinations the compute cluster had to try.
“[They] We don’t just want to solve it, we want to solve it in an impressive way.” Alexander Soifer from 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 tile with eight different numbers, it doesn’t matter if the first number you place is one above the center square, one to the right, or one below it to the left. central square. There is no reason to check both, as the two placements are symmetrical to each other and constrain the next move in exactly the same way.
If all packing problems could be solved with a chessboard pattern where a diagonal grid of 1’s covers the entire space (like the dark spaces on a chessboard), the computation could be greatly simplified. However, this is not always the case, as in the example of finite tiles packed with 14 numbers. The chessboard pattern should break in several places towards the top left.Courtesy of Bernardo Subercaseaux and Marijn Heule
