ES
Un muestreador en GPU encuentra en paralelo entradas válidas para circuitos
SAT Sampling at Scale via GPU-based Boolean Constraint Propagation · arXiv:2610.28805
En palabras sencillas
Quienes prueban circuitos necesitan patrones de entrada válidos que hagan que el circuito produzca salidas elegidas, incluso salidas que rara vez se alcanzan con entradas aleatorias normales. Este artículo presenta Gpap-S, un muestreador para GPU que prueba muchas asignaciones aleatorias a la vez y conserva solo las que terminan satisfaciendo las reglas del circuito.
En pruebas con colecciones de circuitos, Gpap-S generó muestras más rápido que los muestreadores de gradiente para GPU comparados cuando los objetivos eran poco frecuentes; Demotic no produjo ninguna muestra en cinco de sus siete instancias probadas con esos objetivos.
Una prueba estadística independiente aceptó Gpap-S en 65 instancias conservadas. Ese resultado es evidencia según los criterios de la prueba, no una garantía de uniformidad perfecta.
La investigación
La verificación de circuitos necesita entradas válidas que lleven un diseño a salidas elegidas, incluidos patrones poco frecuentes que rara vez se alcanzan con entradas aleatorias.
¿Puede una GPU generar muchas entradas válidas sin perder muestras útiles, como puede ocurrir cuando los métodos basados en gradientes redondean sus resultados a asignaciones booleanas?
Gpap-S genera muestras de entradas válidas para circuitos mediante muchos intentos aleatorios de propagación en paralelo en una GPU y conserva las asignaciones completas.
Gpap-S ejecuta en una GPU muchos intentos aleatorios de decisión y propagación, descarta las contradicciones y conserva las asignaciones completas que satisfacen la fórmula como muestras. Así, sus resultados son válidos sin redondear ni corregir las asignaciones.
En las filas comunicadas para cada conjunto de circuitos, objetivo y profundidad, Gpap-S tuvo tasas estables de muestreo más altas que CMSGen, un muestreador para CPU.
Sus tasas también superaron a las de los muestreadores de gradiente para GPU comparados con objetivos poco frecuentes, aunque cada comparación cubrió el conjunto de circuitos propio de ese muestreador y solo contó instancias en las que ambas herramientas generaron muestras.
Los resultados proceden de un conjunto acotado de pruebas con circuitos y comparan herramientas bajo el hardware, la configuración y las reglas de medición indicados.
Barbarik aceptó Gpap-S en 65 instancias conservadas, pero este resultado estadístico no garantiza formalmente que las muestras sean uniformes.
Qué muestran las pruebas
- El problema de las entradas poco frecuentes
El artículo presenta Gpap-S, un método para GPU que genera muestras de entradas válidas para circuitos. La pregunta es cómo producir muchas entradas que satisfagan las restricciones, incluidas las que alcanzan patrones de salida poco frecuentes.
Los muestreadores SAT para CPU pueden encontrar asignaciones válidas, mientras que los muestreadores de gradiente para GPU pueden perder resultados útiles cuando pocas asignaciones redondeadas satisfacen un objetivo poco frecuente.
- Otro tipo de muestreador para GPU
Gpap-S usa Gpap, un motor que propaga muchas asignaciones parciales independientes sobre una misma fórmula compartida. En cada intento, asigna variables y sigue las consecuencias de esas decisiones.
Las asignaciones que terminan satisfaciendo la fórmula se convierten en muestras; los intentos que llegan a una contradicción se descartan. Así, cada muestra generada es válida sin tener que redondear ni corregir una asignación.
- Tasas más altas que CMSGen
En las comparaciones con CMSGen, el muestreador para CPU, Gpap-S tuvo tasas estables más altas de muestras por segundo en las filas comunicadas para cada conjunto de circuitos, objetivo y profundidad. Ambas herramientas recibieron el mismo circuito y profundidad y tuvieron 60 segundos para muestrear, pero el codificador de Gpap-S repitió la simplificación del circuito y después añadió una pasada dc2.
Gpap-S se ejecutó en una GPU y CMSGen en un núcleo de CPU. Las medias por fila solo incluyen instancias en las que ambas herramientas generaron muestras.
- Objetivos poco frecuentes y calidad de las muestras
Las comparaciones con los muestreadores de gradiente para GPU usaron la colección de circuitos propia de cada herramienta. Con objetivos originales, Gpap-S tuvo tasas comunicadas más altas; con objetivos poco frecuentes, su ventaja frente a Recurrent fue mayor, mientras que Demotic no generó muestras en cinco de las siete instancias probadas con esos objetivos.
Una prueba estadística también aceptó Gpap-S y CMSGen en las 65 instancias conservadas. La aceptación aporta evidencia sobre la calidad de las muestras según los criterios de la prueba, pero no demuestra uniformidad.
- El trabajo descartado limita la ventaja
La ventaja en tasa tiene un coste con objetivos secuenciales poco frecuentes. Gpap-S descarta los intentos conflictivos sin aprender de ellos, por lo que puede dedicar mucho más trabajo de propagación a cada muestra que CMSGen, que aprende de los conflictos y retrocede.
Los autores midieron un trabajo por muestra 6,41 y 6,59 veces mayor que el de CMSGen a 25 y 50 ciclos, respectivamente. Estas fueron también las filas en que Gpap-S obtuvo sus menores aumentos medidos de velocidad frente a CMSGen.
Detalles
- Autores del paper original
- Alexander Nadel, Yogev Shalmon, Ofer Strichman
- Enviado a arXiv
- Licencia
- CC BY 4.0