Przyspieszanie hybrydowych problemów spełnialności boolowskiej XOR–CNF natywnie za pomocą obliczeń w pamięci

Dlaczego szybsze rozwiązywanie problemów ma znaczenie

Wiele zadań, które wpływają na nasze życie codzienne — od zabezpieczania komunikacji online po projektowanie szybszej elektroniki — sprowadza się do zadania komputerowi pytania na tak lub nie: czy istnieje kombinacja przełączników, która sprawia, że ta rozbudowana reguła logiczna jest prawdziwa? To jest problem spełnialności boolowskiej, zwany SAT. SAT jest powszechnie trudny, a w miarę jak te zadania rosną pod względem skali i znaczenia, czas i energia potrzebne do ich rozwiązania stają się poważnym wąskim gardłem. Artykuł bada nowy sposób przyspieszenia rozwiązywania SAT przez przeprojektowanie zarówno matematyki, jak i sprzętu tak, aby współdziałały wewnątrz specjalnego typu układu pamięci.

Przekształcanie splątanych reguł w prostsze elementy

Tradycyjne solvery SAT zwykle opisują problemy jednym stylem reguł logicznych, zbudowanych z warunków „LUB” (OR). Jednak wiele rzeczywistych problemów przemysłowych — takich jak dekodowanie sygnałów bezprzewodowych, testowanie układów scalonych pod kątem usterek czy ataki na niektóre schematy kryptograficzne — naturalnie miesza „LUB” z „ekskluzywnym LUB” (XOR), rodzajem sprawdzenia parzystości, które zmienia wynik przy zmianie pojedynczego wejścia. Dzisiejsze narzędzia często zmuszają do przepisania reguł XOR przy użyciu tylko OR, co powiększa rozmiar problemu i spowalnia obliczenia. Autorzy zamiast tego zachowują oba typy reguł, tworząc hybrydowy opis bliższy temu, jak problemy pojawiają się w praktyce.

Robienie więcej przy użyciu mniejszej liczby elementów

Badacze starannie porównują ten hybrydowy opis z tradycyjnym na szeregu zestawów testowych pochodzących z kryptografii oraz klasycznego problemu zwanego minimalnym niezgodnym parytetem. Poprzez automatyczne odtwarzanie ukrytej struktury XOR i stosowanie inteligentnych uproszczeń najpierw, pokazują, że mieszana reprezentacja może zmniejszyć liczbę zmiennych nawet kilkukrotnie i zredukować liczbę reguł mniej więcej o współczynnik cztery do pięciu. Innymi słowy, to samo logiczne pytanie często można sformułować przy znacznie mniejszej liczbie elementów, gdy pozwolimy na współistnienie XOR i OR. Mniejsze problemy są łatwiejsze nie tylko dla oprogramowania, lecz także dla wyspecjalizowanego sprzętu, który ma ścisłe ograniczenia dotyczące liczby reguł, jakie może przechowywać jednocześnie.

Pozwolenie układom pamięci na wykonywanie obliczeń

Aby wykorzystać ten bardziej zwartej opis, zespół projektuje dedykowany akcelerator „obliczeń w pamięci”. Zamiast ciągłego przesyłania danych między procesorem a pamięcią, urządzenie to wykonuje większość obliczeń tam, gdzie dane są przechowywane — wewnątrz siatek małych elementów elektronicznych zwanych memrystorami. Adaptują znaną strategię lokalnego przeszukiwania, WalkSAT, do nowego wariantu nazwanego WalkSAT-XNF, który natywnie obsługuje połączone reguły XOR–OR. Każdy krok algorytmu — sprawdzenie, które klauzule są naruszone, oszacowanie, jak bardzo każda zmienna jest istotna, dodanie odrobiny losowości, aby wydostać się z martwych punktów, oraz odwrócenie najlepszego kandydata — jest zaimplementowany bezpośrednio w układach analogowych na macierzach krzyżowych, z prostymi obwodami pomocniczymi wybierającymi, którą zmienną odwrócić dalej.

Dowód działania w laboratorium i symulacjach

Autorzy najpierw budują mały prototyp wykorzystujący układy memrystorowe, aby wykazać, że sprzęt analogowy może wiernie oceniać klauzule i kierować przeszukiwaniem, nawet w obecności wariacji produkcyjnych i szumów elektrycznych. Eksperymenty na umiarkowanie dużym przypadku testowym pokazują, że zachowanie sprzętu jest bliskie idealnym symulacjom. Następnie modelują bardziej zaawansowany projekt w technologii 28 nanometrów i testują go na rodzinach problemów kryptograficznych i parytetowych. Ponieważ hybrydowy opis pakuje więcej informacji w mniejszej liczbie klauzul, akcelerator potrzebuje znacznie mniej pamięci na chipie i zużywa dużo mniej energii na krok niż wersja ograniczona do reguł tylko OR. Ogólnie rzecz biorąc, hybrydowy solver w pamięci osiąga około dziesięciokrotnego przyspieszenia i mniej więcej tysiąckrotnej poprawy efektywności energetycznej w porównaniu z wiodącymi programowymi solverami SAT uruchamianymi na konwencjonalnych procesorach CPU.

Co to oznacza dla przyszłych komputerów

Mówiąc zwyczajnie, praca pokazuje, że możemy rozwiązywać niektóre niezwykle trudne problemy na tak lub nie znacznie szybciej i przy znacznie mniejszym zużyciu energii, dopasowując sposób zapisu reguł logicznych do sposobu, w jaki nowy rodzaj sprzętu oparty na pamięci wykonuje obliczenia. Dzięki natywnej obsłudze zarówno reguł XOR, jak i OR wewnątrz układu, proponowany akcelerator może stawić czoła realistycznym zadaniom z dziedziny kryptografii, komunikacji i projektowania układów, korzystając z mniejszego, chłodniejszego i szybszego sprzętu. W miarę jak systemy obliczeniowe coraz bardziej napierają na granice energii i szybkości, takie specjalistyczne, wykonywane w pamięci podejścia mogą pomóc utrzymać krytyczną infrastrukturę cyfrową bezpieczną i wydajną.

Cytowanie: Im, H., Böhm, F., Pedretti, G. et al. Accelerating hybrid XOR–CNF Boolean satisfiability problems natively with in-memory computing. Nat Commun 17, 2922 (2026). https://doi.org/10.1038/s41467-026-69465-2

Słowa kluczowe: Spełnialność boolowska, obliczenia w pamięci, krzyżowa pamięć memrystorowa, akceleratory sprzętowe, kryptografia