Accelerare nativamente i problemi di soddisfacibilità booleana XOR–CNF ibridi con il calcolo in memoria

Perché risolvere i problemi più velocemente è importante

Molti compiti che influenzano la nostra vita quotidiana — dalla protezione delle comunicazioni online alla progettazione di elettronica più veloce — si riducono a porre a un computer una domanda sì/no: esiste una combinazione di interruttori che renda vera questa grande regola logica? Questo è il problema della soddisfacibilità booleana, o SAT. SAT è notoriamente difficile e, man mano che questi compiti crescono in dimensione e importanza, il tempo e l’energia necessari per risolverli diventano un serio collo di bottiglia. Questo articolo esplora un nuovo modo per potenziare la risoluzione di SAT riprogettando sia la matematica sia l’hardware in modo che cooperino all’interno di un particolare tipo di chip di memoria.

Trasformare regole intrecciate in blocchi più semplici

I solver SAT tradizionali descrivono di solito i problemi usando uno stile di regole logiche costruite con condizioni “OR”. Ma molti problemi industriali reali — come la decodifica di segnali wireless, il test di chip per difetti o l’attacco ad alcuni schemi crittografici — mescolano naturalmente “OR” con “exclusive OR” (XOR), una forma di controllo di parità che cambia quando qualsiasi singolo input cambia. Gli strumenti odierni spesso costringono a riscrivere queste regole XOR usando solo OR, il che aumenta la dimensione del problema e rallenta tutto. Gli autori invece mantengono entrambi i tipi di regole, creando una rappresentazione ibrida più vicina a come i problemi emergono in pratica.

Fare di più con meno componenti

I ricercatori confrontano accuratamente questa descrizione ibrida con quella tradizionale su diverse famiglie di benchmark tratte dalla crittografia e da un problema classico chiamato minimal disagreement parity. Ricostruendo automaticamente la struttura XOR nascosta e applicando prima semplificazioni intelligenti, mostrano che la rappresentazione mista può ridurre il numero di variabili fino a più volte e tagliare il numero di clausole più o meno di un fattore quattro o cinque. In altre parole, la stessa domanda logica può spesso essere posta con molti meno elementi in movimento quando si permette la convivenza di XOR e OR. Problemi più piccoli sono più facili non solo per il software, ma anche per hardware specializzato che ha limiti rigorosi su quante regole può memorizzare contemporaneamente.

Lasciare che siano i chip di memoria a pensare

Per sfruttare questa descrizione più snella, il team progetta un acceleratore dedicato per il “calcolo in memoria”. Invece di trasferire i dati avanti e indietro tra processore e memoria, questo dispositivo esegue gran parte del calcolo dove risiedono i dati, all’interno di griglie di minuscoli elementi elettronici chiamati memristori. Adattano una nota strategia di ricerca locale, WalkSAT, in una nuova variante chiamata WalkSAT-XNF che gestisce nativamente le regole combinate XOR–OR. Ogni passo dell’algoritmo — verificare quali clausole sono violate, stimare quanto incide ciascuna variabile, aggiungere un po’ di rumore per uscire dai vicoli ciechi e capovolgere il candidato migliore — è implementato direttamente in circuiteria analogica sulle matrici crossbar, con circuiti di supporto semplici che scelgono quale variabile invertire dopo.

Dimostrare che funziona in laboratorio e nelle simulazioni

Gli autori costruiscono prima un piccolo prototipo usando chip a memristori per dimostrare che l’hardware analogico può valutare fedelmente le clausole e guidare la ricerca, anche in presenza di variazioni produttive e rumore elettrico. Esperimenti su un’istanza di test di dimensioni modeste mostrano che il comportamento dell’hardware corrisponde strettamente alle simulazioni ideali. Modellano poi un progetto più avanzato a 28 nanometri e lo valutano su famiglie di problemi crittografici e di parità. Poiché la descrizione ibrida comprime più informazione in meno clausole, l’acceleratore richiede molta meno memoria on-chip e consuma molto meno energia per passo rispetto a una versione limitata a sole regole OR. Complessivamente, il solver ibrido in memoria raggiunge circa un’accelerazione di un fattore dieci e un miglioramento dell’efficienza energetica di circa mille volte rispetto ai principali solver SAT software eseguiti su CPU convenzionali.

Cosa significa per i computer del futuro

In termini semplici, il lavoro mostra che possiamo risolvere certi problemi sì/no notoriamente difficili molto più velocemente e con molta meno potenza adeguando il modo in cui scriviamo le regole logiche al modo in cui un nuovo tipo di hardware basato sulla memoria calcola. Supportando nativamente all’interno del chip sia le regole XOR sia quelle OR, l’acceleratore proposto può affrontare compiti realistici di crittografia, comunicazioni e progettazione di circuiti usando hardware più piccolo, più freddo e più veloce. Con i sistemi di calcolo sempre più in tensione rispetto ai limiti di energia e velocità, approcci specifici per problema e basati sulla memoria potrebbero aiutare a mantenere l’infrastruttura digitale critica sicura ed efficiente.

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

Parole chiave: Soddisfacibilità booleana, calcolo in memoria, crossbar a memristori, acceleratori hardware, crittografia