e-boost: Extracción de E-Grafos Mejorada con Heurísticas Adaptativas y Solución Exacta

Los e-grafos han atraído un creciente interés en muchos campos, particularmente en la síntesis lógica y la verificación formal. La extracción de e-grafos es un problema difícil de optimización combinatoria NP-duro. Requiere identificar términos óptimos de una cantidad exponencial de expresiones equivalentes, sirviendo como el principal cuello de botella en las tareas de optimización basadas en e-grafos. Sin embargo, los métodos de extracción tradicionales enfrentan una compensación crítica: los enfoques heurísticos ofrecen velocidad pero sacrifican optimalidad, mientras que los métodos exactos proporcionan soluciones óptimas pero enfrentan costos computacionales prohibitivos en problemas prácticos. Presentamos e-boost, un marco novedoso que cierra esta brecha a través de tres innovaciones clave: (1) extracción heurística paralelizada que aprovecha la débil dependencia de datos para calcular los costos de DAG de manera concurrente, permitiendo un rendimiento eficiente en múltiples hilos sin sacrificar la calidad de extracción; (2) poda adaptativa del espacio de búsqueda que emplea un mecanismo de umbral parametrizado para retener solo candidatos prometedores, reduciendo dramáticamente el espacio de soluciones mientras se preservan soluciones cercanas a lo óptimo; y (3) solución exacta inicializada que formula el problema reducido como un Programa Lineal Entero con capacidades de inicio en caliente, guiando a los solucionadores hacia soluciones de alta calidad más rápido. A través de los diversos benchmarks en los campos de verificación formal y síntesis lógica, e-boost demuestra un aumento de velocidad de 558 veces en tiempo de ejecución en comparación con los enfoques exactos tradicionales (ILP) y una mejora de rendimiento del 19.04% sobre el marco de extracción de última generación (SmoothE). En tareas realistas de síntesis lógica, e-boost produce mejoras del 7.6% y 8.1% en área en comparación con herramientas de síntesis convencionales con dos diferentes bibliotecas de asignación tecnológica. e-boost está disponible en https://github.com/Yu-Maryland/e-boost.