Los solucionadores SAT son muy importantes en los ataques algebraicos , por ejemplo, walkingat y minisat .
Sin embargo, al resolver los problemas de referencia disponibles aquí, existe una enorme diferencia de rendimiento entre los dos: Walksat es mucho más rápido que el minisat para estos problemas. ¿Por qué es esto?
Esta implementación de Walkat parece tener algunas mejoras en el rendimiento. ¿Hay alguna razón por la que no se haya incluido en las competiciones SAT internacionales ?
ds.algorithms
sat
ir01
fuente
fuente
Respuestas:
Sí, hay una gran diferencia entre MiniSAT y WalkSAT. Primero, aclaremos: MiniSAT es una implementación específica de la clase genérica de algoritmos DPLL / CDCL que utilizan el seguimiento y el aprendizaje de cláusulas, mientras que WalkSAT es el nombre general de un algoritmo que alterna entre pasos codiciosos y pasos aleatorios.
En general, DPLL / CDCL es mucho más rápido en instancias SAT estructuradas, mientras que WalkSAT es más rápido en k-SAT aleatorio . Las instancias de SAT industriales y aplicadas tienden a tener mucha estructura, por lo que DPLL / CDCL es dominante en la mayoría de los solucionadores de SAT modernos. Sin embargo, una técnica de instancia a instancia puede ganar, que es una de las razones por las cuales los solucionadores de carteras se han vuelto populares.
Tengo muchos problemas con su afirmación de que WalkSAT es mucho más rápido que MiniSAT en las instancias de esa página. Por un lado, hay gigabytes de instancias SAT allí: ¿en cuántas intentaste compararlas? WalkSAT no es del todo competitivo en la mayoría de las instancias estructuradas, por lo que a menudo no se ve en las competiciones.
En una nota al margen: Vijay tiene razón en que MiniSAT sigue siendo relevante. En realidad, debido a que es de código abierto y está bien escrito, MiniSAT es el solucionador que hay que superar para demostrar que una optimización dada es prometedora. Muchas personas modifican MiniSAT para mostrar sus optimizaciones: eche un vistazo a la categoría "Hack de MiniSAT" en las recientes competiciones SAT.
fuente
Un buen artículo para leer sobre este tema es este de Nudelman et al . El objetivo principal del documento es determinar las características fáciles de calcular de las instancias de SAT que pueden decirle qué algoritmos tienen un mejor rendimiento y cuáles no. Con esta técnica, es posible construir un algoritmo basado en cartera que analizará rápidamente una instancia problemática y luego resolverá la instancia con el algoritmo más apropiado. Hay una progresión de documentos que sigue a esa; Google SATzilla mostrará mucho material de lectura.
fuente