Naukowcy zaprezentowali AFSAT (Accelerated Fourier SAT), w pełni zoptymalizowany solver dla problemu spełnialności pseudo-Boolean'a. System wykorzystuje akcelerację GPU i technikę ciągłego wyszukiwania lokalnego (CLS), aby efektywnie rozwiązywać trudne problemy optymalizacyjne. AFSAT rozwinął wcześniejszą ideę FastFourierSAT w praktyczne narzędzie zdolne obsługiwać dowolne kombinacje różnorodnych ograniczeń symetrycznych w jednym problemie.
Sercem rozwiązania jest użycie kompilatora JAX, który umożliwia automatyczną wektoryzację, automatyczne różniczkowanie oraz kompilację just-in-time. Dzięki temu system może uruchamiać ogromnie paralelne wyszukiwanie całych partii kandydatów jednocześnie. Zespół zidentyfikował i rozwiązał szereg wyzwań związanych z opóźnieniami pamięci i dokładnością liczb zmiennoprzecinkowych, implementując dostosowaną transformację Fouriera, która poprawia stabilność numeryczną.
Wyniki pokazują znaczną poprawę w wydajności i efektywności pamięci w porównaniu z prototypem. Szczególnie imponujące jest skalowanie — system osiąga prawie liniową przepustowość przy rozproszeniu obliczeń na wiele akceleratorów. To otwiera możliwości dla szybszego rozwiązywania rzeczywistych problemów optymalizacyjnych, które do tej pory były trudne do obliczenia.