Os principais solucionadores de SAT podem fatorar números fáceis?

Os solucionadores modernos de SAT são muito bons em resolver muitos exemplos reais de instâncias de SAT. No entanto, sabemos como gerar números difíceis: por exemplo, use uma redução do fatorial para o SAT e forneça os números RSA como entrada.

Isso levanta a questão: e se eu pegar um exemplo fácil de fatoração. Em vez de pegar dois números primos grandes em bits, e se eu pegar um primo on bits e um primo q em bits, deixe e a codificação como uma instância SAT. seria um número fácil de fatorar por métodos de busca por força bruta ou peneira, já que um dos fatores é tão pequeno; um solucionador moderno de SAT com alguma redução padrão de fatoração para SAT também adota essa estrutura?$n/2$$p$$\log n$$n/\log n$$N = pq$$\mathrm{FACTOR}(N)$$N$

É possível superar o fator de resolução de SAT onde rapidamente?| p | = log $N = pq$$|p| = \log n$

Existem outras instâncias muito mais simples que sabemos que os algoritmos atuais não podem resolver em tempo subexponencial. Esses algoritmos são incapazes de contar (quase todos são melhorias do DPLL que correspondem ao sistema de prova proposicional da Resolution).

Infelizmente, esses exemplos são instâncias insatisfatórias. A questão sobre encontrar instâncias naturais satisfatórias e naturais para esses algoritmos é um problema de pesquisa interessante (Russeell Impagliazzo mencionou isso durante o workshop de complexidade de provas no ano passado em Banff). Há casos satisfatórios em que sabemos que os algoritmos falham mal, se houver, mas eles não são muito naturais (são baseados em fórmulas que expressam a solidez dos algoritmos).

Em relação ao fatoração, se o tamanho dos números for pequeno (por exemplo, logarítmico, como no seu caso, ou seja, os números são apresentados em unário), teoricamente não há resultado que diga que não possa ser resolvido pelos algoritmos atuais e, de fato, possamos escrever de maneira simples. algoritmos de tempo polinomial que fatoram esses números. Portanto, se um determinado programa solucionador SAT pode resolvê-los pode depender do algoritmo específico.