Heule jednak uznał odkrycie wcześniejszych wyników za ożywcze. Pokazało, że inni badacze uznali problem za wystarczająco ważny, aby nad nim pracować, i potwierdziło dla niego, że jedynym wynikiem, który warto uzyskać, jest całkowite rozwiązanie problemu.
„Kiedy zorientowaliśmy się, że nad problemem pracowano przez 20 lat, całkowicie zmieniło to obraz” – powiedział.
Unikanie wulgaryzmów
Przez lata Heule zrobił karierę na znajdowaniu skutecznych sposobów wyszukiwania wśród ogromnych możliwych kombinacji. Jego podejście nazywa się rozwiązywaniem SAT – skrót od „satisfiability”. Polega na skonstruowaniu długiej formuły, zwanej formułą boolowską, która może mieć dwa możliwe wyniki: 0 lub 1. Jeśli wynikiem jest 1, formuła jest prawdziwa i problem jest spełniony.
W przypadku problemu z kolorowaniem upakowania każda zmienna we wzorze może reprezentować, czy dana komórka jest zajęta przez daną liczbę. Komputer szuka sposobów przypisania zmiennych, aby spełnić formułę. Jeśli komputer może to zrobić, wiesz, że można spakować siatkę w ustalonych warunkach.
Niestety, proste zakodowanie problemu kolorowania upakowania w postaci formuły boolowskiej mogłoby obejmować wiele milionów terminów — komputer, a nawet cała flota komputerów, mogłaby bez końca testować różne sposoby przypisywania zmiennych.
„Próba wykonania tej brutalnej siły zajęłaby cały wszechświat, gdybyś zrobił to naiwnie” – powiedział Goddard. „Potrzebujesz więc fajnych uproszczeń, aby sprowadzić to do czegoś, co jest w ogóle możliwe”.
Co więcej, za każdym razem, gdy dodajesz liczbę do problemu kolorowania opakowań, staje się on około 100 razy trudniejszy ze względu na sposób, w jaki możliwe kombinacje się mnożą. Oznacza to, że gdyby bank komputerów pracujących równolegle mógł wykluczyć 12 w ciągu jednego dnia obliczeń, potrzebowałby 100 dni czasu obliczeń, aby wykluczyć 13.
Heule i Subercaseaux uważali skalowanie podejścia obliczeniowego metodą brute-force za wulgarne. „Mieliśmy kilka obiecujących pomysłów, więc przyjęliśmy nastawienie „Spróbujmy zoptymalizować nasze podejście, aż będziemy w stanie rozwiązać ten problem w czasie krótszym niż 48 godzin obliczeń w klastrze” – powiedział Subercaseaux.
Aby to zrobić, musieli wymyślić sposoby ograniczenia liczby kombinacji, które musiał wypróbować klaster obliczeniowy.
“[They] chcą nie tylko go rozwiązać, ale rozwiązać w imponujący sposób” – powiedział Alexander Soifer z University of Colorado w Colorado Springs.
Heule i Subercaseaux uznali, że wiele kombinacji jest zasadniczo takich samych. Jeśli próbujesz wypełnić płytkę w kształcie rombu ośmioma różnymi liczbami, nie ma znaczenia, czy pierwsza liczba, którą umieścisz, to jedna w górę i jedna na prawo od środkowego kwadratu, czy jedna w dół i jedna na lewo od centralny plac. Te dwa miejsca są względem siebie symetryczne i ograniczają twój następny ruch dokładnie w ten sam sposób, więc nie ma powodu, aby sprawdzać je oba.
Gdyby każdy problem z pakowaniem można było rozwiązać za pomocą szachownicy, w której ukośna siatka 1s pokrywa całą przestrzeń (jak ciemne pola na szachownicy), obliczenia można by znacznie uprościć. Jednak nie zawsze tak jest, jak w tym przykładzie skończonej płytki zawierającej 14 liczb. Wzór szachownicy musi być przerwany w kilku miejscach w kierunku lewego górnego rogu.Dzięki uprzejmości Bernardo Subercaseaux i Marijn Heule
