La publicación de blog de Scott Aaronson hoy dio una lista de interesantes problemas / tareas abiertas en complejidad. Uno en particular me llamó la atención:
Cree una biblioteca pública de instancias 3SAT, con la menor cantidad de variables y cláusulas posibles, que tendrían consecuencias notables si se resuelven. (Por ejemplo, instancias que codifican los desafíos de factorización de RSA). Investigue el rendimiento de los mejores solucionadores de SAT actuales en esta biblioteca.
Esto provocó mi pregunta: ¿Cuál es la técnica estándar para reducir los problemas de RSA / factorización a SAT y qué tan rápido es? ¿Existe tal reducción estándar?
Para ser claros, por "rápido" no me refiero al tiempo polinomial. Me pregunto si tenemos límites superiores más estrictos en la complejidad de la reducción. Por ejemplo, ¿hay una reducción cúbica conocida?
fuente
Extendiendo lo que escribió @Amir, me encontré con la siguiente página web que alberga un generador CNF para factorizar circuitos que uno podría, por ejemplo, ejecutar en algunos de los números (ahora inactivos) del Desafío de Factoring RSA . Las instancias generadas están en DIMACS formato que directamente se puede alimentar a cualquiera de los competidores actuales en el anual SAT solucionador de la competencia . Con respecto a las instancias difíciles de SAT en general, los problemas de referencia dados en el sitio de competencia SAT parecen ser bastante útiles, también la clasificación en aleatoria / artesanal / industrial es agradable.
fuente
Aquí hay un documento sobre la generación de instancias SAT a partir de la factorización:
Horie, S. y Watanabe, O. [1997] " Generación de instancias difíciles para SAT " Algoritmos y Computación 1350: 22-31 ( pdf )
fuente
ToughSat de Henry Yuen y Joseph Bebel es otra herramienta similar a la vinculada por @Martin, que genera fórmulas CNF que codifican instancias de factoring y otros problemas difíciles.
fuente
Ver
satfactor
:Convierta la factorización entera en un problema booleano de SATISFIABILIDAD
Visión general
Los factores determinantes de un gran número entero han sido de interés para el Hombre desde al menos los tiempos de Euclides. No se conoce un algoritmo general para este problema que se escale en menos tiempo exponencial con respecto al número de bits necesarios para representar el número entero.
Lo que hace este código
Convierte un problema de factorización de enteros en un problema booleano de SATISFIABILIDAD. Si el solucionador SAT soluciona el problema, extrae los factores enteros.
Los solucionadores de satisfacción boolen mejoran cada año. Cada 2 años, se lleva a cabo una competencia internacional entre solucionadores (ver http://www.satcompetition.org/ y http://www.satlive.org/ ). ¿Qué tan bien pueden hacer estos solucionadores de vanguardia contra uno de los problemas matemáticos abiertos más antiguos que existen?
Este proyecto tiene 2 propósitos principales:
1) ¡Convertir el problema y factorizar un número entero de interés!
2) Cree rápidamente un problema de SATISFIABILIDAD solucionable o insoluble, cuya dificultad es fácilmente controlada por el creater.
- Para crear un problema de SATISFIABILIDAD sin solución, simplemente codifique un número primo.
- Para crear problemas más difíciles pero solucionables, elija números compuestos más grandes con menos factores.
¡El número de intereses puede ser de cualquier tamaño!
Hay algunos solucionadores de SATISFIABILIDAD de código abierto. Ver http://www.satlive.org/ para algunos de estos.
Construir
make -C src /
Cómo
Ingrese un número de interés en su forma binaria:
bin / iencode 10101> composite.21
// resuelve con tu solucionador favorito y coloca los resultados en solution.txt
bin / extract-sat composite.21 solution.txt
La salida sería:
00011
00111
que son representaciones binarias para enteros decimales 3 y 7, los factores de 21.
Si un entero de entrada tiene más de 2 factores, y el problema SAT está resuelto, la salida será solo dos de los factores. Es posible que estos no sean números primos (puede probarlo fácilmente en Maxima, Maple o Mathematica).
No todos los resultados de los solucionadores SAT tienen el mismo formato. Es posible que necesite un poco de esos resultados. extract-sat requiere un archivo de solución que contenga una lista de enteros (en cualquier número de líneas). Por ejemplo,
1 -2 3 4 -5 ...
fuente