Un generador de instancias aleatorias SAT basado en modularidad

Hoy en día, muchas instancias industriales de SAT pueden resolverse de manera eficiente por los solucionadores de SAT modernos. Sin embargo, el número de instancias del mundo real es finito. Por lo tanto, el proceso de desarrollo y prueba de técnicas de solución de SAT puede beneficiarse de nuevos modelos de fórmulas aleatorias que capturan más realísticamente las características de los problemas del mundo real. En muchos trabajos, se ha analizado la estructura de las instancias industriales representándolas como gráficos y estudiando algunas de sus propiedades, como la modularidad. En este documento, utilizamos la modularidad, o estructura comunitaria, para definir un nuevo modelo de instancias aleatorias pseudo-industriales de SAT, llamado Comunidad de Adhesión. Demostramos que el punto de transición de fase, si existe, es independiente de la modularidad. Evaluamos la adecuación de este modelo a problemas industriales reales en términos de rendimiento de los solucionadores de SAT y mostramos que los solucionadores modernos realmente explotan esta estructura comunitaria.