A veces. Esto es lo que hace que los solucionadores SAT sean útiles.
No puedo hablar específicamente de la factorización de enteros, pero los solucionadores de SAT se usan ampliamente en varios campos, incluida la seguridad y la verificación. Es sorprendente que sea útil reducir los problemas prácticos a instancias de un problema de NP completo ; solo puede funcionar si esas instancias tienen una estructura interna que las hace mucho más fáciles de resolver que las instancias “difíciles” del mismo problema. El hecho de que esas instancias puedan tener millones de variables es una prueba más de que está sucediendo algo especial.
Curiosamente, el algoritmo central utilizado por los solucionadores de SAT modernos sigue siendo, en el fondo, simplemente retroceder. No hay nada loco sucediendo a un alto nivel; funciona bien porque el algoritmo de retroceso aprovecha la estructura de los problemas SAT que surgen de ciertas aplicaciones industriales.
- ¿Podría el basilisco de Roko realmente suceder?
- ¿Cuál es la forma más sencilla de explicar el problema P = NP?
- ¿Cómo se mejora su escritura técnica / científica?
- Dadas N monedas, colocadas en una fila, indexadas 1 a N de izquierda a derecha. Inicialmente todas las monedas muestran cabeza. En cada turno, dos enteros, no necesariamente distintos, A y B entre 1 y N (inclusive) se eligen de manera uniforme al azar. Todas las monedas con un índice de A a B (inclusive) se voltean. ¿Cuál es el número esperado de monedas que muestran la cabeza después de que M gira?
- ¿Cuál es el orden de las operaciones para la notación sigma?
Cuando se visualiza, la estructura es llamativa:
(Visualizaciones en paralelo de una instancia SAT industrial y una aleatoria. La instancia industrial tiene una estructura de red clara, mientras que la aleatoria es un gran blog de líneas. Ilustración creada con SATGraf¹.)
Las variables de estas instancias industriales de SAT se dividen naturalmente en grupos o “comunidades”, lo que significa que la mayoría de los conflictos surgen en “variables puente” que conectan comunidades distintas entre sí. Esta estructura nos permite descartar rápidamente las asignaciones potenciales y retroceder de manera más eficiente al priorizar las variables que tienen más probabilidades de entrar en conflicto.
Los solucionadores de SAT modernos encuentran y usan esta estructura interna con un algoritmo llamado Aprendizaje de cláusulas controladas por conflictos (CDCL). A medida que el solucionador intenta las posibles asignaciones y retrocede, aprende nuevas cláusulas de variables que tienen más probabilidades de causar conflictos y prueba estas cláusulas sintéticas primero . Como la mayoría de las tareas fallan en un pequeño conjunto de variables, estas cláusulas aprendidas permiten que el solucionador falle rápidamente y realice un ciclo a través de una gran cantidad de tareas potenciales rápidamente.
Se ha demostrado empíricamente que el tiempo de ejecución de los solucionadores basados en CDCL está correlacionado con la estructura comunitaria de una instancia SAT². Si su reducción a SAT de otro problema tiene esta estructura, como lo hacen muchas reducciones prácticas, es ciertamente más fácil que una instancia aleatoria, y se puede resolver de manera eficiente con los algoritmos actuales.
Al mismo tiempo, es bastante difícil entender el rendimiento del SAT en la práctica. Pasé algún tiempo trabajando con Z3³ y descubrí que su rendimiento dependía en gran medida tanto del problema que estaba resolviendo como de cómo codifiqué el problema para alimentar al solucionador. Parecía que las únicas personas con alguna intuición sobre cómo se desempeñaban los solucionadores SAT eran investigadores que trabajaban en solucionadores SAT; otras personas, incluso con una amplia experiencia en el uso de solucionadores SAT y SMT, trataban el rendimiento práctico como una especie de caja negra.
notas al pie
SAT “SATGraf: Visualizando la evolución de la estructura de fórmulas SAT en solucionadores” por Zack Newsham, William Lindsay, Vijay Ganesh, Jia Hui Liang, Sebastian Fischmeister y Krzysztof Czarnecki
² “Impacto de la estructura de la comunidad en el desempeño del SAT Solver” por Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard y Laurent Simon
³ Z3 es un solucionador SMT en lugar de un solucionador SAT; considérelo como un solucionador SAT con capacidades adicionales, algunas de las cuales (como la aritmética lineal real) no están codificadas naturalmente en SAT simple. Sin embargo, Z3 usa CDCL para su resolución SAT, y estaba trabajando con un subconjunto de las capacidades de Z3 que encaja perfectamente en SAT simple. (Estaba usando principalmente la teoría de los vectores de bits que se puede compilar para SAT simple en un proceso llamado “explosión de bits”).
