Les meilleurs solveurs SAT peuvent-ils prendre en compte les nombres faciles?

Les solveurs SAT modernes sont très efficaces pour résoudre de nombreux exemples concrets d'instances SAT. Cependant, nous savons comment générer des disques durs: par exemple, utilisez une réduction de l'affacturage vers SAT et donnez les numéros RSA en entrée.

Cela soulève la question: et si je prends un exemple simple d'affacturage. Au lieu de prendre deux grands nombres premiers sur bits, que se passe-t-il si je prends un p premier sur log n bits et un premier q sur n / log n bits, soit N = p q et le codage F A C T O R ( N ) en tant qu'instance SAT. $n/2$$p$$\log n$$n/\log n$$N = pq$$\mathrm{FACTOR}(N)$$N$serait un nombre facile à factoriser par recherche par force brute ou par tamisage, car l'un des facteurs est si petit; Est-ce qu'un solveur SAT moderne avec une réduction standard de l'affacturage à SAT reprend également cette structure?

Peut dépasser le facteur -solveurs N = p q où | p | = log n rapidement?$N = pq$$|p| = \log n$

Il existe d'autres exemples beaucoup plus simples que nous savons de manière prouvable que les algorithmes actuels ne peuvent pas résoudre en temps sous-exponentiel. Ces algorithmes sont incapables de compter (presque tous sont des améliorations de DPLL qui correspondent au système de preuve propositionnelle Resolution).

Malheureusement, ces exemples ne sont pas des exemples satisfaisants. La question de la recherche d'instances dures naturelles satisfaisables pour ces algorithmes est un problème de recherche intéressant (Russeell Impagliazzo l'a mentionné lors de l'atelier de complexité de la preuve l'an dernier à Banff). Il existe des exemples satisfaisants que nous savons de manière prouvable que les algorithmes échouent mal s'il y en a, mais ils ne sont pas très naturels (ils sont basés sur des formules exprimant la solidité des algorithmes).

En ce qui concerne l'affacturage, si la taille des nombres est petite (par exemple logarithmique comme dans votre cas, c'est-à-dire que les nombres sont donnés en unaire), alors théoriquement il n'y a aucun résultat qui dit qu'il ne peut pas être résolu par les algorithmes actuels, et en fait, nous pouvons écrire simple algorithmes de temps polynomiaux qui tiennent compte de ces nombres. Donc, si un programme de résolution SAT particulier peut les résoudre, cela dépendra de l'algorithme particulier.