Accélération native des problèmes de satisfiabilité booléenne XOR–CNF hybrides par calcul en mémoire

Pourquoi résoudre plus vite a de l’importance

De nombreuses tâches qui façonnent notre quotidien — de la sécurisation des communications en ligne à la conception d’électronique plus rapide — se ramènent à poser à un ordinateur une question oui/non : existe-t-il une combinaison d’interrupteurs qui rende vraie cette grande règle logique ? C’est le problème de satisfiabilité booléenne, ou SAT. Le SAT est réputé difficile, et à mesure que ces tâches prennent de l’ampleur et de l’importance, le temps et l’énergie nécessaires pour les résoudre deviennent un goulot d’étranglement majeur. Cet article explore une nouvelle façon d’accélérer la résolution de SAT en repensant conjointement les mathématiques et le matériel pour qu’ils fonctionnent ensemble à l’intérieur d’un type particulier de puce mémoire.

Transformer des règles emmêlées en briques plus simples

Les solveurs SAT classiques décrivent généralement les problèmes en utilisant un style de règle logique construit à partir de conditions « OU ». Mais de nombreux problèmes industriels réels — comme le décodage de signaux sans fil, les tests de puces pour détecter des défauts, ou l’attaque de certains schémas cryptographiques — mêlent naturellement le « OU » et le « OU exclusif » (XOR), une sorte de contrôle de parité qui change quand une entrée change. Les outils actuels contraignent souvent ces règles XOR à être réécrites en termes d’OU uniquement, ce qui gonfle la taille du problème et ralentit tout. Les auteurs conservent au contraire les deux types de règles, créant une représentation hybride plus proche de la façon dont les problèmes apparaissent en pratique.

Faire plus avec moins d’éléments

Les chercheurs comparent soigneusement cette description hybride à la description traditionnelle sur plusieurs familles de benchmarks tirées de la cryptographie et d’un problème classique appelé parité de désaccord minimal. En reconstruisant automatiquement la structure XOR cachée et en appliquant d’abord des simplifications intelligentes, ils montrent que la représentation mixte peut réduire le nombre de variables jusqu’à plusieurs fois et diminuer le nombre de clauses d’environ un facteur quatre à cinq. Autrement dit, la même question logique peut souvent être posée avec bien moins d’éléments mobiles lorsque l’on autorise la coexistence de XOR et d’OU. Les problèmes plus petits sont plus faciles non seulement pour les logiciels, mais aussi pour le matériel spécialisé qui dispose de limites strictes sur le nombre de clauses qu’il peut stocker simultanément.

Laisser les puces mémoire réfléchir

Pour exploiter cette description plus compacte, l’équipe conçoit un accélérateur dédié de « calcul en mémoire ». Plutôt que de faire transiter les données entre un processeur et la mémoire, cet appareil effectue une grande partie du calcul là où résident les données, à l’intérieur de grilles de petits éléments électroniques appelés mémristors. Ils adaptent une stratégie de recherche locale connue, WalkSAT, en une nouvelle variante appelée WalkSAT-XNF qui gère nativement les règles combinées XOR–OU. Chaque étape de l’algorithme — vérifier quelles clauses sont violées, estimer l’importance de chaque variable, ajouter un peu de bruit pour échapper aux impasses, et inverser le meilleur candidat — est implémentée directement en circuits analogiques sur les réseaux crossbar, avec des circuits de soutien simples choisissant quelle variable inverser ensuite.

Preuve par l’expérience et par simulation

Les auteurs construisent d’abord un petit prototype utilisant des puces à mémristors pour démontrer que le matériel analogique peut évaluer fidèlement les clauses et guider la recherche, même en présence de variations de fabrication et de bruit électrique. Des expériences sur une instance de test de taille modeste montrent que le comportement du matériel correspond étroitement aux simulations idéales. Ils modélisent ensuite une conception plus avancée en 28 nanomètres et la testent sur des familles de problèmes cryptographiques et de parité. Parce que la description hybride condense plus d’information dans moins de clauses, l’accélérateur requiert beaucoup moins de mémoire sur puce et consomme bien moins d’énergie par étape qu’une version limitée aux seules clauses OU. Dans l’ensemble, le solveur hybride en mémoire obtient environ un gain de vitesse d’un facteur dix et une amélioration de l’efficacité énergétique d’environ mille fois par rapport aux meilleurs solveurs SAT logiciels s’exécutant sur des CPU conventionnels.

Ce que cela signifie pour les ordinateurs de demain

En termes simples, ce travail montre que l’on peut résoudre certains problèmes oui/non notoirement difficiles beaucoup plus rapidement et avec beaucoup moins d’énergie en adaptant la façon dont on écrit les règles logiques à la façon dont un nouveau type de matériel basé sur la mémoire calcule. En prenant en charge nativement à la fois les règles XOR et OU à l’intérieur de la puce, l’accélérateur proposé peut traiter des tâches réalistes de cryptographie, de communications et de conception de circuits en utilisant un matériel plus petit, plus frais et plus rapide. Alors que les systèmes informatiques poussent toujours plus loin les limites d’énergie et de vitesse, ces approches spécifiques au problème et basées sur le calcul en mémoire pourraient aider à maintenir l’infrastructure numérique critique sécurisée et efficace.

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

Mots-clés: Satisfiabilité booléenne, calcul en mémoire, réseau de mémristors, accélérateurs matériels, cryptographie