Reducción rápida de RSA a SAT

28

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?

Huck Bennett
fuente

Respuestas:

26

Un enfoque para codificar la factorización (RSA) a SAT es utilizar circuitos multiplicadores (cada circuito puede codificarse como CNF).

Supongamos que se nos da un número entero con bits, . Estamos interesados en la búsqueda de dos bits enteros y cuyo producto es .2 n C = ( c 1 , c 2 , , c 2 n ) 2 n A = ( a 1 , , a n ) A = ( b 1 , , b n ) C = A Bdo2nortedo=(do1,do2,,do2norte)2norteUNA=(una1,,unanorte)UNA=(si1,,sinorte)do=UNAsi

La codificación más ingenua puede ser algo como esto: sabemos que

do2norte=unanortesinorte
do2norte-1=(unanortesinorte-1)Xor(unanorte-1sinorte)
c 2 n - 2 =( a n b n - 2 )xor( a n - 1 b n - 1 )xor( a n - 2 b n )xor d 2 n - 1
dounarry:re2norte-1=(unanortesinorte-1)(unanorte-1sinorte)
do2norte-2=(unanortesinorte-2)Xor(unanorte-1sinorte-1)Xor(unanorte-2sinorte)Xorre2norte-1
...

Luego, utilizando la transformación Tseitin, la codificación anterior se puede traducir a CNF.

Este enfoque produce un CNF relativamente pequeño. Pero esta codificación no admite "Propagación de unidades" y, por lo tanto, el rendimiento de los solucionadores SAT es realmente malo.

Existen otros circuitos para la multiplicación que pueden usarse para este propósito, pero producen un CNF más grande.

Amir
fuente
10
En la sección 6.1 de "Encontrar instancias difíciles del problema de satisfacción: una encuesta", por Cook y Mitchell, utilizan este problema como un desafío.
Amir
¿Cómo sabe que A y B deben tener una longitud de n bits? ¿No podría ser n - 1 yn bits? Seguro que puede ser de 2n bits y 1 bit.
Ilya Gazman
1
@Babibu: Si estamos hablando de factorización general, tienes razón. Pero para el caso de RSA, sabemos que cada uno de los dos primos tiene bits. norte
Amir el
Entiendo que respondas pero no sé cómo continuar. ¿Puedes mostrar ? do2norte-2
Ilya Gazman
¿Qué pasa con RSA-129
Ilya Gazman
18

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.

Martin Schwarz
fuente
1
¡Ese enlace es muy bueno!
Huck Bennett
Si realmente intenta ingresar uno de esos números, encontrará que su código fuente usa el tipo de datos int y, por lo tanto, solo puede contener números de 32 bits, mientras que los números RSA sin factorizar comienzan en cientos de bits.
Elliot Gorokhovsky
9

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.

Alessandro Cosentino
fuente
1
Scott también escribió sobre esto: scottaaronson.com/blog/?p=676
Alessandro Cosentino
0

Ver satfactor:


Convierta la factorización entera en un problema booleano de SATISFIABILIDAD

Shane Neph

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 ...

Geremia
fuente
1
¿Puedes resumir las técnicas utilizadas por este software? En este sitio estamos más interesados ​​en algoritmos y técnicas, en lugar de un anuncio de una herramienta de software. Por ejemplo, las preguntas sobre la complejidad de la reducción. No veo cómo has abordado la pregunta; en los sitios de Stack Exchange, solo debe responder si puede responder la pregunta específica que se le hizo. Además, ¿tiene alguna relación con la herramienta o sus autores?
DW