Beschleunigung hybrider XOR–CNF-Boolean-Satisfiability-Probleme nativ mit In-Memory-Computing

Warum schnellere Problemlösung wichtig ist

Viele Aufgaben, die unseren Alltag prägen – von der Absicherung von Online-Kommunikation bis hin zur Entwicklung schnellerer Elektronik – laufen darauf hinaus, dem Computer eine Ja‑oder‑Nein‑Frage zu stellen: Gibt es eine Kombination von Schaltern, die diese große logische Regel wahr macht? Das ist das Problem der booleschen Erfüllbarkeit, kurz SAT. SAT ist bekanntermaßen schwer, und je größer und wichtiger diese Aufgaben werden, desto mehr Zeit und Energie werden für ihre Lösung benötigt. Diese Arbeit untersucht einen neuen Weg, SAT‑Löser zu beschleunigen, indem sowohl die Mathematik als auch die Hardware neu gestaltet werden, sodass sie gemeinsam in einer speziellen Art von Speicherchip arbeiten.

Verknotete Regeln in einfachere Bausteine verwandeln

Konventionelle SAT‑Solver beschreiben Probleme meist mit einer Art logischer Regel, die aus „ODER“-Bedingungen aufgebaut ist. Viele reale Industrieprobleme – etwa das Dekodieren drahtloser Signale, das Testen von Chips auf Fehler oder das Angreifen bestimmter kryptographischer Verfahren – mischen jedoch natürlich „ODER“ mit „exklusivem ODER“ (XOR), einer Art Paritätsprüfung, die umschlägt, wenn sich ein einzelner Eingang ändert. Heutige Werkzeuge zwingen diese XOR‑Regeln oft dazu, ausschließlich mit ODER ausgedrückt zu werden, was die Problemgröße aufbläht und alles verlangsamt. Die Autoren behalten stattdessen beide Regeltypen bei und erzeugen eine hybride Darstellung, die näher an der tatsächlichen Entstehung der Probleme liegt.

Mehr erreichen mit weniger Teilen

Die Forscher vergleichen diese hybride Darstellung sorgfältig mit der traditionellen Darstellung über mehrere Benchmark‑Familien aus der Kryptographie und einem klassischen Testproblem namens minimale Disagreement‑Parität. Indem sie automatisch versteckte XOR‑Strukturen rekonstruieren und zuerst intelligente Vereinfachungen anwenden, zeigen sie, dass die gemischte Repräsentation die Zahl der Variablen um ein Mehrfaches reduzieren und die Anzahl der Klauseln um etwa den Faktor vier bis fünf verringern kann. Anders gesagt: Dieselbe logische Frage lässt sich oft mit deutlich weniger beweglichen Teilen stellen, wenn XOR und ODER koexistieren dürfen. Kleinere Probleme sind nicht nur für Software leichter, sondern auch für spezialisierte Hardware, die strikte Grenzen dafür hat, wie viele Regeln sie gleichzeitig speichern kann.

Den Speicherchips das Denken überlassen

Um diese schlankere Darstellung auszunutzen, entwirft das Team einen dedizierten In‑Memory‑Computing‑Beschleuniger. Statt Daten zwischen Prozessor und Speicher hin und her zu schaufeln, führt dieses Gerät den Großteil der Berechnungen dort aus, wo die Daten liegen, nämlich in Gittern winziger elektronischer Elemente, sogenannter Memristoren. Sie adaptieren eine bekannte Local‑Search‑Strategie, WalkSAT, zu einer neuen Variante namens WalkSAT‑XNF, die die kombinierten XOR–ODER‑Regeln nativ handhabt. Jeder Schritt des Algorithmus – prüfen, welche Klauseln verletzt sind, abschätzen, wie wichtig jede Variable ist, etwas Rauschen hinzufügen, um aus Sackgassen zu entkommen, und die beste Kandidatin umschalten – wird direkt in analoger Schaltungstechnik auf den Crossbar‑Arrays implementiert, wobei einfache Unterstützungsschaltungen entscheiden, welche Variable als Nächstes umgeschaltet wird.

Nachweis in Labor und Simulation

Die Autoren bauen zunächst einen kleinen Prototyp mit Memristor‑Chips, um zu demonstrieren, dass die analoge Hardware Klauseln zuverlässig auswerten und die Suche leiten kann – selbst unter Fertigungsschwankungen und elektrischem Rauschen. Experimente an einer moderat großen Testinstanz zeigen, dass das Verhalten der Hardware den idealen Simulationen sehr nahekommt. Anschließend modellieren sie ein fortgeschritteneres 28‑Nanometer‑Design und benchmarken es an Familien kryptographischer und paritätsbasierter Probleme. Weil die hybride Darstellung mehr Information in weniger Klauseln bündelt, benötigt der Beschleuniger deutlich weniger On‑Chip‑Speicher und verbraucht pro Schritt viel weniger Energie als eine auf ODER‑allein beschränkte Version. Insgesamt erzielt der hybride In‑Memory‑Solver etwa eine zehnfache Beschleunigung und eine ungefähr tausendfache Verbesserung der Energieeffizienz im Vergleich zu führenden Software‑SAT‑Lösern auf herkömmlichen CPUs.

Was das für zukünftige Computer bedeutet

Einfach ausgedrückt zeigt die Arbeit, dass wir bestimmte notorisch schwierige Ja‑oder‑Nein‑Probleme deutlich schneller und mit weit geringerem Energieaufwand lösen können, wenn wir die Art, wie wir die logischen Regeln formulieren, auf die Art abstimmen, wie eine neue Klasse speicherbasierter Hardware rechnet. Durch die native Unterstützung von XOR‑ und ODER‑Regeln im Chip kann der vorgeschlagene Beschleuniger realistische Aufgaben aus Kryptographie, Kommunikation und Schaltungsentwurf mit kleinerer, kühlerer und schnellerer Hardware bewältigen. Da Rechensysteme zunehmend an Energie‑ und Geschwindigkeitsgrenzen stoßen, könnten solche problemspezifischen In‑Memory‑Ansätze helfen, kritische digitale Infrastrukturen sicher und effizient zu halten.

Zitation: 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

Schlüsselwörter: Boolesche Erfüllbarkeit, In-Memory-Computing, Memristor-Crossbar, Hardwarebeschleuniger, Kryptographie