¿Los principales solucionadores de SAT pueden factorizar números fáciles?

Los solucionadores de SAT modernos son muy buenos para resolver muchos ejemplos del mundo real de instancias de SAT. Sin embargo, sabemos cómo generar los difíciles: por ejemplo, use una reducción de factoring a SAT y proporcione los números RSA como entrada.

Esto plantea la pregunta: ¿qué pasa si tomo un ejemplo fácil de factoring? En lugar de tomar dos números primos grandes en bits, ¿qué sucede si tomo un primo en bits y un primo q en bits, deje y la codificación como una instancia SAT. sería un número fácil de factorizar mediante métodos de búsqueda de fuerza bruta o tamiz, ya que uno de los factores es muy pequeño; ¿Un solucionador de SAT moderno con alguna reducción estándar de factoring a SAT también capta esta estructura?$n/2$$p$$\log n$$n/\log n$$N = pq$$\mathrm{FACTOR}(N)$$N$

Puede superar el factor de solución de SAT donde rápidamente?$N = pq$$|p| = \log n$

Hay otras instancias mucho más simples que sabemos que los algoritmos actuales no pueden resolver en un tiempo sub-exponencial. Estos algoritmos son incapaces de contar (casi todos son mejoras de DPLL que corresponden al sistema de resolución de prueba proposicional).

Lamentablemente, tales ejemplos son instancias insatisfactorias. La pregunta sobre cómo encontrar instancias duras satisfactorias naturales para estos algoritmos es un problema de investigación interesante (Russeell Impagliazzo lo mencionó durante el taller de complejidad de pruebas el año pasado en Banff). Hay instancias satisfactorias en las que sabemos que los algoritmos fallan gravemente si existe, pero no son muy naturales (se basan en fórmulas que expresan la solidez de los algoritmos).

Con respecto a la factorización, si el tamaño de los números es pequeño (por ejemplo, logarítmico como en su caso, es decir, los números se dan en unario), entonces, teóricamente, no hay ningún resultado que diga que los algoritmos actuales no pueden resolverlo, y de hecho podemos escribir de manera simple. algoritmos de tiempo polinómico que factorizan estos números. Entonces, si un programa particular de solución SAT puede resolverlos, puede depender del algoritmo particular.