Accelerera hybrid XOR–CNF Boolean satisfiabilitetsproblem nativt med in-memory computing

Varför snabbare problemlösning spelar roll

Många uppgifter som påverkar vår vardag — från att säkra onlinetrafik till att designa snabbare elektronik — kokar ner till att ställa en ja-eller-nej-fråga till en dator: finns det en kombination av växlar som gör att denna stora logiska regel blir sann? Detta är det Boolean satisfiability-, eller SAT-, problemet. SAT är välkänt svårt, och när dessa uppgifter växer i omfattning och betydelse blir tiden och energin som krävs för att lösa dem en huvudbegränsning. Denna artikel utforskar ett nytt sätt att snabba upp SAT-lösning genom att omdesigna både matematiken och hårdvaran så att de arbetar tillsammans inuti en speciell typ av minneschip.

Att förvandla ihoptrasslade regler till enklare byggstenar

Traditionella SAT-lösare beskriver vanligtvis problem med en stil av logiska regler byggda av "ELLER"-villkor. Men många verkliga industriella problem — som att avkoda trådlösa signaler, testa kretsar för fel eller angripa vissa kryptografiska scheman — blandar naturligt "ELLER" med "exklusivt ELLER" (XOR), en sorts paritetskontroll som växlar när någon enskild ingång ändras. Dagens verktyg tvingar ofta dessa XOR-regler att skrivas om med bara ELLER, vilket blåser upp problemets storlek och saktar ner allt. Författarna behåller istället båda typerna av regler och skapar en hybridbeskrivning som ligger närmare hur problemen uppstår i praktiken.

Få mer gjort med färre delar

Forskarna jämför noggrant denna hybridbeskrivning med den traditionella över flera referensfamiljer hämtade från kryptografi och ett klassiskt testproblem kallat minimal disagreement parity. Genom att automatiskt återskapa dold XOR-struktur och först tillämpa smarta förenklingar visar de att den blandade representationen kan minska antalet variabler med upp till flera gånger och skära ner antalet satser med ungefär en faktor fyra till fem. Med andra ord kan samma logiska fråga ofta uttryckas med betydligt färre rörliga delar när man tillåter att XOR och ELLER samexisterar. Mindre problem är enklare inte bara för mjukvara utan också för specialiserad hårdvara som har strikta gränser för hur många satser den kan lagra samtidigt.

Låta minneschippen göra tänkandet

För att utnyttja denna mer kompakta beskrivning designar teamet en dedikerad "in-memory computing"-accelerator. Istället för att skicka data fram och tillbaka mellan processor och minne utför denna enhet mycket av beräkningen där datan ligger, inuti gitter av små elektroniska element kallade memristorer. De anpassar en känd lokal sökstrategi, WalkSAT, till en ny variant kallad WalkSAT-XNF som nativt hanterar de kombinerade XOR–ELLER-reglerna. Varje steg i algoritmen — att kontrollera vilka satser som bryts, uppskatta hur mycket varje variabel betyder, lägga till lite slump för att undkomma återvändsgränder och växla den bästa kandidaten — implementeras direkt i analog krets på crossbar-matriserna, med enkla stödkretsar som väljer vilken variabel som ska ändras härnäst.

Bevisa att det fungerar i labbet och i simuleringar

Författarna bygger först en liten prototyp med memristorchips för att demonstrera att den analoga hårdvaran troget kan utvärdera klausuler och styra sökningen, även i närvaro av tillverkningsvariationer och elektriskt brus. Experiment på ett måttligt stort testfall visar att hårdvarans beteende stämmer väl överens med ideala simuleringar. De modellerar sedan en mer avancerad 28-nanometers design och jämför prestanda på familjer av kryptografiska och paritetsproblem. Eftersom hybridbeskrivningen packar mer information i färre klausuler behöver acceleratoren mycket mindre on-chip-minne och förbrukar avsevärt mindre energi per steg än en version begränsad till endast ELLER-regler. Sammantaget uppnår den hybrida in-memory-lösaren ungefär en tiofaldig hastighetsökning och omkring tusen gånger bättre energieffektivitet jämfört med ledande mjukvaru-SAT-lösare som körs på konventionella CPU:er.

Vad detta betyder för framtidens datorer

Enkelt uttryckt visar arbetet att vi kan lösa vissa ökända svåra ja-eller-nej-problem mycket snabbare och med mycket mindre effekt genom att anpassa hur vi uttrycker de logiska reglerna till hur en ny typ av minnesbaserad hårdvara beräknar. Genom att nativt stödja både XOR- och ELLER-regler inne i chippet kan den föreslagna acceleratoren angripa realistiska kryptografiska, kommunikations- och kretsdesignuppgifter med mindre, svalare och snabbare hårdvara. Eftersom datorsystem i allt högre grad pressas mot gränser för energi och hastighet kan sådana uppgiftsspecifika, in-memory-lösningar bidra till att hålla kritisk digital infrastruktur säker och effektiv.

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

Nyckelord: Boolean satisfiabilitet, in-memory computing, memristor-crossbar, hårdvaruacceleratorer, kryptografi