Aceleración nativa de problemas híbridos XOR–CNF de satisfacibilidad booleana mediante computación en memoria

Por qué importa resolver problemas más rápido

Muchas tareas que moldean nuestra vida cotidiana —desde asegurar las comunicaciones en línea hasta diseñar electrónica más rápida— se reducen a plantear a un ordenador una pregunta de sí o no: ¿existe una combinación de interruptores que haga verdadera esta gran regla lógica? Este es el problema de satisfacibilidad booleana, o SAT. SAT es famosamente difícil, y a medida que estas tareas crecen en tamaño e importancia, el tiempo y la energía necesarios para resolverlas se convierten en un cuello de botella. Este artículo explora una nueva forma de acelerar la resolución de SAT rediseñando tanto las matemáticas como el hardware para que trabajen juntos dentro de un tipo especial de chip de memoria.

Convertir reglas enredadas en bloques constructivos más simples

Los solucionadores SAT tradicionales suelen describir los problemas usando un estilo de regla lógica basado en condiciones “OR”. Pero muchos problemas industriales reales —como decodificar señales inalámbricas, probar chips en busca de fallos o atacar ciertos esquemas criptográficos— mezclan de forma natural “OR” con “exclusive OR” (XOR), un tipo de comprobación de paridad que cambia cuando cualquiera de las entradas cambia. Las herramientas actuales a menudo fuerzan que estas reglas XOR se reescriban usando solo OR, lo que hincha el tamaño del problema y ralentiza todo. Los autores, en cambio, conservan ambos tipos de reglas, creando una descripción híbrida que se aproxima más a cómo surgen los problemas en la práctica.

Hacer más con menos componentes

Los investigadores comparan cuidadosamente esta descripción híbrida con la tradicional en varias familias de pruebas procedentes de la criptografía y de un problema clásico llamado paridad de desacuerdo mínimo. Al reconstruir automáticamente la estructura XOR oculta y aplicar simplificaciones inteligentes primero, muestran que la representación mixta puede reducir el número de variables hasta varias veces y recortar el número de cláusulas aproximadamente por un factor de cuatro a cinco. Dicho de otro modo, la misma pregunta lógica a menudo puede plantearse con muchos menos elementos móviles cuando se permite la coexistencia de XOR y OR. Los problemas más pequeños son más fáciles no solo para el software, sino también para hardware especializado que tiene límites estrictos sobre cuántas cláusulas puede almacenar a la vez.

Dejar que los chips de memoria hagan el razonamiento

Para explotar esta descripción más compacta, el equipo diseña un acelerador dedicado de “computación en memoria”. En lugar de mover datos constantemente entre un procesador y la memoria, este dispositivo realiza gran parte del cómputo donde residen los datos, dentro de rejillas de diminutos elementos electrónicos llamados memristores. Adaptan una estrategia de búsqueda local conocida, WalkSAT, a una nueva variante llamada WalkSAT-XNF que maneja de forma nativa las reglas combinadas XOR–OR. Cada paso del algoritmo —comprobar qué cláusulas están incumplidas, estimar cuánto importa cada interruptor, añadir un poco de ruido para escapar de callejones sin salida y cambiar el mejor candidato— se implementa directamente en circuitería analógica sobre las matrices cruzadas, con circuitos de apoyo sencillos que eligen qué variable voltear a continuación.

Demostrar que funciona en el laboratorio y en simulaciones

Los autores primero construyen un pequeño prototipo usando chips de memristores para demostrar que el hardware analógico puede evaluar cláusulas y guiar la búsqueda de forma fiel, incluso en presencia de variaciones de fabricación y ruido eléctrico. Experimentos con una instancia de prueba de tamaño modesto muestran que el comportamiento del hardware coincide estrechamente con simulaciones ideales. Luego modelan un diseño más avanzado en tecnología de 28 nanómetros y lo evalúan en familias de problemas criptográficos y de paridad. Debido a que la descripción híbrida empaqueta más información en menos cláusulas, el acelerador necesita mucha menos memoria en chip y consume mucha menos energía por paso que una versión restringida a reglas solo OR. En conjunto, el solucionador híbrido en memoria logra aproximadamente una aceleración de diez veces y una mejora en eficiencia energética de alrededor de mil veces en comparación con los principales solucionadores SAT por software ejecutándose en CPUs convencionales.

Qué significa esto para los ordenadores del futuro

En términos sencillos, el trabajo muestra que podemos resolver ciertos problemas de sí o no notoriamente duros mucho más rápido y con mucha menos energía al alinear la forma en que escribimos las reglas lógicas con la forma en que un nuevo tipo de hardware basado en memoria calcula. Al soportar de forma nativa tanto reglas XOR como OR dentro del chip, el acelerador propuesto puede abordar tareas realistas de criptografía, comunicaciones y diseño de circuitos usando hardware más pequeño, más frío y más rápido. A medida que los sistemas informáticos tensionan cada vez más los límites de energía y velocidad, estos enfoques específicos por problema y basados en memoria podrían ayudar a mantener la infraestructura digital crítica segura y eficiente.

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

Palabras clave: Satisfacibilidad booleana, computación en memoria, cruzamiento de memristores, aceleradores hardware, criptografía