La satisfacibilidad booleana, el problema SAT, es el motor detrás de una amplia gama de tareas computacionales, desde la verificación de chips hasta la ciberseguridad y la verificación formal de pruebas. Los algoritmos que lo resuelven han sido refinados por expertos humanos durante décadas, mejorando incrementalmente el rendimiento mediante ingeniosas heurísticas para la selección de variables, la reducción de cláusulas y la sincronización de reinicios.
Un estudio publicado en Nature Communications el 17 de julio muestra que los modelos de lenguaje grandes ahora pueden generar heurísticas para solucionadores SAT que superan a las diseñadas por humanos, logrando una mejora del 40 % en el tiempo de ejecución sobre un solucionador base y superando las mejores versiones ajustadas de sistemas de última generación en 8 de 11 conjuntos de datos de referencia.
Lo que hicieron los investigadores
El equipo, liderado por Ke Wei de la Universidad de Fudan y Shaowei Cai de la Academia China de Ciencias, construyó un marco llamado AutoModSAT. La idea clave fue que las bases de código de los solucionadores SAT son masivas y enredadas: el popular solucionador Kissat alcanza los 250,000 tokens. Pedirle a un LLM que modifique directamente una base de código así sería inútil. En cambio, los investigadores modularizaron un solucionador CDCL (aprendizaje de cláusulas impulsado por conflictos), exponiendo exactamente siete funciones heurísticas, la sincronización de reinicios, la reducción de cláusulas, el aumento de actividad de variables y otras, como un espacio de búsqueda limpio.
Con el solucionador modularizado, el sistema alterna entre tres agentes LLM: un Codificador genera nuevo código heurístico en C++, un Evaluador filtra el código semánticamente idéntico a heurísticas existentes, y un Reparador corrige errores de compilación. Las heurísticas con mejor rendimiento se mantienen en un bucle evolutivo. Todo el proceso utiliza 50 llamadas LLM por dominio de problema y se basa en DeepSeek-V3, elegido por su rendimiento competitivo a bajo costo.
Lo que encontró
En 11 conjuntos de datos de referencia que abarcan problemas de competencias SAT, verificación de automatización de diseño electrónico (EDA) y rompecabezas combinatorios, AutoModSAT generó heurísticas optimizadas que ofrecieron una mejora promedio del 40 % en la puntuación PAR-2 (una métrica estándar que penaliza las instancias no resueltas) sobre el solucionador modular base.
En comparación con versiones ajustadas de los solucionadores de última generación Kissat y CaDiCaL, AutoModSAT ganó en 8 de 11 conjuntos de datos con una aceleración promedio de aproximadamente el 20 %. En el problema de asignación de registros, la heurística descubierta por el LLM resolvió 18 de 20 instancias mientras que la base resolvió menos de 6. En el problema de verificación de seguridad de tablas hash, con 11.7 millones de variables y 53.6 millones de cláusulas, AutoModSAT produjo una puntuación PAR-2 de 3,302 frente a los 7,322 del mejor competidor.
El LLM también inventó heurísticas que no habían sido descritas previamente en la literatura. Para la estrategia de reinicio, generó un método dinámico que utiliza promedios móviles de puntuaciones de calidad de cláusulas, un enfoque novedoso que no formaba parte de ningún solucionador existente.
Por qué es importante
Esto es cualitativamente diferente del ajuste automatizado de hiperparámetros, que ajusta perillas existentes. AutoModSAT genera nuevo código algorítmico, heurísticas que los expertos humanos no habían concebido. El costo total es de unos pocos dólares en tarifas de API por ejecución de optimización, lo que lo hace práctico para el despliegue industrial real.
El enfoque de modularización en sí mismo es la afirmación más sólida del artículo: hacer que el código del solucionador sea amigable para los LLM no es opcional sino fundamental. El enfoque podría extenderse a otros solucionadores complejos para programación lineal mixta, satisfacción de restricciones y demostración de teoremas.
Advertencias
El solucionador base (ModSAT) es más simple que sistemas de última generación como Kissat, que tienen décadas de optimización. Algunas ganancias reflejan la debilidad relativa de la base. El marco solo expone siete funciones heurísticas y no puede tocar los parámetros de preprocesamiento de alto nivel, que son críticos en algunos conjuntos de datos. En el conjunto de datos Zamkeller, Kissat ajustado superó a AutoModSAT por un factor de cuatro porque la brecha estaba en un componente que el sistema no podía modificar.
El artículo se publica en Nature Communications (DOI: 10.1038/s41467-026-74949-2) por Y. Sun, F. Ye, Z. Chen, K. Wei y S. Cai.
Fuentes
1. Y. Sun, F. Ye, Z. Chen, K. Wei, S. Cai, “Discovering Heuristics in a Complex SAT Solver with Large Language Models,” Nature Communications (2026). DOI: 10.1038/s41467-026-74949-2
Traducido por Alessandra